{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T11:31:26Z","timestamp":1770809486647,"version":"3.50.0"},"reference-count":65,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"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":[[2017,11,30]]},"abstract":"<jats:p> We propose a development method for security protocols based on stepwise refinement. Our refinement strategy transforms abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style intruder. As intermediate levels of abstraction, we employ messageless guard protocols and channel protocols communicating over channels with security properties. These abstractions provide insights on why protocols are secure and foster the development of families of protocols sharing common structure and properties. We have implemented our method in Isabelle\/HOL and used it to develop different entity authentication and key establishment protocols, including realistic features such as key confirmation, replay caches, and encrypted tickets. Our development highlights that guard protocols and channel protocols provide fundamental abstractions for bridging the gap between security properties and standard protocol descriptions based on cryptographic messages. It also shows that our refinement approach scales to protocols of nontrivial size and complexity. <\/jats:p>","DOI":"10.3233\/jcs-16814","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T16:16:30Z","timestamp":1507911390000},"page":"71-120","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":6,"title":["Refining security protocols"],"prefix":"10.1177","volume":"26","author":[{"given":"Christoph","family":"Sprenger","sequence":"first","affiliation":[{"name":"Institute of Information Security, Department of Computer Science, ETH Zurich, Switzerland"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"Institute of Information Security, Department of Computer Science, ETH Zurich, Switzerland"}]}],"member":"179","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"ref001","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3086"},{"key":"ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref003","doi-asserted-by":"crossref","unstructured":"J.R.\u00a0Abrial, Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010. doi:10.1017\/CBO9781139195881.","DOI":"10.1017\/CBO9781139195881"},{"issue":"1","key":"ref004","first-page":"1","volume":"77","author":"Abrial J.-R.","year":"2007","journal-title":"Fundam. Inform."},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"R.\u00a0Alur, P.\u00a0Cern\u00fd and S.\u00a0Zdancewic, Preserving secrecy under refinement, in: Proc. 33rd International Colloquium on Automata, Languages and Programming (ICALP), M.\u00a0Bugliesi, B.\u00a0Preneel, V.\u00a0Sassone and I.\u00a0Wegener, eds, Lecture Notes in Computer Science, Vol.\u00a04052, 2006, pp.\u00a0107\u2013118.","DOI":"10.1007\/11787006_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, K.Etessami and S.K.Rajamani, eds, Lecture Notes in Computer Science, Vol.\u00a03576, Springer, 2005, pp.\u00a0281\u2013285.","DOI":"10.1007\/11513988_27"},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.05.002"},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.1145\/2658996"},{"key":"ref009","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-130472"},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2013.162"},{"key":"ref011","doi-asserted-by":"crossref","unstructured":"G.\u00a0Bella, Formal Correctness of Security Protocols, Information Security and Cryptography, Springer, 2007. doi:10.1007\/978-3-540-68136-6.","DOI":"10.1007\/978-3-540-68136-6"},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"G.\u00a0Bella, C.\u00a0Longo and L.C.\u00a0Paulson, Verifying second-level security protocols, in: TPHOLs, D.A.Basin and B.Wolff, eds, Lecture Notes in Computer Science, Vol.\u00a02758, Springer, 2003, pp.\u00a0352\u2013366.","DOI":"10.1007\/10930755_23"},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"G.\u00a0Bella and L.C.\u00a0Paulson, Kerberos version 4: Inductive analysis of the secrecy goals, in: Proc. 5th European Symposium on Research in Computer Security (ESORICS), 1998, pp.\u00a0361\u2013375.","DOI":"10.1007\/BFb0055875"},{"key":"ref014","doi-asserted-by":"crossref","unstructured":"G.\u00a0Bella and L.C.\u00a0Paulson, Mechanising BAN Kerberos by the inductive method, in: CAV, A.J.Hu and M.Y.Vardi, eds, Lecture Notes in Computer Science, Vol.\u00a01427, Springer, 1998, pp.\u00a0416\u2013427.","DOI":"10.1007\/BFb0028763"},{"issue":"12","key":"ref015","first-page":"1337","volume":"3","author":"Bella G.","year":"1997","journal-title":"Journal of Universal Computer Science"},{"key":"ref016","unstructured":"N.\u00a0Bena\u00efssa, La composition des protocoles de s\u00e9curit\u00e9 avec la m\u00e9thode B \u00e9v\u00e9nementielle, PhD thesis, Universit\u00e9 Henri Poincar\u00e9 \u2013 Nancy I, France, 2010, (in French)."},{"key":"ref017","doi-asserted-by":"crossref","unstructured":"P.\u00a0Bieber and N.\u00a0Boulahia-Cuppens, Formal development of authentication protocols, in: Sixth BCS-FACS Refinement Workshop, 1994.","DOI":"10.1007\/978-1-4471-3240-0_5"},{"key":"ref018","doi-asserted-by":"crossref","unstructured":"P.\u00a0Bieber, N.\u00a0Boulahia-Cuppens, T.\u00a0Lehmann and E.\u00a0van Wickeren, Abstract machines for communication security, in: Proc. 6th IEEE Computer Security Foundations Workshop (CSFW), 1993, pp.\u00a0137\u2013146.","DOI":"10.1109\/CSFW.1993.246632"},{"key":"ref019","doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: CSFW, IEEE Computer Society, Los Alamitos, CA, 2001, pp.\u00a082\u201396.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref020","doi-asserted-by":"publisher","DOI":"10.1109\/49.223872"},{"key":"ref021","doi-asserted-by":"crossref","unstructured":"A.D.\u00a0Brucker and S.\u00a0M\u00f6dersheim, Integrating automated and interactive protocol verification, in: Formal Aspects in Security and Trust \u2013 6th International Workshop, FAST 2009: Revised Selected Papers Eindhoven, The Netherlands, November 5\u20136, 2009, P.Degano and J.D.Guttman, eds, Lecture Notes in Computer Science, Vol.\u00a05983, Springer, 2009, pp.\u00a0248\u2013262.","DOI":"10.1007\/978-3-642-12459-4_18"},{"key":"ref022","unstructured":"F.\u00a0Butler, I.\u00a0Cervesato, A.D.\u00a0Jaggard and A.\u00a0Scedrov, A formal analysis of some properties of Kerberos 5 using MSR, in: Proc. 15th IEEE Computer Security Foundations Workshop (CSFW), IEEE Computer Society, Los Alamitos, CA, 2002, pp.\u00a0175\u2013192."},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.040"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200025"},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"R.\u00a0Canetti, Universally composable security: A new paradigm for cryptographic protocols, in: FOCS, 2001, pp.\u00a0136\u2013145.","DOI":"10.1109\/SFCS.2001.959888"},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"I.\u00a0Cervesato, C.\u00a0Meadows and D.\u00a0Pavlovic, An encapsulated authentication logic for reasoning about key distribution protocols, in: CSFW \u201905: Proceedings of the 18th IEEE Workshop on Computer Security Foundations, Washington, DC, USA, 2005, pp.\u00a048\u201361. doi:10.1109\/CSFW.2005.7.","DOI":"10.1109\/CSFW.2005.7"},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cortier, M.\u00a0Rusinowitch and E.\u00a0Zalinescu, Relating two standard notions of secrecy, Logical Methods in Computer Science 3(3) (2007). doi:10.2168\/LMCS-3(3:2)2007.","DOI":"10.2168\/LMCS-3(3:2)2007"},{"key":"ref028","doi-asserted-by":"crossref","unstructured":"C.J.F.\u00a0Cremers, The Scyther tool: Verification, falsification, and analysis of security protocols, in: CAV, A.Gupta and S.Malik, eds, Lecture Notes in Computer Science, Vol.\u00a05123, Springer, 2008, pp.\u00a0414\u2013418.","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"ref029","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2005-13304"},{"key":"ref030","unstructured":"S.\u00a0Delaune, S.\u00a0Kremer and O.\u00a0Pereira, Simulation based security in the applied pi calculus, in: FSTTCS, R.Kannan and K.N.Kumar, eds, LIPIcs, Vol.\u00a04, Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik, 2009, pp.\u00a0169\u2013180."},{"key":"ref031","doi-asserted-by":"publisher","DOI":"10.1145\/358722.358740"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"T.\u00a0Gross and S.\u00a0M\u00f6dersheim, Vertical protocol composition, in: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, June 27\u201329, 2011, IEEE Computer Society, Los Alamitos, CA, 2011, pp.\u00a0235\u2013250. doi:10.1109\/CSF.2011.23.","DOI":"10.1109\/CSF.2011.23"},{"key":"ref033","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140499"},{"key":"ref034","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2001-91-202"},{"key":"ref035","unstructured":"ISO, Information technology \u2013 Security techniques \u2013 Entity authentication mechanisms \u2013 Part 3: Entity authentication using a public-Key algorithm ISO\/IEC 9798-3, International Standard, 2nd edn, 1998."},{"key":"ref036","doi-asserted-by":"crossref","unstructured":"J.\u00a0J\u00fcrjens, Secrecy-preserving refinement, in: Proc. 10th Symposium on Formal Methods Europe (FME 2001), Lecture Notes in Computer Science, Vol.\u00a02021, Springer, 2001, pp.\u00a0135\u2013152.","DOI":"10.1007\/3-540-45251-6_8"},{"key":"ref037","doi-asserted-by":"crossref","unstructured":"A.\u00a0Kamil and G.\u00a0Lowe, Understanding abstractions of secure channels, in: Formal Aspects of Security and Trust \u2013 7th International Workshop, FAST 2010: Revised Selected Papers, Pisa, Italy, September 16\u201317, 2010, Lecture Notes in Computer Science, Vol.\u00a06561, Springer 2010, pp.\u00a050\u201364. doi:10.1007\/978-3-642-19751-2_4.","DOI":"10.1007\/978-3-642-19751-2_4"},{"key":"ref038","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2011-0429"},{"key":"ref039","doi-asserted-by":"crossref","unstructured":"J.\u00a0Lallemand, D.A.\u00a0Basin and C.\u00a0Sprenger, Refining authenticated key agreement with strong adversaries, in: 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26\u201328, 2017, IEEE, 2017, pp.\u00a092\u2013107. doi:10.1109\/EuroSP.2017.22.","DOI":"10.1109\/EuroSP.2017.22"},{"key":"ref040","first-page":"93","volume":"17","author":"Lowe G.","year":"1996","journal-title":"Software \u2013 Concepts and Tools"},{"key":"ref041","doi-asserted-by":"crossref","unstructured":"G.\u00a0Lowe, A hierarchy of authentication specifications, in: IEEE Computer Security Foundations Workshop, IEEE Computer Society, Los Alamitos, CA, 1997, pp.\u00a031\u201343. doi:10.1109\/CSFW.1997.596782.","DOI":"10.1109\/CSFW.1997.596782"},{"key":"ref042","doi-asserted-by":"crossref","unstructured":"N.A.\u00a0Lynch, I\/O automaton models and proofs for shared-key communication systems, in: Proc. 12th IEEE Computer Security Foundations Workshop (CSFW), 1999, pp.\u00a014\u201329.","DOI":"10.1109\/CSFW.1999.779759"},{"key":"ref043","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"ref044","doi-asserted-by":"crossref","unstructured":"H.\u00a0Mantel, Preserving information flow properties under refinement, in: Proc. 22nd IEEE Symposium on Security & Privacy, 2001, pp.\u00a078\u201391. doi:10.1109\/SECPRI.2001.924289.","DOI":"10.1109\/SECPRI.2001.924289"},{"key":"ref045","doi-asserted-by":"crossref","unstructured":"U.M.\u00a0Maurer and P.E.\u00a0Schmid, A calculus for secure channel establishment in open networks, in: Proc. 9th European Symposium on Research in Computer Security (ESORICS), 1994, pp.\u00a0175\u2013192.","DOI":"10.1007\/3-540-58618-0_63"},{"key":"ref046","doi-asserted-by":"crossref","unstructured":"A.\u00a0McIver and C.C.\u00a0Morgan, Sums and lovers: Case studies in security, compositionality and refinement, in: FM 2009: Formal Methods, Second World Congress: Proceedings, Eindhoven, The Netherlands, November 2\u20136, 2009, Springer, 2009, pp.\u00a0289\u2013304.","DOI":"10.1007\/978-3-642-05089-3_19"},{"key":"ref047","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2012-0455"},{"key":"ref048","unstructured":"R.\u00a0Milner, An algebraic definition of simulation between programs, in: IJCAI, 1971, pp.\u00a0481\u2013489."},{"key":"ref049","doi-asserted-by":"crossref","unstructured":"S.\u00a0M\u00f6dersheim and L.\u00a0Vigan\u00f2, Secure pseudonymous channels, in: Proc. 14th European Symposium on Research in Computer Security (ESORICS), M.\u00a0Backes and P.\u00a0Ning, eds, Lecture Notes in Computer Science, Vol.\u00a05789, Springer, 2009, pp.\u00a0337\u2013354.","DOI":"10.1007\/978-3-642-04444-1_21"},{"key":"ref050","doi-asserted-by":"crossref","unstructured":"S.\u00a0M\u00f6dersheim and L.\u00a0Vigan\u00f2, Sufficient conditions for vertical composition of security protocols, in: 9th ACM Symposium on Information, Computer and Communications Security, ASIA CCS \u201914, Kyoto, Japan, June 3\u20136, 2014, S.Moriai, T.Jaeger and K.Sakurai, eds, ACM, 2014, pp.\u00a0435\u2013446. doi:10.1145\/2590296.2590330.","DOI":"10.1145\/2590296.2590330"},{"key":"ref051","doi-asserted-by":"crossref","unstructured":"C.\u00a0Morgan, The shadow knows: Refinement of ignorance in sequential programs, in: Mathematics of Program Construction, 8th International Conference, MPC 2006: Proceedings, Kuressaare, Estonia, July 3\u20135, 2006, Lecture Notes in Computer Science, Vol.\u00a04014, Springer, 2006, pp.\u00a0359\u2013378.","DOI":"10.1007\/11783596_21"},{"key":"ref052","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.003"},{"key":"ref053","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"ref054","doi-asserted-by":"publisher","DOI":"10.1109\/35.312841"},{"key":"ref055","doi-asserted-by":"crossref","unstructured":"B.T.\u00a0Nguyen and C.\u00a0Sprenger, Sound security protocol transformations, in: Principles of Security and Trust \u2013 Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013: Proceedings, Rome, Italy, March 16\u201324, 2013, D.A.Basin and J.C.Mitchell, eds, Lecture Notes in Computer Science, Vol.\u00a07796, Springer, 2013, pp.\u00a083\u2013104. doi:10.1007\/978-3-642-36830-1_5.","DOI":"10.1007\/978-3-642-36830-1_5"},{"key":"ref056","doi-asserted-by":"crossref","unstructured":"B.T.\u00a0Nguyen and C.\u00a0Sprenger, Abstractions for security protocol verification, in: Principles of Security and Trust \u2013 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015: Proceedings, London, UK, April 11\u201318, 2015, R.Focardi and A.C.Myers, eds, Lecture Notes in Computer Science, Vol.\u00a09036, Springer, 2015, pp.\u00a0196\u2013215. doi:10.1007\/978-3-662-46666-7_11.","DOI":"10.1007\/978-3-662-46666-7_11"},{"key":"ref057","doi-asserted-by":"crossref","unstructured":"T.\u00a0Nipkow, L.C.\u00a0Paulson and M.\u00a0Wenzel, Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, Vol.\u00a02283, Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"ref058","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"ref059","doi-asserted-by":"crossref","unstructured":"D.\u00a0Pavlovic and C.\u00a0Meadows, Deriving secrecy in key establishment protocols, in: Proc. 11th European Symposium on Research in Computer Security (ESORICS), 2006, pp.\u00a0384\u2013403.","DOI":"10.1007\/11863908_24"},{"key":"ref060","doi-asserted-by":"crossref","unstructured":"N.\u00a0Polikarpova and M.\u00a0Moskal, Verifying implementations of security protocols by refinement, in: VSTTE, R.Joshi, P.\u00a0M\u00fcller and A.Podelski, eds, Lecture Notes in Computer Science, Vol.\u00a07152, Springer, 2012, pp.\u00a050\u201365.","DOI":"10.1007\/978-3-642-27705-4_5"},{"key":"ref061","doi-asserted-by":"crossref","unstructured":"B.\u00a0Schmidt, S.\u00a0Meier, C.J.F.\u00a0Cremers and D.A.\u00a0Basin, Automated analysis of Diffie-Hellman protocols and advanced security properties, in: 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25\u201327, 2012, IEEE Computer Society, Los Alamitos, CA, 2012, pp.\u00a078\u201394. doi:10.1109\/CSF.2012.25.","DOI":"10.1109\/CSF.2012.25"},{"key":"ref062","doi-asserted-by":"crossref","unstructured":"C.\u00a0Sprenger and D.\u00a0Basin, Developing security protocols by refinement, in: Proc. 17th ACM Conference on Computer and Communications Security (CCS), Chicago, IL, USA, October 4\u20138, 2010, ACM, 2010, pp.\u00a0361\u2013374. doi:10.1145\/1866307.1866349.","DOI":"10.1145\/1866307.1866349"},{"key":"ref063","doi-asserted-by":"crossref","unstructured":"C.\u00a0Sprenger and D.A.\u00a0Basin, Refining key establishment, in: 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25\u201327, 2012, IEEE Computer Society, Los Alamitos, CA, 2012, pp.\u00a0230\u2013246. doi:10.1109\/CSF.2012.21.","DOI":"10.1109\/CSF.2012.21"},{"key":"ref064","unstructured":"C.\u00a0Sprenger and I.\u00a0Somaini, Developing security protocols by refinement, Archive of Formal Proofs (2017), https:\/\/www.isa-afp.org\/entries\/Security_Protocol_Refinement.shtml."},{"key":"ref065","unstructured":"J.G.\u00a0Steiner, B.C.\u00a0Neuman and J.I.\u00a0Schiller, Kerberos: An authentication service for open network systems, in: Winter 1988 Usenix Conference, 1988."}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-16814","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-16814","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-16814","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T05:57:36Z","timestamp":1741672656000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-16814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":65,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,11,30]]}},"alternative-id":["10.3233\/JCS-16814"],"URL":"https:\/\/doi.org\/10.3233\/jcs-16814","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,12]]}}}