{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T14:31:52Z","timestamp":1768314712868,"version":"3.49.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319101804","type":"print"},{"value":"9783319101811","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10181-1_15","type":"book-chapter","created":{"date-parts":[[2014,8,29]],"date-time":"2014-08-29T14:28:38Z","timestamp":1409322518000},"page":"241-255","source":"Crossref","is-referenced-by-count":15,"title":["Formal Security Analysis of the MaCAN Protocol"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Bruni","sequence":"first","affiliation":[]},{"given":"Michal","family":"Sojka","sequence":"additional","affiliation":[]},{"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Hanne","family":"Riis Nielson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: Verification of Stateful Processes. In: 2011 IEEE 24th Computer Security Foundations, pp. 33\u201347 (2011)","DOI":"10.1109\/CSF.2011.10"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE workshop on Computer Security Foundations, pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"4","key":"15_CR3","doi-asserted-by":"crossref","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B. Blanchet","year":"2009","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security\u00a017(4), 363\u2013434 (2009)","journal-title":"Journal of Computer Security"},{"key":"15_CR4","unstructured":"Blanchet, B., Smyth, B.: Proverif 1.88: Automatic cryptographic protocol verifier, user manual and tutorial (2013)"},{"key":"15_CR5","unstructured":"Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., Savage, S., Koscher, K., Czeskis, A., Roesner, F., Kohno, T.: Comprehensive experimental analyses of automotive attack surfaces. In: Proceedings of the 20th USENIX Conference on Security (2011)"},{"issue":"3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s11241-007-9012-7","volume":"35","author":"R.I. Davis","year":"2007","unstructured":"Davis, R.I., Burns, A., Bril, R.J., Lukkien, J.J.: Controller area network (CAN) schedulability analysis: Refuted, revisited and revised. Real-Time Systems\u00a035(3), 239\u2013272 (2007)","journal-title":"Real-Time Systems"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Dworkin, M.J.: SP 800-38B. recommendation for block cipher modes of operation: the CMAC mode for authentication (2005)","DOI":"10.6028\/NIST.SP.800-38b-2005"},{"key":"15_CR8","unstructured":"FlexRay Consortium, et al.: FlexRay communications system-protocol specification. Version, 2(1):198\u2013207 (2005)"},{"key":"15_CR9","unstructured":"Robert\u00a0Bosch GmbH. Road vehicles \u2013 Controller area network (CAN) \u2013 Part 1: Data link layer and physical signalling (1991)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Groza, B., Murvay, S., Van Herrewege, A., Verbauwhede, I.: LiBrA-CAN: a Lightweight Broadcast Authentication protocol for Controller Area Networks (2012)","DOI":"10.1007\/978-3-642-35404-5_15"},{"key":"15_CR11","unstructured":"Hartkopp, O., Reuber, C., Schilling, R.: MaCAN - message authenticated CAN. In: Proceedings of the 10th Escar Conference on Embedded Security in Cars (2012)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Koscher, K., Czeskis, A., Roesner, F., Patel, S., Kohno, T., Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., Savage, S.: Experimental Security Analysis of a Modern Automobile. In: 2010 IEEE Symposium on Security and Privacy, pp. 447\u2013462 (2010)","DOI":"10.1109\/SP.2010.34"},{"key":"15_CR13","unstructured":"Hartwich, F.: CAN with Flexible Data-Rate (2005)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proceedings of the 10th Computer Security Foundations Workshop, pp. 31\u201343. IEEE (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S.A.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 351\u2013360. ACM (2010)","DOI":"10.1145\/1866307.1866348"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Schweppe, H., Roudier, Y., Weyl, B., Apvrille, L., Scheuermann, D.: Car2x communication: securing the last meter-a cost-effective approach for ensuring trust in car2x applications using in-vehicle symmetric cryptography. In: Vehicular Technology Conference (VTC Fall), pp. 1\u20135. IEEE (2011)","DOI":"10.1109\/VETECF.2011.6093081"},{"key":"15_CR17","unstructured":"Van Herrewege, A., Singelee, D., Verbauwhede, I.: CANAuth \u2014 a simple, backward compatible broadcast authentication protocol for CAN bus. In: ECRYPT Workshop on Lightweight Cryptography 2011 (2011)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Ziermann, T., Wildermann, S., Teich, J.: CAN+: A new backward-compatible Controller Area Network (CAN) protocol with up to 16\u00d7 higher data rates. In: Design, Automation & Test in Europe Conference & Exhibition, pp. 1088\u20131093. IEEE (2009)","DOI":"10.1109\/DATE.2009.5090826"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10181-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T11:48:10Z","timestamp":1746359290000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10181-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319101804","9783319101811"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10181-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}