{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:01:38Z","timestamp":1777806098857,"version":"3.51.4"},"reference-count":64,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T00:00:00Z","timestamp":1573603200000},"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":[[2020,2,4]]},"abstract":"<jats:p>In cryptographic protocols, in particular RFID protocols, exclusive-or (XOR) operations are common. Due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. In this paper, we improve the Tamarin prover and its underlying theory to deal with an equational theory modeling XOR operations. The XOR theory can be combined with all equational theories previously supported, including user-defined equational theories. This makes Tamarin the first verification tool for cryptographic protocols in the symbolic model to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.<\/jats:p>","DOI":"10.3233\/jcs-191358","type":"journal-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T08:20:58Z","timestamp":1573633258000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":10,"title":["Verification of stateful cryptographic protocols with exclusive OR"],"prefix":"10.1177","volume":"28","author":[{"given":"Jannik","family":"Dreier","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, France. E-mails:\u00a0,\u00a0"}]},{"given":"Lucca","family":"Hirschi","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, France. E-mails:\u00a0,\u00a0"}]},{"given":"Sa\u0161a","family":"Radomirovi\u0107","sequence":"additional","affiliation":[{"name":"School of Science and Engineering, University of Dundee, UK. E-mail:\u00a0"}]},{"given":"Ralf","family":"Sasse","sequence":"additional","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Switzerland. E-mail:\u00a0"}]}],"member":"179","published-online":{"date-parts":[[2019,11,13]]},"reference":[{"key":"ref001","unstructured":"3GPP, 3G security; Security architecture, TS, 33.102, 3rd Generation Partnership Project (3GPP), http:\/\/www.3gpp.org\/DynaReport\/33102.htm."},{"key":"ref002","unstructured":"3GPP, System Architecture Evolution (SAE), TR, 33.401, 3rd Generation Partnership Project (3GPP), http:\/\/www.3gpp.org\/DynaReport\/33401.htm."},{"key":"ref003","unstructured":"3GPP, Security Architecture and Procedures for 5G System, TS, 33.501, 3rd Generation Partnership Project (3GPP), http:\/\/www.3gpp.org\/DynaReport\/33501.htm."},{"key":"ref004","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 the IEEE Computer Security Foundations Symposium, IEEE Comp. Soc. Press, 2010.","DOI":"10.1109\/CSF.2010.15"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"M.\u00a0Arapinis, E.\u00a0Ritter and M.\u00a0Ryan, StatVerif: Verification of stateful processes, in: Proc. 24th IEEE Computer Security Foundations Symposium (CSF\u201911), IEEE Press, 2011, pp.\u00a033\u201347.","DOI":"10.1109\/CSF.2011.10"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"A.\u00a0Armando, D.A.\u00a0Basin, Y.\u00a0Boichut, Y.\u00a0Chevalier, L.\u00a0Compagna, J.\u00a0Cu\u00e9llar, P.H.\u00a0Drielsma, P.C.\u00a0H\u00e9am, O.\u00a0Kouchnarenko, J.\u00a0Mantovani, S.\u00a0M\u00f6dersheim, D.\u00a0von Oheimb, M.\u00a0Rusinowitch, J.\u00a0Santiago, M.\u00a0Turuani, L.\u00a0Vigan\u00f2 and L.\u00a0Vigneron, The AVISPA tool for the automated validation of Internet security protocols and applications, in: CAV, 2005, pp.\u00a0281\u2013285.","DOI":"10.1007\/11513988_27"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"A.\u00a0Armando, R.\u00a0Carbone, L.\u00a0Compagna, J.\u00a0Cuellar and L.\u00a0Tobarra, Formal analysis of SAML 2.0 web browser single sign-on: Breaking the SAML-based single sign-on for Google apps, in: Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, ACM, 2008, pp.\u00a01\u201310.","DOI":"10.1145\/1456396.1456397"},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.22"},{"key":"ref009","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, J.M.\u00a0Crespo, B.\u00a0Gr\u00e9goire, C.\u00a0Kunz, Y.\u00a0Lakhnech, B.\u00a0Schmidt and S.Z.\u00a0B\u00e9guelin, Fully automated analysis of padding-based encryption in the computational model, in: 2013 ACM SIGSAC Conference on Computer and Communications, Security, CCS\u201913, Berlin, Germany, November 4\u20138, 2013, A.\u00a0Sadeghi, V.D.\u00a0Gligor and M.\u00a0Yung, eds, ACM, 2013, pp.\u00a01247\u20131260. ISBN 978-1-4503-2477-9.","DOI":"10.1145\/2508859.2516663"},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"ref011","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, B.\u00a0Gr\u00e9goire and B.\u00a0Schmidt, Automated proofs of pairing-based cryptography, in: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, October 12\u20136, 2015, I.\u00a0Ray, N.\u00a0Li and C.\u00a0Kruegel, eds, ACM, 2015, pp.\u00a01156\u20131168. ISBN 978-1-4503-3832-5.","DOI":"10.1145\/2810103.2813697"},{"key":"ref012","doi-asserted-by":"publisher","DOI":"10.1145\/2658996"},{"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":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"ref015","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"ref016","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.14"},{"key":"ref017","unstructured":"B.\u00a0Blanchet, A computationally sound mechanized prover for security protocols, in: 2006 IEEE Symposium on Security and Privacy (S&P 2006), 21\u201324 May 2006, IEEE Computer Society, Berkeley, California, USA, 2006, pp.\u00a0140\u2013154. ISBN 0-7695-2574-1."},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"ref019","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.29"},{"key":"ref020","unstructured":"B.\u00a0Blanchet, B.\u00a0Smyth and V.\u00a0Cheval, Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, 2016."},{"key":"ref021","doi-asserted-by":"publisher","DOI":"10.2478\/popets-2019-0039"},{"key":"ref022","unstructured":"M.\u00a0Brus\u00f3, Dissecting unlinkability, PhD thesis, Ph. D. dissertation, Technische Universiteit Eindhoven, 2014."},{"key":"ref023","doi-asserted-by":"crossref","unstructured":"M.\u00a0Brus\u00f3, K.\u00a0Chatzikokolakis, S.\u00a0Etalle and J.\u00a0Den Hartog, Linking unlinkability, in: International Symposium on Trustworthy Global Computing, Springer, 2012, pp.\u00a0129\u2013144.","DOI":"10.1007\/978-3-642-41157-1_9"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.1145\/2926715"},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"D.\u00a0Chaum, Blind signatures for untraceable payments, in: Advances in Cryptology: Proceedings of CRYPTO \u201982, Plenum Press, 1982, pp.\u00a0199\u2013203.","DOI":"10.1007\/978-1-4757-0602-4_18"},{"key":"ref026","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-34799-2_25"},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cheval, H.\u00a0Comon-Lundh and S.\u00a0Delaune, Trace equivalence decision: Negative tests and non-determinism, in: 18th Conference on Computer and Communications Security (CCS\u201911), ACM, Chicago, Illinois, USA, 2011.","DOI":"10.1145\/2046707.2046744"},{"key":"ref028","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00032"},{"key":"ref029","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Chevalier, R.\u00a0K\u00fcsters, M.\u00a0Rusinowitch and M.\u00a0Turuani, An NP decision procedure for protocol insecurity with XOR, in: LICS, IEEE Computer Society, 2003, pp.\u00a0261\u2013270. ISBN 0-7695-1884-2.","DOI":"10.1109\/LICS.2003.1210066"},{"key":"ref030","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77092-3_37"},{"key":"ref031","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"ref032","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"ref033","unstructured":"S.\u00a0Delaune, M.D.\u00a0Ryan and B.\u00a0Smyth, Automatic verification of privacy properties in the applied pi-calculus, in: Proceedings 2nd Joint ITrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM\u201908), Springer, 2008."},{"key":"ref034","doi-asserted-by":"crossref","unstructured":"J.\u00a0Dreier, C.\u00a0Dum\u00e9nil, S.\u00a0Kremer and R.\u00a0Sasse, Beyond subterm-convergent equational theories in automated verification of stateful protocols, in: Principles of Security and Trust \u2013 6th International Conference, POST 2017, LNCS, Vol.\u00a010204, Springer, 2017, pp.\u00a0117\u2013140.","DOI":"10.1007\/978-3-662-54455-6_6"},{"key":"ref035","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 2018, Oxford, United Kingdom, July 9\u201312, 2018, IEEE Computer Society, 2018, pp.\u00a0359\u2013373.","DOI":"10.1109\/CSF.2018.00033"},{"key":"ref036","doi-asserted-by":"crossref","unstructured":"J.\u00a0Dreier, A.\u00a0Kassem and P.\u00a0Lafourcade, Formal Analysis of E-Cash Protocols, in: SECRYPT 2015 \u2013 Proceedings of the 12th International Conference on Security and Cryptography, SciTePress, 2015, pp.\u00a065\u201375.","DOI":"10.5220\/0005544500650075"},{"key":"ref037","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"ref038","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"ref039","unstructured":"J.D.\u00a0Guttman and J.D.\u00a0Ramsdell, CPSA: A cryptographic protocol shapes analyzer, 2009, http:\/\/hackage.haskell.org\/package\/cpsa."},{"key":"ref040","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.40"},{"key":"ref041","doi-asserted-by":"crossref","unstructured":"L.\u00a0Hirschi, D.\u00a0Baelde and S.\u00a0Delaune, A method for unbounded verification of privacy-type properties,\n                      Journal of Computer Security\n                      (2019), 1\u201366.","DOI":"10.3233\/JCS-171070"},{"key":"ref042","doi-asserted-by":"crossref","unstructured":"I.J.\u00a0Kim, E.Y.\u00a0Choi and D.H.\u00a0Lee, Secure mobile RFID system against privacy and security problems, in: SecPerU 2007, 2007.","DOI":"10.1109\/SECPERU.2007.10"},{"key":"ref043","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160556"},{"key":"ref044","doi-asserted-by":"crossref","unstructured":"R.\u00a0K\u00fcsters and T.\u00a0Truderung, Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach, in: Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, ACM, 2008, pp.\u00a0129\u2013138. ISBN 978-1-59593-810-7.","DOI":"10.1145\/1455770.1455788"},{"key":"ref045","unstructured":"S.\u00a0Lee, T.\u00a0Asano and K.\u00a0Kim, RFID mutual authentication scheme based on synchronized secret information, in: Symposium on Cryptography and Information Security, Hiroshima, Japan, 2006."},{"key":"ref046","doi-asserted-by":"publisher","DOI":"10.1145\/1229285.1229318"},{"key":"ref047","doi-asserted-by":"crossref","unstructured":"G.\u00a0Lowe, Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR, in: TACAS, 1996, pp.\u00a0147\u2013166.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"ref048","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1997.596782"},{"key":"ref049","doi-asserted-by":"crossref","unstructured":"S.\u00a0Meier, B.\u00a0Schmidt, C.J.F.\u00a0Cremers and D.\u00a0Basin, The TAMARIN prover for the symbolic analysis of security protocols, in: CAV, LNCS, Vol.\u00a08044, Springer, 2013, pp.\u00a0696\u2013701.","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref050","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-76481-8_7"},{"key":"ref051","doi-asserted-by":"crossref","unstructured":"J.D.\u00a0Ramsdell, D.J.\u00a0Dougherty, J.D.\u00a0Guttman and P.D.\u00a0Rowe, A hybrid analysis for security protocols with state, in: Proc. 11th International Conference on Integrated Formal Methods (IFM\u201914), LNCS, Vol.\u00a08739, Springer, 2014, pp.\u00a0272\u2013287.","DOI":"10.1007\/978-3-319-10181-1_17"},{"key":"ref052","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 (STM) 2014, Springer, 2014, pp.\u00a0162\u2013177.","DOI":"10.1007\/978-3-319-11851-2_11"},{"key":"ref053","doi-asserted-by":"crossref","unstructured":"R.\u00a0Sasse, S.\u00a0Escobar, C.\u00a0Meadows and J.\u00a0Meseguer, Protocol analysis modulo combination of theories: A case study in maude-NPA, in: STM, 2010, pp.\u00a0163\u2013178.","DOI":"10.1007\/978-3-642-22444-7_11"},{"key":"ref054","unstructured":"B.\u00a0Schmidt, Formal Analysis of Key Exchange Protocols and Physical Protocols, PhD dissertation, ETH, Zurich, 2012."},{"key":"ref055","doi-asserted-by":"crossref","unstructured":"B.\u00a0Schmidt, S.\u00a0Meier, C.J.F.\u00a0Cremers and D.\u00a0Basin, Automated analysis of Diffie\u2013Hellman protocols and advanced security properties, in: Computer Security Foundations Symposium (CSF), IEEE, 2012, pp.\u00a078\u201394.","DOI":"10.1109\/CSF.2012.25"},{"key":"ref056","unstructured":"Tamarin Models for Security Protocols with Exclusive OR, 2019, Accessed: 2019-11-04. https:\/\/github.com\/tamarin-prover\/tamarin-prover\/tree\/develop\/examples\/jcs19-xor."},{"key":"ref057","unstructured":"Tamarin website, Accessed: 2019-10-16, 2019, https:\/\/tamarin-prover.github.io\/."},{"key":"ref058","doi-asserted-by":"crossref","unstructured":"M.\u00a0Turuani, The CL-atse protocol analyser, in: Term Rewriting and Applications, 17th International Conference, RTA 2006, LNCS, Vol.\u00a04098, Springer, 2006, pp.\u00a0277\u2013286. ISBN 3-540-36834-5.","DOI":"10.1007\/11805618_21"},{"key":"ref059","unstructured":"D.\u00a0Unruh,\n                      The impossibility of computationally sound XOR.\n                      , IACR Cryptology ePrint Archive 2010 (2010), 389."},{"key":"ref060","doi-asserted-by":"crossref","unstructured":"T.\u00a0van Deursen, S.\u00a0Mauw, S.\u00a0Radomirovi\u0107 and P.\u00a0Vullers, Secure ownership and ownership transfer in RFID systems, in: Proc. 14th European Symposium on Research in Computer Security (ESORICS\u201909), Lecture Notes in Computer Science, Vol.\u00a05789, Springer, 2009, pp.\u00a0637\u2013654.","DOI":"10.1007\/978-3-642-04444-1_39"},{"key":"ref061","doi-asserted-by":"crossref","unstructured":"T.\u00a0van Deursen and S.\u00a0Radomirovi\u0107, Security of an RFID protocol for supply chains, in: Proc. 1st Workshop on Advances in RFID (AIR\u201908), IEEE Computer Society, 2008, pp.\u00a0568\u2013573.","DOI":"10.1109\/ICEBE.2008.44"},{"key":"ref062","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03944-7_4"},{"key":"ref063","doi-asserted-by":"crossref","unstructured":"T.\u00a0van Deursen and S.\u00a0Radomirovi\u0107, Attacks on RFID Protocols (version 1.1), 2009, http:\/\/eprint.iacr.org\/2008\/310.","DOI":"10.1007\/978-3-540-79966-5_1"},{"key":"ref064","unstructured":"J.\u00a0Yang, J.\u00a0Park, H.\u00a0Lee, K.\u00a0Ren and K.\u00a0Kim, Mutual authentication protocol for low-cost RFID, in: Ecrypt, Graz, Austria, 2005."}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-191358","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-191358","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-191358","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:21Z","timestamp":1777495521000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-191358"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,13]]},"references-count":64,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,2,4]]}},"alternative-id":["10.3233\/JCS-191358"],"URL":"https:\/\/doi.org\/10.3233\/jcs-191358","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,13]]}}}