@inproceedings(BGH14b,
 author       = {T. Bourke and R.J. van Glabbeek and P. H{\"o}fner},
 year         = {2014},
 title        = {A mechanized proof of loop freedom of the (untimed) {AODV} routing protocol},
 editor       = {F. Cassez and J.-F. Raskin},
 booktitle    = {Automated Technology for Verification and Analysis {\rm (ATVA '14)}},
 series       = {{\rm LNCS}},
 volume       = {8837},
 publisher    = {Springer},
 pages        = {47--63},
 doi          = {10.1007/978-3-319-11936-6\_5},
)
@article(BGH16,
 author       = {T. Bourke and R.J. van Glabbeek and P. H{\"o}fner},
 year         = {2016},
 title        = {Mechanizing a Process Algebra for Network Protocols},
 journal      = {Journal of Automated Reasoning},
 volume       = {56},
 number       = {3},
 pages        = {309--341},
 doi          = {10.1007/s10817-015-9358-9},
)
@techreport(Nist800-38D,
 author       = {M.J. Dworkin},
 year         = {2007},
 title        = {{Recommendation for Block Cipher Modes of Operation: Galois/Counter Mode (GCM) and GMAC}},
 type         = {NIST Special Publication 800-38D},
 institution  = {{National Institute of Standards and Technology (NIST), U.S. Department of Commerce}},
 doi          = {10.6028/NIST.SP.800-38D},
)
@book(E01,
 author       = {K. Etschberger},
 year         = {2001},
 title        = {Controller Area Network: Basics, Protocols, Chips and Applications},
 publisher    = {IXXAT Automation GmbH},
)
@inproceedings(ESOP12,
 author       = {A. Fehnker and R. J. van Glabbeek and P. H{\"o}fner and A. K. McIver and M. Portmann and W. L. Tan},
 year         = {2012},
 title        = {A Process Algebra for Wireless Mesh Networks},
 editor       = {H. Seidl},
 booktitle    = {European Symposium on Programming {\rm (ESOP '12)}},
 series       = {{\rm LNCS}},
 volume       = {7211},
 publisher    = {Springer},
 pages        = {295--315},
 doi          = {10.1007/978-3-642-28869-2\_15},
)
@article(GHPT16,
 author       = {R.J. van Glabbeek and P. H{\"o}fner and M. Portmann and W.L. Tan},
 year         = {2016},
 title        = {Modelling and Verifying the {AODV} Routing Protocol},
 journal      = {Distributed Computing},
 volume       = {29},
 number       = {4},
 pages        = {279--315},
 doi          = {10.1007/s00446-015-0262-7},
)
@misc(rfc2104,
 author       = {H. Krawczyk and M. Bellare and R. Canetti},
 year         = {1997},
 title        = {{HMAC:} Keyed-Hashing for Message Authentication},
 howpublished = {RFC 2104 (Informational, Errata Exist)},
 url          = {http://tools.ietf.org/html/rfc2104},
)
@book(NipkowPaulsonWenzel02,
 author       = {T. Nipkow and L. C. Paulson and M. Wenzel},
 year         = {2002},
 title        = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
 series       = {{\rm LNCS}},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@manual(CAN,
 organization = {Robert Bosch GmbH},
 address      = {Stuttgart, Germany},
 year         = {1991},
 title        = {CAN Specification{\rm , Version 2.0}},
 url          = {http://www.bosch-semiconductors.de/media/ubk_semiconductors/pdf_1/canliteratur/can2spec.pdf},
)
@inproceedings(Shin14,
 author       = {C. Shin},
 year         = {2014},
 title        = {A framework for fragmenting/reconstituting data frame in {Controller Area Network (CAN)}},
 booktitle    = {International Conference on Advanced Communication Technology {\rm (ICACT '14)}},
 publisher    = {IEEE},
 pages        = {1261--1264},
 doi          = {10.1109/ICACT.2014.6779161},
)
@misc(ShinPatent,
 author       = {C.M. Shin and T.M. Han and H.S. Ham and W.J. Lee},
 year         = {2010},
 title        = {Method for Transmitting/Receiving Data Frame in {CAN} Protocol},
 url          = {http://www.google.com/patents/US20100158045},
 note         = {US Patent App. 12/543,876},
)
@book(SD15,
 author       = {C. Sommer and F. Dressler},
 year         = {2015},
 title        = {Vehicular Networking},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781107110649},
)
@book(isotp,
 author       = {International Organization for Standardization},
 year         = {2011},
 title        = {Road Vehicles -- Diagnostic Communication Over Controller Area Network {(DoCAN)} -- Part 2: Transport protocol and network layer services},
 volume       = {ISO 15765-2:2011(en)},
 publisher    = {ISO},
 url          = {http://www.iso.org/iso/home/store/catalogue_ics/catalogue_detail_ics.htm?csnumber=54499},
)
@misc(rfc6151,
 author       = {S. Turner and L. Chen},
 year         = {2011},
 title        = {{Updated Security Considerations for the MD5 Message-Digest and the HMAC-MD5 Algorithms}},
 howpublished = {RFC 6151 (Informational)},
 url          = {http://tools.ietf.org/html/rfc6151},
)