{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T19:22:31Z","timestamp":1768159351884,"version":"3.49.0"},"reference-count":36,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[2016,8,3]],"date-time":"2016-08-03T00:00:00Z","timestamp":1470182400000},"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":[[2016,11,8]]},"abstract":"<jats:p> Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols \u2013 sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. A notable exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (msr) rules, a formalism expressive enough to encode state. As multiset rewriting is a \u201clow-level\u201d specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process. <\/jats:p><jats:p> We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to msr rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and an optimistic contract signing protocol. <\/jats:p>","DOI":"10.3233\/jcs-160556","type":"journal-article","created":{"date-parts":[[2016,8,5]],"date-time":"2016-08-05T14:51:26Z","timestamp":1470408686000},"page":"583-616","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":37,"title":["Automated analysis of security protocols with global state"],"prefix":"10.1177","volume":"24","author":[{"given":"Steve","family":"Kremer","sequence":"first","affiliation":[{"name":"Inria Nancy \u2013 Grand Est and LORIA, France"}]},{"given":"Robert","family":"K\u00fcnnemann","sequence":"additional","affiliation":[{"name":"CISPA and Saarland University, Germany"}]}],"member":"179","published-online":{"date-parts":[[2016,8,3]]},"reference":[{"key":"ref001","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"ref002","doi-asserted-by":"crossref","unstructured":"M.\u00a0Abadi and C.\u00a0Fournet, Mobile values, new names, and secure communication, in: Proc. 28th ACM Symp. on Principles of Programming Languages (POPL\u201901), ACM Press, 2001, pp.\u00a0104\u2013115.","DOI":"10.1145\/360204.360213"},{"key":"ref003","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":"ref004","doi-asserted-by":"crossref","unstructured":"A.\u00a0Armando, D.A.\u00a0Basin, Y.\u00a0Boichut, Y.\u00a0Chevalier, L.\u00a0Compagna, J.\u00a0Cu\u00e9llar, P.\u00a0Hankes Drielsma, 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: Proc. 17th International Conference on Computer Aided Verification (CAV\u201905), LNCS, Springer, 2005, pp.\u00a0281\u2013285.","DOI":"10.1007\/11513988_27"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"A.\u00a0Armando, R.\u00a0Carbone, L.\u00a0Compagna, J.\u00a0Cuellar and L.\u00a0Tobarra Abad, 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), 2008, pp.\u00a01\u201310. doi:10.1145\/1456396.1456397.","DOI":"10.1145\/1456396.1456397"},{"key":"ref006","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2005-13102"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in: Proc. 14th Computer Security Foundations Workshop (CSFW\u201901), IEEE Press, 2001, pp.\u00a082\u201396.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref008","unstructured":"B.\u00a0Blanchet, B.\u00a0Smyth and V.\u00a0Cheval, ProVerif 1.88: Automatic cryptographic protocol verifier, user manual and tutorial, 2013."},{"key":"ref009","doi-asserted-by":"publisher","DOI":"10.1109\/2.955101"},{"key":"ref010","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bortolozzo, M.\u00a0Centenaro, R.\u00a0Focardi and G.\u00a0Steel, Attacking and fixing PKCS#11 security tokens, in: Proc. 17th ACM Conference on Computer and Communications Security (CCS\u201910), ACM Press, 2010, pp.\u00a0260\u2013269. doi:10.1145\/1866307.1866337.","DOI":"10.1145\/1866307.1866337"},{"key":"ref011","unstructured":"CCA Basic Services Reference and Guide. CCA Basic Services Reference and Guide, October 2006, available online."},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"S.\u00a0Delaune, S.\u00a0Kremer, M.D.\u00a0Ryan and G.\u00a0Steel, Formal analysis of protocols based on TPM state registers, in: Proc. 24th IEEE Computer Security Foundations Symposium (CSF\u201911), IEEE Press, 2011, pp.\u00a066\u201382.","DOI":"10.1109\/CSF.2011.12"},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"S.\u00a0Delaune, S.\u00a0Kremer and G.\u00a0Steel, Formal analysis of PKCS#11 and proprietary extensions, Journal of Computer Security 18(6) (2010), http:\/\/www.lsv.ens-cachan.fr\/Publis\/PAPERS\/PDF\/DKS-jcs09.pdf. doi:10.3233\/JCS-2009-0394.","DOI":"10.3233\/JCS-2009-0394"},{"key":"ref014","doi-asserted-by":"crossref","unstructured":"S.\u00a0Escobar, C.\u00a0Meadows and J.\u00a0Meseguer, Maude-npa: Cryptographic protocol analysis modulo equational properties, in: Foundations of Security Analysis and Design V, LNCS, Vol.\u00a05705, Springer, 2009, pp.\u00a01\u201350. doi:10.1007\/978-3-642-03829-7_1.","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"S.B.\u00a0Fr\u00f6schle and N.\u00a0Sommer, Reasoning with past to prove PKCS#11 keys secure, in: Proc. 7th International Workshop on Formal Aspects in Security and Trust (FAST\u201910), LNCS, Vol.\u00a06561, 2010, pp.\u00a096\u2013110. doi:10.1007\/978-3-642-19751-2_7.","DOI":"10.1007\/978-3-642-19751-2_7"},{"key":"ref016","doi-asserted-by":"crossref","unstructured":"J.A.\u00a0Garay, M.\u00a0Jakobsson and P.D.\u00a0MacKenzie, Abuse-free optimistic contract signing, in: Advances in Cryptology\u00a0\u2013 Crypto\u201999, LNCS, Vol.\u00a01666, Springer, 1999, pp.\u00a0449\u2013466. doi:10.1007\/3-540-48405-1_29.","DOI":"10.1007\/3-540-48405-1_29"},{"key":"ref017","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9202-1"},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2006.85"},{"key":"ref019","unstructured":"I.\u00a0Rakotonirina, V\u00e9rification automatique de protocoles de s\u00e9curit\u00e9 avec m\u00e9moire globale et boucles, Intership report, September 2014, URL http:\/\/www.dptinfo.ens-cachan.fr\/~irakoton\/stagel3\/rapportl3.pdf."},{"key":"ref020","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1999-72-304"},{"key":"ref021","doi-asserted-by":"crossref","unstructured":"S.\u00a0Kremer and R.\u00a0K\u00fcnnemann, Automated analysis of security protocols with global state, in: Proc. 35th IEEE Symposium on Security and Privacy (S&P\u201914), IEEE Computer Society Press, 2014, pp.\u00a0163\u2013178. doi:10.1109\/SP.2014.18.","DOI":"10.1109\/SP.2014.18"},{"key":"ref022","doi-asserted-by":"crossref","unstructured":"R.\u00a0K\u00fcnnemann, Automated backward analysis of PKCS#11 v2.20, in: Proc. 4th Conference on Principles of Security and Trust (POST\u201915), LNCS, Vol.\u00a09036, Springer, 2015, pp.\u00a0219\u2013238.","DOI":"10.1007\/978-3-662-46666-7_12"},{"key":"ref023","doi-asserted-by":"crossref","unstructured":"R.\u00a0K\u00fcnnemann and G.\u00a0Steel, YubiSecure? Formal security analysis results for the Yubikey and YubiHSM, in: Proc. 8th Workshop on Security and Trust Management (STM\u201912), LNCS, Vol.\u00a07783, 2012, pp.\u00a0257\u2013272. doi:10.1007\/978-3-642-38004-4_17.","DOI":"10.1007\/978-3-642-38004-4_17"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.1016\/0167-4048(92)90222-D"},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"G.\u00a0Lowe, Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR, in: Proc. 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201996), LNCS, Vol.\u00a01055, Springer, 1996, pp.\u00a0147\u2013166. doi:10.1007\/3-540-61042-1_43.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"S.\u00a0M\u00f6dersheim, Abstraction by set-membership: Verifying security protocols and web services with databases, in: Proc. 17th ACM Conference on Computer and Communications Security (CCS\u201910), ACM, 2010, pp.\u00a0351\u2013360. doi:10.1145\/1866307.1866348.","DOI":"10.1145\/1866307.1866348"},{"key":"ref027","unstructured":"PKCS #11: Cryptographic token interface standard, RSA Security Inc., v2.20, June 2004."},{"key":"ref028","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.","DOI":"10.1007\/978-3-319-10181-1_17"},{"key":"ref029","unstructured":"B.\u00a0Schmidt, Formal analysis of key-exchange protocols and physical protocols, PhD thesis, ETH Z\u00fcrich, 2012."},{"key":"ref030","doi-asserted-by":"crossref","unstructured":"B.\u00a0Schmidt, S.\u00a0Meier, C.\u00a0Cremers and D.\u00a0Basin, Automated analysis of Diffie\u2013Hellman protocols and advanced security properties, in: Proc. 25th IEEE Computer Security Foundations Symposium (CSF\u201912), IEEE Press, 2012, pp.\u00a078\u201394.","DOI":"10.1109\/CSF.2012.25"},{"key":"ref031","doi-asserted-by":"crossref","unstructured":"B.\u00a0Schmidt, S.\u00a0Meier, 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":"ref032","doi-asserted-by":"crossref","unstructured":"B.\u00a0Schmidt, R.\u00a0Sasse, C.\u00a0Cremers and D.A.\u00a0Basin, Automated verification of group key agreement protocols, in: Proc. 35th IEEE Symposium on Security and Privacy (S&P\u201914), IEEE Computer Society Press, 2014, pp.\u00a0179\u2013194. doi:10.1109\/SP.2014.19.","DOI":"10.1109\/SP.2014.19"},{"key":"ref033","doi-asserted-by":"crossref","unstructured":"J.\u00a0Shao, Y.\u00a0Qin, D.\u00a0Feng and W.\u00a0Wang, Formal analysis of enhanced authorization in the TPM 2.0, in: Proc. 10th ACM Symposium on Information, Computer and Communications Security (ASIA CCS\u201915), ACM, 2015, pp.\u00a0273\u2013284.","DOI":"10.1145\/2714576.2714610"},{"key":"ref034","unstructured":"The YubiKey Manual \u2013 Usage, configuration and introduction of basic concepts (Version 2.2), available at: http:\/\/www.yubico.com\/documentation. Yubico AB, Kungsgatan 37, 111 56 Stockholm Sweden, June 2010."},{"key":"ref035","unstructured":"Trusted Computing Group, TPM specification version 1.2. Parts 1\u20133, revision 103, 2007, available at: http:\/\/www.trustedcomputinggroup.org\/resources\/tpm_main_specification."},{"key":"ref036","unstructured":"Yubico AB, Yubico customer list, 2014, URL https:\/\/www.yubico.com\/about\/reference-customers\/, accessed: Do 13 November 2014, 08:33:34 CET."}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-160556","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-160556","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-160556","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,10]],"date-time":"2025-03-10T15:48:40Z","timestamp":1741621720000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-160556"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,3]]},"references-count":36,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,11,8]]}},"alternative-id":["10.3233\/JCS-160556"],"URL":"https:\/\/doi.org\/10.3233\/jcs-160556","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,8,3]]}}}