{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T12:01:17Z","timestamp":1773835277432,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319156170","type":"print"},{"value":"9783319156187","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15618-7_2","type":"book-chapter","created":{"date-parts":[[2015,2,27]],"date-time":"2015-02-27T01:10:31Z","timestamp":1424999431000},"page":"17-33","source":"Crossref","is-referenced-by-count":12,"title":["Formal Verification of Privacy Properties in Electric Vehicle Charging"],"prefix":"10.1007","author":[{"given":"Marouane","family":"Fazouane","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henning","family":"Kopp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rens W.","family":"van der Heijden","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Le M\u00e9tayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Kargl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-06749-0_1","volume-title":"Privacy Technologies and Policy","author":"T. Antignac","year":"2014","unstructured":"Antignac, T., Le M\u00e9tayer, D.: Privacy by Design: From Technologies to Architectures. In: Preneel, B., Ikonomou, D. (eds.) APF 2014. LNCS, vol.\u00a08450, pp. 1\u201317. Springer, Heidelberg (2014)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Backes, M., D\u00fcrmuth, M., Karjoth, G.: Unification in Privacy Policy Evaluation - Translating EPAL into Prolog. In: POLICY, pp. 185\u2013188 (2004)","DOI":"10.1109\/POLICY.2004.1309165"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Barth, A., Mitchell, J.C., Datta, A., Sundaram, S.: Privacy and Utility in Business Processes. In: CSF, pp. 279\u2013294 (2007)","DOI":"10.1109\/CSF.2007.26"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-17714-9_10","volume-title":"Information Systems Security","author":"M.Y. Becker","year":"2010","unstructured":"Becker, M.Y., Malkis, A., Bussard, L.: A Practical Generic Privacy Language. In: Jha, S., Mathuria, A. (eds.) ICISS 2010. LNCS, vol.\u00a06503, pp. 125\u2013139. Springer, Heidelberg (2010)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005, pp. 331\u2013340. IEEE (2005)","DOI":"10.1109\/LICS.2005.8"},{"key":"2_CR6","unstructured":"Blanchet, B., Smyth, B.: Proverif 1.85: Automatic cryptographic protocol verifier, user manual and tutorial (2011)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-41157-1_9","volume-title":"Trustworthy Global Computing","author":"M. Brus\u00f3","year":"2013","unstructured":"Brus\u00f3, M., Chatzikokolakis, K., Etalle, S., den Hartog, J.: Linking Unlinkability. In: Palamidessi, C., Ryan, M.D. (eds.) TGC 2012. LNCS, vol.\u00a08191, pp. 129\u2013144. Springer, Heidelberg (2013)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Camenisch, J., Van Herreweghen, E.: Design and implementation of the idemix anonymous credential system. In: Proceedings of the 9th ACM Conference on Computer and Communications Security, pp. 21\u201330. ACM (2002)","DOI":"10.1145\/586110.586114"},{"issue":"4","key":"2_CR9","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S. Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Verifying Privacy-type Properties of Electronic Voting Protocols. Journal of Computer Security\u00a017(4), 435\u2013487 (2009), http:\/\/www.lsv.ens-cachan.fr\/Publis\/PAPERS\/PDF\/DKR-jcs08.pdf","journal-title":"Journal of Computer Security"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11787006_1","volume-title":"Automata, Languages and Programming","author":"C. Dwork","year":"2006","unstructured":"Dwork, C.: Differential Privacy. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 1\u201312. Springer, Heidelberg (2006)"},{"issue":"1","key":"2_CR11","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/1866739.1866758","volume":"54","author":"C. Dwork","year":"2011","unstructured":"Dwork, C.: A firm foundation for private data analysis. Commun. ACM\u00a054(1), 86\u201395 (2011)","journal-title":"Commun. ACM"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Glasgow, J., MacEwen, G., Panangaden, P.: A logic for reasoning about security. In: Proc. of the 3rd Computer Security Foundations Workshop, pp. 2\u201313 (1990)","DOI":"10.1109\/CSFW.1990.128180"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1145\/1324249.1324273","volume-title":"Proc. of the 11th Conf. on Th. Aspects of Rationality and Knowl.","author":"J.Y. Halpern","year":"2007","unstructured":"Halpern, J.Y., Pucella, R.: Dealing with Logical Omniscience. In: Proc. of the 11th Conf. on Th. Aspects of Rationality and Knowl., pp. 169\u2013176. ACM, USA (2007), http:\/\/doi.acm.org\/10.1145\/1324249.1324273"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"H\u00f6fer, C., Petit, J., Schmidt, R., Kargl, F.: POPCORN: privacy-preserving charging for eMobility. In: Proceedings of the 2013 ACM Workshop on Security, Privacy & Dependability for Cyber Vehicles, pp. 37\u201348. ACM (2013)","DOI":"10.1145\/2517968.2517971"},{"key":"2_CR15","unstructured":"ISO: Road vehicles - Vehicle-to-Grid Communication Interface - Part 1: General information and use-case definition. ISO 15118, International Organization for Standardization, Geneva, Switzerland (2012)"},{"key":"2_CR16","unstructured":"ISO: Road vehicles - Vehicle-to-Grid Communication Interface - Part 2: Technical protocol description and Open Systems Interconnections (OSI) layer requirements. ISO 15118, International Organization for Standardization, Geneva, Switzerland (2012)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Jafari, M., Fong, P.W.L., Safavi-Naini, R., Barker, K., Sheppard, N.P.: Towards defining semantic foundations for purpose-based privacy policies. In: CODASPY, pp. 213\u2013224 (2011)","DOI":"10.1145\/1943513.1943541"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-01465-9_11","volume-title":"Formal Aspects in Security and Trust","author":"D. M\u00e9tayer Le","year":"2009","unstructured":"Le M\u00e9tayer, D.: A Formal Privacy Management Framework. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol.\u00a05491, pp. 162\u2013176. Springer, Heidelberg (2009)"},{"key":"2_CR19","first-page":"95","volume-title":"Proc. of the 3rd ACM Conference on Data and Application Security and Privacy","author":"D. M\u00e9tayer Le","year":"2013","unstructured":"Le M\u00e9tayer, D.: Privacy by Design: A Formal Framework for the Analysis of Architectural Choices. In: Proc. of the 3rd ACM Conference on Data and Application Security and Privacy, pp. 95\u2013104. ACM, USA (2013), http:\/\/doi.acm.org\/10.1145\/2435349.2435361"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Li, L., Pang, J., Liu, Y., Sun, J., Dong, J.S.: Symbolic analysis of an electric vehicle charging protocol. In: Proc. 19th IEEE Conference on Engineering of Complex Computer Systems (ICECCS 2014). IEEE Computer Society (2014)","DOI":"10.1109\/ICECCS.2014.11"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Li, N., Li, T., Venkatasubramanian, S.: t-Closeness: Privacy Beyond k-Anonymity and l-Diversity. In: IEEE 23rd International Conference on Data Engineering, pp. 106\u2013115 (April 2007)","DOI":"10.1109\/ICDE.2007.367856"},{"key":"2_CR22","unstructured":"Li, N., Qardaji, W.H., Su, D.: Provably Private Data Anonymization: Or, k-Anonymity Meets Differential Privacy. CoRR abs\/1101.2604 (2011)"},{"key":"2_CR23","unstructured":"Li, N., Yu, T., Ant\u00f3n, A.I.: A semantics based approach to privacy languages. Comput. Syst. Sci. Eng.\u00a021(5) (2006)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-33167-1_23","volume-title":"Computer Security \u2013 ESORICS 2012","author":"J.K. Liu","year":"2012","unstructured":"Liu, J.K., Au, M.H., Susilo, W., Zhou, J.: Enhancing location privacy for electric vehicles (at the right time). In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol.\u00a07459, pp. 397\u2013414. Springer, Heidelberg (2012)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Ma, Z., Kargl, F., Weber, M.: A location privacy metric for V2X communication systems. In: IEEE Sarnoff Symposium, pp. 1\u20136 (March 2009)","DOI":"10.1109\/SARNOF.2009.4850318"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Machanavajjhala, A., Gehrke, J., Kifer, D., Venkitasubramaniam, M.: l-Diversity: Privacy Beyond k-Anonymity. In: ICDE, p. 24 (2006)","DOI":"10.1109\/ICDE.2006.1"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"May, M.J., Gunter, C.A., Lee, I.: Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies. In: CSFW, pp. 85\u201397 (2006)","DOI":"10.1109\/CSFW.2006.24"},{"issue":"9","key":"2_CR28","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1810891.1810916","volume":"53","author":"F. McSherry","year":"2010","unstructured":"McSherry, F.: Privacy integrated queries: an extensible platform for privacy-preserving data analysis. Commun. ACM\u00a053(9), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"McSherry, F., Talwar, K.: Mechanism Design via Differential Privacy. In: FOCS, pp. 94\u2013103 (2007)","DOI":"10.1109\/FOCS.2007.66"},{"key":"2_CR30","volume-title":"Communicating and Mobile Systems: The Pi-calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: The Pi-calculus. Cambridge University Press, New York (1999)"},{"key":"2_CR31","unstructured":"Pucella, R.: Deductive Algorithmic Knowledge. CoRR cs.AI\/0405038 (2004)"},{"key":"2_CR32","unstructured":"Ryan, M.D., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, ch.\u00a06. IOS Press (2011), http:\/\/www.bensmyth.com\/files\/Smyth10-applied-pi-calculus.pdf"},{"issue":"5","key":"2_CR33","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1142\/S0218488502001648","volume":"10","author":"L. Sweeney","year":"2002","unstructured":"Sweeney, L.: k-Anonymity: A Model for Protecting Privacy. International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems\u00a010(5), 557\u2013570 (2002)","journal-title":"International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Tschantz, M.C., Kaynar, D.K., Datta, A.: Formal Verification of Differential Privacy for Interactive Systems. CoRR abs\/1101.2819 (2011)","DOI":"10.1016\/j.entcs.2011.09.015"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Yu, T., Li, N., Ant\u00f3n, A.I.: A formal semantics for P3P. In: SWS, pp. 1\u20138 (2004)","DOI":"10.1145\/1111348.1111349"}],"container-title":["Lecture Notes in Computer Science","Engineering Secure Software and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15618-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T04:07:19Z","timestamp":1747714039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-15618-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319156170","9783319156187"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15618-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}