{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:01:24Z","timestamp":1777806084973,"version":"3.51.4"},"reference-count":52,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T00:00:00Z","timestamp":1555977600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2019,6,10]]},"abstract":"<jats:p>In this paper, we consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus, notably used in the [Formula: see text]\u00a0tool. Existing tools and techniques do not allow to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using [Formula: see text]. Our two conditions correspond to two broad classes of attacks on unlinkability, i.e.\u00a0data and control-flow leaks. This theoretical result is general enough that it applies to a wide class of protocols based on a variety of cryptographic primitives. In particular, using our tool, [Formula: see text], we provide the first formal security proofs of protocols such as BAC and PACE (e-passport), Hash-Lock (RFID authentication), etc. Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in a weak sense).<\/jats:p>","DOI":"10.3233\/jcs-171070","type":"journal-article","created":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T12:18:03Z","timestamp":1556021883000},"page":"277-342","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":15,"title":["A method for unbounded verification of privacy-type properties"],"prefix":"10.1177","volume":"27","author":[{"given":"Lucca","family":"Hirschi","sequence":"first","affiliation":[{"name":"Inria & LORIA, France. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Baelde","sequence":"additional","affiliation":[{"name":"LSV, ENS Paris-Saclay, CNRS & Universit\u00e9 Paris-Saclay, France. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phanie","family":"Delaune","sequence":"additional","affiliation":[{"name":"Univ Rennes, CNRS, IRISA, France. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2019,4,23]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"M.\u00a0Abadi and B.\u00a0Blanchet, Computer-assisted verification of a protocol for certified email, in: Static Analysis, Springer, 2003, pp.\u00a0316\u2013335. doi:10.1007\/3-540-44898-5_17.","DOI":"10.1007\/3-540-44898-5_17"},{"key":"ref002","doi-asserted-by":"crossref","unstructured":"M.\u00a0Abadi and C.\u00a0Fournet, Mobile values, new names, and secure communication, in: Proceedings of POPL\u201901, ACM Press, 2001.","DOI":"10.1145\/360204.360213"},{"key":"ref003","doi-asserted-by":"crossref","unstructured":"G.\u00a0Alp\u00e1r and J.H.\u00a0Hoepman, A secure channel for attribute-based credentials:[short paper], in: Proceedings of the 2013 ACM Workshop on Digital Identity Management, ACM, 2013, pp.\u00a013\u201318. doi:10.1145\/2517881.2517884.","DOI":"10.1145\/2517881.2517884"},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"M.\u00a0Arapinis, V.\u00a0Cheval and S.\u00a0Delaune, Verifying privacy-type properties in a modular way, in: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF\u201912), IEEE Computer Society Press, Cambridge Massachusetts, USA, 2012, pp.\u00a095\u2013109.","DOI":"10.1109\/CSF.2012.16"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"M.\u00a0Arapinis, T.\u00a0Chothia, E.\u00a0Ritter and M.\u00a0Ryan, Analysing unlinkability and anonymity using the applied pi calculus, in: Proceedings of CSF\u201910, IEEE Comp. Soc. Press, 2010.","DOI":"10.1109\/CSF.2010.15"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"M.\u00a0Arapinis, L.\u00a0Mancini, E.\u00a0Ritter, M.\u00a0Ryan, N.\u00a0Golde, K.\u00a0Redon and R.\u00a0Borgaonkar, New privacy issues in mobile telephony: Fix and verification, in: Proceedings of the ACM Conference on Computer and Communications Security, ACM, 2012, pp.\u00a0205\u2013216.","DOI":"10.1145\/2382196.2382221"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"M.\u00a0Arapinis, L.I.\u00a0Mancini, E.\u00a0Ritter and M.\u00a0Ryan, Privacy through pseudonymity in mobile telephony systems, in: NDSS, 2014.","DOI":"10.14722\/ndss.2014.23082"},{"key":"ref008","unstructured":"A.\u00a0Armando et al., The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures, in: Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201912), Vol.\u00a07214, Springer, 2012, pp.\u00a0267\u2013282."},{"key":"ref009","doi-asserted-by":"crossref","unstructured":"A.\u00a0Armando, R.\u00a0Carbone, L.\u00a0Compagna, J.\u00a0Cu\u00e9llar and M.L.\u00a0Tobarra, Formal analysis of SAML 2.0 web browser single sign-on: Breaking the SAML-based single sign-on for Google apps, in: Proc. 6th ACM Workshop on Formal Methods in Security Engineering (FMSE\u201908), ACM, 2008, pp.\u00a01\u201310.","DOI":"10.1145\/1456396.1456397"},{"key":"ref010","doi-asserted-by":"crossref","unstructured":"M.\u00a0Backes, C.\u00a0Hritcu and M.\u00a0Maffei, Automated verification of remote electronic voting protocols in the applied pi-calculus, in: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, 23\u201325 June, IEEE Computer Society, Pittsburgh, Pennsylvania, 2008, pp.\u00a0195\u2013209. doi:10.1109\/CSF.2008.26.","DOI":"10.1109\/CSF.2008.26"},{"key":"ref011","doi-asserted-by":"crossref","unstructured":"M.\u00a0Backes, M.\u00a0Maffei and D.\u00a0Unruh, Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol, in: Security and Privacy, SP 2008. IEEE Symposium on, IEEE, 2008, pp.\u00a0202\u2013215.","DOI":"10.1109\/SP.2008.23"},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"D.\u00a0Basin, J.\u00a0Dreier, L.\u00a0Hirschi, S.\u00a0Radomirovi\u0107, R.\u00a0Sasse and V.\u00a0Stettler, Formal analysis of 5G authentication, 2018, arXiv preprint arXiv:1806.10360.","DOI":"10.1145\/3243734.3243846"},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"D.\u00a0Basin, J.\u00a0Dreier and R.\u00a0Sasse, Automated symbolic proofs of observational equivalence, in: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, ACM, 2015, pp.\u00a01144\u20131155.","DOI":"10.1145\/2810103.2813662"},{"key":"ref014","doi-asserted-by":"crossref","unstructured":"M.\u00a0Baudet, Deciding security of protocols against off-line guessing attacks, in: Proc. 12th Conference on Computer and Communications Security, ACM, 2005.","DOI":"10.1145\/1102120.1102125"},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"J.\u00a0Bender, \u00d6.\u00a0Dagdelen, M.\u00a0Fischlin and D.\u00a0K\u00fcgler, The pace aa protocol for machine readable travel documents, and its security, in: Financial Cryptography and Data Security, Springer, 2012, pp.\u00a0344\u2013358. doi:10.1007\/978-3-642-32946-3_25.","DOI":"10.1007\/978-3-642-32946-3_25"},{"key":"ref016","doi-asserted-by":"crossref","unstructured":"J.\u00a0Bender, M.\u00a0Fischlin and D.\u00a0K\u00fcgler, Security analysis of the pace key-agreement protocol, in: Information Security, Springer, 2009, pp.\u00a033\u201348. doi:10.1007\/978-3-642-04474-8_3.","DOI":"10.1007\/978-3-642-04474-8_3"},{"key":"ref017","doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, in: Proceedings of CSFW\u201901, IEEE Comp. Soc. Press, 2001, pp.\u00a082\u201396.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref018","doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet, M.\u00a0Abadi and C.\u00a0Fournet, Automated verification of selected equivalences for security protocols,\n                      Journal of Logic and Algebraic Programming\n                      (2008).","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"ref019","doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet and B.\u00a0Smyth, Automated reasoning for equivalences in the applied pi calculus with barriers, in: Proc. 29th Computer Security Foundations Symposium, 2016.","DOI":"10.1109\/CSF.2016.29"},{"key":"ref020","unstructured":"M.\u00a0Brus\u00f3, Dissecting Unlinkability, PhD thesis, Technische Universiteit Eindhoven, 2014."},{"key":"ref021","doi-asserted-by":"crossref","unstructured":"M.\u00a0Brus\u00f3, K.\u00a0Chatzikokolakis and J.\u00a0den Hartog, Formal verification of privacy for RFID systems, in: Proceedings of CSF\u201910, 2010.","DOI":"10.1109\/CSF.2010.13"},{"key":"ref022","doi-asserted-by":"crossref","unstructured":"M.\u00a0Brus\u00f3, K.\u00a0Chatzikokolakis, S.\u00a0Etalle and J.\u00a0Den Hartog, Linking unlinkability, in: Trustworthy Global Computing, Springer, 2012, pp.\u00a0129\u2013144.","DOI":"10.1007\/978-3-642-41157-1_9"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.7"},{"key":"ref024","doi-asserted-by":"crossref","unstructured":"J.\u00a0Camenisch, S.\u00a0M\u00f6dersheim and D.\u00a0Sommer, A formal model of identity mixer, in: Formal Methods for Industrial Critical Systems, Springer, 2010, pp.\u00a0198\u2013214. doi:10.1007\/978-3-642-15898-8_13.","DOI":"10.1007\/978-3-642-15898-8_13"},{"key":"ref025","unstructured":"L.\u00a0Cheikhrouhou, W.\u00a0Stephan, \u00d6.\u00a0Dagdelen, M.\u00a0Fischlin and M.\u00a0Ullmann, Merging the cryptographic security analysis and the algebraic-logic security proof of pace, in: Sicherheit, 2012, pp.\u00a083\u201394."},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cheval and B.\u00a0Blanchet, Proving more observational equivalences with ProVerif, in: Proc. 2nd Conference on Principles of Security and Trust, LNCS, Vol.\u00a07796, Springer, 2013, pp.\u00a0226\u2013246. doi:10.1007\/978-3-642-36830-1_12.","DOI":"10.1007\/978-3-642-36830-1_12"},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cheval, H.\u00a0Comon-Lundh and S.\u00a0Delaune, Trace equivalence decision: Negative tests and non-determinism, in: Proceedings of CCS\u201911, ACM Press, 2011.","DOI":"10.1145\/2046707.2046744"},{"key":"ref028","doi-asserted-by":"crossref","unstructured":"R.\u00a0Chr\u00e9tien, V.\u00a0Cortier and S.\u00a0Delaune, From security protocols to pushdown automata, ACM Transactions on Computational Logic 1 (2015), 3.","DOI":"10.1145\/2811262"},{"key":"ref029","doi-asserted-by":"crossref","unstructured":"K.\u00a0Cohn-Gordon, C.\u00a0Cremers, B.\u00a0Dowling, L.\u00a0Garratt and D.\u00a0Stebila, A formal security analysis of the signal messaging protocol, in: Security and Privacy (EuroS&P), 2017 IEEE European Symposium on, IEEE, 2017, pp.\u00a0451\u2013466. doi:10.1109\/EuroSP.2017.27.","DOI":"10.1109\/EuroSP.2017.27"},{"key":"ref030","doi-asserted-by":"crossref","unstructured":"H.\u00a0Comon and A.\u00a0Koutsos, Formal computational unlinkability proofs of rfid protocols, in: 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 2017, pp.\u00a0100\u2013114. doi:10.1109\/CSF.2017.9.","DOI":"10.1109\/CSF.2017.9"},{"key":"ref031","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2006-14101"},{"key":"ref032","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2012-0458"},{"key":"ref033","doi-asserted-by":"crossref","unstructured":"S.\u00a0Delaune and L.\u00a0Hirschi, A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols,\n                      Journal of Logical and Algebraic Methods in Programming\n                      (2016).","DOI":"10.1016\/j.jlamp.2016.10.005"},{"key":"ref034","doi-asserted-by":"crossref","unstructured":"S.\u00a0Delaune, S.\u00a0Kremer and M.D.\u00a0Ryan, Verifying privacy-type properties of electronic voting protocols,\n                      Journal of Computer Security\n                      4\n                      (2008).","DOI":"10.3233\/JCS-2009-0340"},{"key":"ref035","doi-asserted-by":"crossref","unstructured":"S.\u00a0Delaune, M.D.\u00a0Ryan and B.\u00a0Smyth, Automatic verification of privacy properties in the applied pi-calculus, in: Proceedings of the 2nd Joint ITrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM\u201908), IFIP Conference Proceedings, Vol.\u00a0263, Springer, 2008.","DOI":"10.1007\/978-0-387-09428-1_17"},{"key":"ref036","doi-asserted-by":"crossref","unstructured":"N.\u00a0Dong, H.\u00a0Jonker and J.\u00a0Pang, Formal analysis of privacy in an ehealth protocol, in: Computer Security\u2013ESORICS 2012, Springer, 2012, pp.\u00a0325\u2013342. doi:10.1007\/978-3-642-33167-1_19.","DOI":"10.1007\/978-3-642-33167-1_19"},{"key":"ref037","doi-asserted-by":"crossref","unstructured":"J.\u00a0Dreier, L.\u00a0Hirschi, S.\u00a0Radomirovic and R.\u00a0Sasse, Automated unbounded verification of stateful cryptographic protocols with exclusive or, in: 31st IEEE Computer Security Foundations Symposium (CSF\u20192018), 2018.","DOI":"10.1109\/CSF.2018.00033"},{"key":"ref038","doi-asserted-by":"crossref","unstructured":"M.\u00a0Feldhofer, S.\u00a0Dominikus and J.\u00a0Wolkerstorfer, Strong authentication for RFID systems using the AES algorithm, in: Cryptographic Hardware and Embedded Systems-CHES 2004, Springer, 2004, pp.\u00a0357\u2013370. doi:10.1007\/978-3-540-28632-5_26.","DOI":"10.1007\/978-3-540-28632-5_26"},{"key":"ref039","unstructured":"L.\u00a0Hirschi, Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice, PhD thesis, \u00c9cole Normale Sup\u00e9rieure Paris-Saclay, 2017."},{"key":"ref040","doi-asserted-by":"crossref","unstructured":"L.\u00a0Hirschi, D.\u00a0Baelde and S.\u00a0Delaune, A method for verifying privacy-type properties: The unbounded case, in: Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P\u201916), IEEE Computer Society Press, San Jose, California, USA, 2016.","DOI":"10.1109\/SP.2016.40"},{"key":"ref041","unstructured":"Iso 15408-2: Common criteria for information technology security evaluation \u2013 part 2: Security functional components, 2009."},{"key":"ref042","doi-asserted-by":"crossref","unstructured":"A.\u00a0Juels and S.A.\u00a0Weis, Defining strong privacy for RFID, ACM Transactions on Information and System Security (TISSEC) 13(1) (2009), 7. doi:10.1145\/1609956.1609963.","DOI":"10.1145\/1609956.1609963"},{"key":"ref043","unstructured":"S.\u00a0Lee, T.\u00a0Asano and K.\u00a0Kim, RFID mutual authentication scheme based on synchronized secret information, in: Symposium on Cryptography and Information Security, 2006."},{"key":"ref044","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806125"},{"key":"ref045","doi-asserted-by":"crossref","unstructured":"S.\u00a0Meier, B.\u00a0Schmidt, C.\u00a0Cremers and D.\u00a0Basin, The tamarin prover for the symbolic analysis of security protocols, in: Proc. 25th International Conference on Computer Aided Verification (CAV\u201913), LNCS, Vol.\u00a08044, Springer, 2013, pp.\u00a0696\u2013701.","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref046","unstructured":"C.\u00a0Paquin and G.\u00a0Zaverucha, U-prove cryptographic specification v1.1 (revision 3), December 2013."},{"key":"ref047","doi-asserted-by":"crossref","unstructured":"A.\u00a0Pfitzmann and M.\u00a0K\u00f6hntopp, Anonymity, Unobservability, and Pseudonymity\u00a0\u2013 a Proposal for Terminology. In Designing Privacy Enhancing Technologies, Springer, 2001, pp.\u00a01\u20139.","DOI":"10.1007\/3-540-44702-4_1"},{"key":"ref048","unstructured":"PKI for machine readable travel documents offering ICC read-only access, 2004, Technical report, International Civil Aviation Organization."},{"key":"ref049","doi-asserted-by":"crossref","unstructured":"S.\u00a0Santiago, S.\u00a0Escobar, C.\u00a0Meadows and J.\u00a0Meseguer, A formal definition of protocol indistinguishability and its verification using maude-npa, in: Security and Trust Management, Springer, 2014, pp.\u00a0162\u2013177.","DOI":"10.1007\/978-3-319-11851-2_11"},{"key":"ref050","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.04.004"},{"key":"ref051","unstructured":"UKano tool and case studies. http:\/\/projects.lsv.ens-cachan.fr\/ukano\/. Accessed: 12-11-2018."},{"key":"ref052","unstructured":"T.\u00a0Van Deursen and S.\u00a0Radomirovic, Attacks on RFID protocols, IACR Cryptology ePrint Archive 2008 (2008), 310."}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-171070","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-171070","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-171070","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:18Z","timestamp":1777495518000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-171070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,23]]},"references-count":52,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6,10]]}},"alternative-id":["10.3233\/JCS-171070"],"URL":"https:\/\/doi.org\/10.3233\/jcs-171070","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4,23]]}}}