{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T18:11:22Z","timestamp":1791137482491,"version":"4.1.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:p>We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.<\/jats:p>","DOI":"10.1145\/1452044.1452049","type":"journal-article","created":{"date-parts":[[2008,12,10]],"date-time":"2008-12-10T15:32:31Z","timestamp":1228923151000},"page":"1-61","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":51,"title":["Verified interoperable implementations of security protocols"],"prefix":"10.1145","volume":"31","author":[{"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen","family":"Tse","sequence":"additional","affiliation":[{"name":"University of Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2008,12,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-001-0014-7"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2005.25"},{"key":"e_1_2_1_5_1","unstructured":"Apache Software Foundation 2006. Apache WSS4J. Apache Software Foundation. http:\/\/ws.apache.org\/wss4j\/.  Apache Software Foundation 2006. Apache WSS4J. Apache Software Foundation. http:\/\/ws.apache.org\/wss4j\/."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11555827_12"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/948109.948140"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96717"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1237500.1237504"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455828"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1030083.1030120"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.005"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11841197_6"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'03)","volume":"3188","author":"Bhargavan K.","unstructured":"Bhargavan , K. , Fournet , C. , Gordon , A. D. , and Pucella , R . 2004a. TulaFale: A security tool for Web services . In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'03) . Lecture Notes in Computer Science , vol. 3188 . Springer, 197--222. Bhargavan, K., Fournet, C., Gordon, A. D., and Pucella, R. 2004a. TulaFale: A security tool for Web services. In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'03). Lecture Notes in Computer Science, vol. 3188. Springer, 197--222."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368330"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.32"},{"key":"e_1_2_1_17_1","unstructured":"Bhargavan K. Fournet C. Gordon A. D. and Tse S. 2007a. Verified interoperable implementations of security protocols. In Software System Reliability and Security. IOS Press 87--115.  Bhargavan K. Fournet C. Gordon A. D. and Tse S. 2007a. Verified interoperable implementations of security protocols. In Software System Reliability and Security. IOS Press 87--115."},{"key":"e_1_2_1_18_1","unstructured":"Bhargavan K. Fournet C. Gordon A. D. and Tse S. 2007b. Verified interoperable implementations of security protocols. Tech. rep. MSR-TR-2006-46 Microsoft Research.  Bhargavan K. Fournet C. Gordon A. D. and Tse S. 2007b. Verified interoperable implementations of security protocols. Tech. rep. MSR-TR-2006-46 Microsoft Research."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.16"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.8"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.018"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW'03)","author":"Bodei C.","unstructured":"Bodei , C. , Buchholtz , M. , Degano , P. , and Nielson , F . 2003. Automatic validation of protocol narration . In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW'03) . 126--140. Bodei, C., Buchholtz, M., Degano, P., and Nielson, F. 2003. Automatic validation of protocol narration. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW'03). 126--140."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Eastlake D. Reagle J. Imamura T. Dillaway B. and Simon E. 2002. XML Encryption Syntax and Processing. W3C. W3C Recommendation.  Eastlake D. Reagle J. Imamura T. Dillaway B. and Simon E. 2002. XML Encryption Syntax and Processing. W3C. W3C Recommendation.","DOI":"10.17487\/rfc3075"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Eastlake D. Reagle J. Solo D. Bartel M. Boyer J. Fox B. LaMacchia B. and Simon E. 2002. XML-Signature Syntax and Processing. W3C. W3C Recommendation.  Eastlake D. Reagle J. Solo D. Bartel M. Boyer J. Fox B. LaMacchia B. and Simon E. 2002. XML-Signature Syntax and Processing. W3C. W3C Recommendation.","DOI":"10.17487\/rfc3075"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.01.006"},{"key":"e_1_2_1_28_1","unstructured":"Galois Connections. 2005. Cryptol Reference Manual. Galois Connections.  Galois Connections. 2005. Cryptol Reference Manual. Galois Connections."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.01.002"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/764792.764797"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_24"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the Conference Trusted Global Computing (TGC'05)","volume":"3705","author":"Guttman J. D.","unstructured":"Guttman , J. D. , Herzog , J. C. , Ramsdell , J. D. , and Sniffen , B. T . 2005. Programming cryptographic protocols . In Proceedings of the Conference Trusted Global Computing (TGC'05) . Lecture Notes in Computer Science , vol. 3705 . Springer, 116--145. Guttman, J. D., Herzog, J. C., Ramsdell, J. D., and Sniffen, B. T. 2005. Programming cryptographic protocols. In Proceedings of the Conference Trusted Global Computing (TGC'05). Lecture Notes in Computer Science, vol. 3705. Springer, 116--145."},{"key":"e_1_2_1_33_1","volume-title":"IBM WebSphere Application Server","author":"IBM Corporation","unstructured":"IBM Corporation . 2006. IBM WebSphere Application Server . IBM Corporation . http:\/\/www.ibm.com\/software\/websphere\/. IBM Corporation. 2006. IBM WebSphere Application Server. IBM Corporation. http:\/\/www.ibm.com\/software\/websphere\/."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the Conference Automated Reasoning for Security Protocol Analysis (ARSPA 04)","author":"Kleiner E.","unstructured":"Kleiner , E. and Roscoe , A. W . 2004. Web services security: A preliminary study using Casper and FDR . In Proceedings of the Conference Automated Reasoning for Security Protocol Analysis (ARSPA 04) . Kleiner, E. and Roscoe, A. W. 2004. Web services security: A preliminary study using Casper and FDR. In Proceedings of the Conference Automated Reasoning for Security Protocol Analysis (ARSPA 04)."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the Conference Mathematical Foundations of Programming Semantics (MFPS).","author":"Kleiner E.","unstructured":"Kleiner , E. and Roscoe , A. W . 2005. On the relationship between Web services security and traditional protocols . In Proceedings of the Conference Mathematical Foundations of Programming Semantics (MFPS). Kleiner, E. and Roscoe, A. W. 2005. On the relationship between Web services security and traditional protocols. In Proceedings of the Conference Mathematical Foundations of Programming Semantics (MFPS)."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the Southern African Telecommunication Networks and Applications Conference (SATNAC).","author":"Lukell S.","unstructured":"Lukell , S. , Veldman , C. , and Hutchison , A. C. M. 2003. Automated attack analysis and code generation in a multi-dimensional security protocol engineering framework . In Proceedings of the Southern African Telecommunication Networks and Applications Conference (SATNAC). Lukell, S., Veldman, C., and Hutchison, A. C. M. 2003. Automated attack analysis and code generation in a multi-dimensional security protocol engineering framework. In Proceedings of the Southern African Telecommunication Networks and Applications Conference (SATNAC)."},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the Conference Automata, Languages and Programming (ICALP'98)","volume":"1443","author":"Merro M.","unstructured":"Merro , M. and Sangiorgi , D . 1998. On asynchrony in name-passing calculi . In Proceedings of the Conference Automata, Languages and Programming (ICALP'98) . Lecture Notes in Computer Science , vol. 1443 . Springer, 856--867. Merro, M. and Sangiorgi, D. 1998. On asynchrony in name-passing calculi. In Proceedings of the Conference Automata, Languages and Programming (ICALP'98). Lecture Notes in Computer Science, vol. 1443. Springer, 856--867."},{"key":"e_1_2_1_38_1","volume-title":"Web Services Enhancements (WSE) 2.0","author":"Microsoft Corporation","unstructured":"Microsoft Corporation . 2004. Web Services Enhancements (WSE) 2.0 . Microsoft Corporation . http:\/\/msdn.microsoft.com\/webservices\/building\/wse\/default.aspx. Microsoft Corporation. 2004. Web Services Enhancements (WSE) 2.0. Microsoft Corporation. http:\/\/msdn.microsoft.com\/webservices\/building\/wse\/default.aspx."},{"key":"e_1_2_1_39_1","unstructured":"Microsoft Corporation. 2005. F&num;. Microsoft Corporation. http:\/\/research.microsoft.com\/fsharp\/.  Microsoft Corporation. 2005. F&num;. Microsoft Corporation. http:\/\/research.microsoft.com\/fsharp\/."},{"key":"e_1_2_1_40_1","volume-title":"Windows Communication Foundation (WCF)","author":"Microsoft Corporation","unstructured":"Microsoft Corporation . 2006. Windows Communication Foundation (WCF) . Microsoft Corporation . http:\/\/wcf.netfx3.com\/. Microsoft Corporation. 2006. Windows Communication Foundation (WCF). Microsoft Corporation. http:\/\/wcf.netfx3.com\/."},{"key":"e_1_2_1_41_1","volume-title":"FS2PV: A Cryptographic-Protocol Verifier for F&num;","author":"Microsoft Corporation","unstructured":"Microsoft Corporation . 2007. FS2PV: A Cryptographic-Protocol Verifier for F&num; . Microsoft Corporation . http:\/\/research.microsoft.com\/projects\/samoa\/. Microsoft Corporation. 2007. FS2PV: A Cryptographic-Protocol Verifier for F&num;. Microsoft Corporation. http:\/\/research.microsoft.com\/projects\/samoa\/."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"e_1_2_1_43_1","unstructured":"Milner R. 1999. Communicating and Mobile Systems: The &pi;-Calculus. CUP.   Milner R. 1999. Communicating and Mobile Systems: The &pi;-Calculus. CUP."},{"key":"e_1_2_1_44_1","unstructured":"Muller F. and Millen J. 2001. Cryptographic protocol generation from CAPSL. Tech. rep. SRI-CSL-01-07 SRI.  Muller F. and Millen J. 2001. Cryptographic protocol generation from CAPSL. Tech. rep. SRI-CSL-01-07 SRI."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_2_1_46_1","volume-title":"Web Services Security: SOAP Message Security 1.0 (WS-Security","year":"2004","unstructured":"OASIS 2004. Web Services Security: SOAP Message Security 1.0 (WS-Security 2004 ). OASIS Standard . OASIS 2004. Web Services Security: SOAP Message Security 1.0 (WS-Security 2004). OASIS Standard."},{"key":"e_1_2_1_47_1","volume-title":"Elyjah: A security analyzer for Java implementations of communications protocols. Fourth year project report, Computer Science, Division of Informatics","author":"O'Shea N.","year":"2006","unstructured":"O'Shea , N. 2006 . Elyjah: A security analyzer for Java implementations of communications protocols. Fourth year project report, Computer Science, Division of Informatics , University of Edinburgh. O'Shea, N. 2006. Elyjah: A security analyzer for Java implementations of communications protocols. Fourth year project report, Computer Science, Division of Informatics, University of Edinburgh."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/24592.24594"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Perrig A. Song D. and Phan D. 2001. AGVI -- automatic generation verification and implementation of security protocols. In Proceedings of the 13th Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science. Springer 241--245.   Perrig A. Song D. and Phan D. 2001. AGVI -- automatic generation verification and implementation of security protocols. In Proceedings of the 13th Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science. Springer 241--245.","DOI":"10.1007\/3-540-44585-4_21"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 18th International Conference on Advanced Information Networking and Applications (AINA","volume":"1","author":"Pozza D.","year":"2004","unstructured":"Pozza , D. , Sisto , R. , and Durante , L . 2004. Spi2Java: automatic cryptographic protocol Java code generation from spi calculus . In Proceedings of the 18th International Conference on Advanced Information Networking and Applications (AINA 2004 ). Vol. 1 . 400--405. Pozza, D., Sisto, R., and Durante, L. 2004. Spi2Java: automatic cryptographic protocol Java code generation from spi calculus. In Proceedings of the 18th International Conference on Advanced Information Networking and Applications (AINA 2004). Vol. 1. 400--405."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01)","author":"Sumii E.","unstructured":"Sumii , E. and Pierce , B. C . 2001. Logical relations for encryption . In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01) . 256--269. Sumii, E. and Pierce, B. C. 2001. Logical relations for encryption. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01). 256--269."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_2_1_53_1","unstructured":"W3C 2003. SOAP Version 1.2. W3C. W3C Recommendation.  W3C 2003. SOAP Version 1.2. W3C. W3C Recommendation."},{"key":"e_1_2_1_54_1","unstructured":"W3C 2004. Web Services Addressing (WS-Addressing). W3C. W3C Member Submission.  W3C 2004. Web Services Addressing (WS-Addressing). W3C. W3C Member Submission."},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 178--194","author":"Woo T.","unstructured":"Woo , T. and Lam , S . 1993. A semantic model for authentication protocols . In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 178--194 . Woo, T. and Lam, S. 1993. A semantic model for authentication protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 178--194."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1452044.1452049","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1452044.1452049","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:06Z","timestamp":1750253406000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1452044.1452049"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["10.1145\/1452044.1452049"],"URL":"https:\/\/doi.org\/10.1145\/1452044.1452049","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12]]},"assertion":[{"value":"2007-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}