{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T06:43:04Z","timestamp":1750488184249,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319680620"},{"type":"electronic","value":"9783319680637"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68063-7_10","type":"book-chapter","created":{"date-parts":[[2017,9,12]],"date-time":"2017-09-12T04:23:18Z","timestamp":1505190198000},"page":"147-163","source":"Crossref","is-referenced-by-count":17,"title":["Formal Analysis of V2X Revocation Protocols"],"prefix":"10.1007","author":[{"given":"Jorden","family":"Whitefield","sequence":"first","affiliation":[]},{"given":"Liqun","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Frank","family":"Kargl","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Paverd","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Wesemeyer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,13]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Basin, D.A., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, pp. 1144\u20131155 (2015)","key":"10_CR1","DOI":"10.1145\/2810103.2813662"},{"doi-asserted-by":"crossref","unstructured":"Bi\u00dfmeyer, N., Petit, J., Bayarou, K.M.: CoPRA: conditional pseudonym resolution algorithm in VANETs. In: 2013 10th Annual Conference on Wireless On-demand Network Systems and Services (WONS), pp. 9\u201316. IEEE (2013)","key":"10_CR2","DOI":"10.1109\/WONS.2013.6578314"},{"unstructured":"Blanchet, B., Smyth, B., Cheval, V.: Proverif 1.96: automatic cryptographic protocol verifier, user manual and tutorial (2016). http:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/manual.pdf","key":"10_CR3"},{"issue":"4","key":"10_CR4","doi-asserted-by":"crossref","first-page":"23:1","DOI":"10.1145\/2926715","volume":"17","author":"R Chadha","year":"2016","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1\u201323:32 (2016)","journal-title":"ACM Trans. Comput. Log."},{"key":"10_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-78636-8","volume-title":"Operational Semantics and Verification of Security Protocols. Information Security and Cryptography","author":"C Cremers","year":"2012","unstructured":"Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Information Security and Cryptography. Springer, Heidelberg (2012)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15497-3_4","volume-title":"Computer Security \u2013 ESORICS 2010","author":"M Dahl","year":"2010","unstructured":"Dahl, M., Delaune, S., Steel, G.: Formal analysis of privacy for vehicular mix-zones. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 55\u201370. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15497-3_4"},{"key":"10_CR7","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/j.jlamp.2016.10.005","volume":"87","author":"S Delaune","year":"2017","unstructured":"Delaune, S., Hirschi, L.: A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J. Log. Algebraic Methods Program. 87, 127\u2013144 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-15618-7_2","volume-title":"Engineering Secure Software and Systems","author":"M Fazouane","year":"2015","unstructured":"Fazouane, M., Kopp, H., van der Heijden, R.W., M\u00e9tayer, D., Kargl, F.: Formal verification of privacy properties in electric vehicle charging. In: Piessens, F., Caballero, J., Bielova, N. (eds.) ESSoS 2015. LNCS, vol. 8978, pp. 17\u201333. Springer, Cham (2015). doi: 10.1007\/978-3-319-15618-7_2"},{"doi-asserted-by":"crossref","unstructured":"Feiri, M., Petit, J., Kargl, F.: Formal model of certificate omission schemes in VANET. In: 2014 IEEE Vehicular Networking Conference, VNC 2014, Paderborn, Germany, 3\u20135 December 2014, pp. 41\u201344 (2014)","key":"10_CR9","DOI":"10.1109\/VNC.2014.7013307"},{"unstructured":"Fischer, L., Aijaz, A., Eckert, C., Vogt, D.: Secure revocable anonymous authenticated inter-vehicle communication (SRAAC). In: 4th Conference on Embedded Security in Cars (ESCAR 2006), Berlin, Germany (2006)","key":"10_CR10"},{"issue":"Part 1","key":"10_CR11","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/j.adhoc.2015.09.011","volume":"37","author":"D F\u00f6rster","year":"2016","unstructured":"F\u00f6rster, D., Kargl, F., L\u00f6hr, H.: PUCA: a pseudonym scheme with strong privacy guarantees for vehicular ad-hoc networks. Ad Hoc Netw. 37(Part 1), 122\u2013132 (2016). Special Issue on Advances in Vehicular Networks","journal-title":"Ad Hoc Netw."},{"doi-asserted-by":"crossref","unstructured":"F\u00f6rster, D., L\u00f6hr, H., Zibuschka, J., Kargl, F.: REWIRE - revocation without resolution: a privacy-friendly revocation mechanism for vehicular ad-hoc networks. In: Trust and Trustworthy Computing - 8th International Conference, TRUST 2015, Heraklion, Greece, 24\u201326 August 2015, Proceedings, pp. 193\u2013208 (2015)","key":"10_CR12","DOI":"10.1007\/978-3-319-22846-4_12"},{"issue":"3","key":"10_CR13","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1109\/JSAC.2011.110309","volume":"29","author":"JJ Haas","year":"2011","unstructured":"Haas, J.J., Hu, Y.C., Laberteaux, K.P.: Efficient certificate revocation list organization and distribution. IEEE J. Sel. Areas Commun. 29(3), 595\u2013604 (2011)","journal-title":"IEEE J. Sel. Areas Commun."},{"unstructured":"van der Heijden, R.W., Dietzel, S., Leinm\u00fcller, T., Kargl, F.: Survey on misbehavior detection in cooperative intelligent transportation systems. CoRR abs\/1610.06810 (2016). http:\/\/arxiv.org\/abs\/1610.06810","key":"10_CR14"},{"doi-asserted-by":"crossref","unstructured":"Kondareddy, Y., Di Crescenzo, G., Agrawal, P.: Analysis of certificate revocation list distribution protocols for vehicular networks. In: Global Telecommunications Conference (GLOBECOM 2010), pp. 1\u20135, IEEE (2010)","key":"10_CR15","DOI":"10.1109\/GLOCOM.2010.5683985"},{"doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: 10th Computer Security Foundations Workshop, pp. 31\u201344. IEEE Computer Society (1997)","key":"10_CR16","DOI":"10.1109\/CSFW.1997.596782"},{"doi-asserted-by":"crossref","unstructured":"Ma, Z., Kargl, F., Weber, M.: Pseudonym-on-demand: a new pseudonym refill strategy for vehicular communications. In: IEEE 68th Vehicular Technology Conference, 2008. VTC 2008-Fall, pp. 1\u20135. IEEE (2008)","key":"10_CR17","DOI":"10.1109\/VETECF.2008.455"},{"unstructured":"Meier, S., Schmidt, B.: Tamarin prover - information security group \u2014 eth zurich (2016). http:\/\/www.infsec.ethz.ch\/research\/software\/tamarin.html . Accessed 18 Jan 2017","key":"10_CR18"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_48"},{"doi-asserted-by":"crossref","unstructured":"Michael, E.N., Henry, L.O.: Scalable certificate revocation list distribution in vehicular ad hoc networks. In: GLOBECOM Workshops (GC Wkshps), pp. 54\u201358. IEEE (2010)","key":"10_CR20","DOI":"10.1109\/GLOCOMW.2010.5700380"},{"doi-asserted-by":"crossref","unstructured":"Backes, M., Jannik Dreier, S.K., K\u00fcnnemann, R.: A novel approach for reasoning about liveness in cryptographic protocols and its application to fair exchange. In: 2nd IEEE European Symposium on Security and Privacy (2017)","key":"10_CR21","DOI":"10.1109\/EuroSP.2017.12"},{"issue":"11","key":"10_CR22","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1109\/MCOM.2008.4689252","volume":"46","author":"P Papadimitratos","year":"2008","unstructured":"Papadimitratos, P., Buttyan, L., Holczer, T., Schoch, E., Freudiger, J., Raya, M., Ma, Z., Kargl, F., Kung, A., Hubaux, J.P.: Secure vehicular communication systems: design and architecture. IEEE Commun. Mag. 46(11), 100\u2013109 (2008)","journal-title":"IEEE Commun. Mag."},{"doi-asserted-by":"crossref","unstructured":"Papadimitratos, P., Buttyan, L., Hubaux, J.P., Kargl, F., Kung, A., Raya, M.: Architecture for secure and private vehicular communications. In: 2007 7th International Conference on ITS Telecommunications, pp. 1\u20136. IEEE (2007)","key":"10_CR23","DOI":"10.1109\/ITST.2007.4295890"},{"doi-asserted-by":"crossref","unstructured":"Papadimitratos, P.P., Mezzour, G., Hubaux, J.P.: Certificate revocation list distribution in vehicular communication systems. In: Proceedings of the Fifth ACM International Workshop on VehiculAr Inter-NETworking, pp. 86\u201387. ACM (2008)","key":"10_CR24","DOI":"10.1145\/1410043.1410062"},{"issue":"1","key":"10_CR25","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1109\/COMST.2014.2345420","volume":"17","author":"J Petit","year":"2015","unstructured":"Petit, J., Schaub, F., Feiri, M., Kargl, F.: Pseudonym schemes in vehicular networks: a survey. IEEE Commun. Surv. Tutor. 17(1), 228\u2013255 (2015)","journal-title":"IEEE Commun. Surv. Tutor."},{"unstructured":"PRECIOSA: European commission : Cordis : Projects and results service : Privacy enabled capability in co-operative systems and safety applications (2010). http:\/\/cordis.europa.eu\/project\/rcn\/86606_en.html . Accessed 31 Jan 2017","key":"10_CR26"},{"unstructured":"PRESERVE: www.preserve-project.eu \u2014 preparing secure V2X communication systems (2011). https:\/\/preserve-project.eu\/ . Accessed 31 Jan 2017","key":"10_CR27"},{"unstructured":"Rabin, M.O.: Digitalized signatures and public-key functions as intractable as factorization. In: Foundations of Secure Computation, pp. 155\u2013168 (1978)","key":"10_CR28"},{"issue":"8","key":"10_CR29","doi-asserted-by":"crossref","first-page":"1557","DOI":"10.1109\/JSAC.2007.071006","volume":"25","author":"M Raya","year":"2007","unstructured":"Raya, M., Papadimitratos, P., Aad, I., Jungels, D., Hubaux, J.P.: Eviction of misbehaving and faulty nodes in vehicular networks. IEEE J. Sel. A. Commun. 25(8), 1557\u20131568 (2007)","journal-title":"IEEE J. Sel. A. Commun."},{"doi-asserted-by":"crossref","unstructured":"Schaub, F., Kargl, F., Ma, Z., Weber, M.: V-Tokens for conditional pseudonymity in VANETs. In: 2010 IEEE Wireless Communications and Networking Conference, WCNC 2010, Proceedings, Sydney, Australia, 18\u201321 April 2010, pp. 1\u20136 (2010)","key":"10_CR30","DOI":"10.1109\/WCNC.2010.5506126"},{"doi-asserted-by":"crossref","unstructured":"Schaub, F., Ma, Z., Kargl, F.: Privacy requirements in vehicular communication systems. In: Computational Science and Engineering, CSE 2009, vol. 3, pp. 139\u2013145, IEEE (2009)","key":"10_CR31","DOI":"10.1109\/CSE.2009.135"},{"doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, 25\u201327 June 2012, pp. 78\u201394 (2012)","key":"10_CR32","DOI":"10.1109\/CSF.2012.25"},{"unstructured":"Weyl, B., Henniger, O., Ruddle, A., Seudie, H., Wolf, M., Wollinger, T.: Securing vehicular on-board IT systems: the EVITA project. In: 25th Joint VDI\/VW Automotive Security Conference, Ingolstadt, Germany (2009). http:\/\/www.evita-project.org\/Publications\/HRSW09.pdf","key":"10_CR33"},{"unstructured":"Whitefield, J., Chen, L., Kargl, F., Schneider, S., Treharne, H., Wesemeyer, S.: Formal analysis of V2X revocation protocols (2017). http:\/\/www.computing.surrey.ac.uk\/personal\/st\/H.Treharne\/papers\/2017\/rewire.html","key":"10_CR34"},{"unstructured":"Willke, T.L., Tientrakool, P., Maxemchuk, N.F.: A survey of inter-vehicle communication protocols and their applications. IEEE Commun. Surv. Tutor. 11(2), 3\u201320 (2009)","key":"10_CR35"}],"container-title":["Lecture Notes in Computer Science","Security and Trust Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68063-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T06:37:24Z","timestamp":1570084644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68063-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319680620","9783319680637"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68063-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}