{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:40:30Z","timestamp":1774946430422,"version":"3.50.1"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/E044956\/1"],"award-info":[{"award-number":["EP\/E044956\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:p>\n            We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a \u03bb-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general-purpose functional language F\n            <jats:sup>#<\/jats:sup>\n            ; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.\n          <\/jats:p>","DOI":"10.1145\/1890028.1890031","type":"journal-article","created":{"date-parts":[[2011,2,8]],"date-time":"2011-02-08T13:21:01Z","timestamp":1297171261000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":105,"title":["Refinement types for secure implementations"],"prefix":"10.1145","volume":"33","author":[{"given":"Jesper","family":"Bengtson","sequence":"first","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]},{"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[{"name":"Microsoft Research, United Kingdom"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, United Kingdom"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Microsoft Research, United Kingdom"}]},{"given":"Sergio","family":"Maffeis","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2011,2,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/324133.324266"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.002"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1044731.1044735"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155225"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS'03)","author":"Abadi M.","unstructured":"Abadi , M. and Fournet , C . 2003. Access control based on execution history . In Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS'03) . Internet Society. Abadi, M. and Fournet, C. 2003. Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS'03). Internet Society."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.481513"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_23"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11555827_12"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00175-4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866351"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481866"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.27"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Bengtson J. Bhargavan K. Fournet C. Gordon A. D. and Maffeis S. 2010. Refinement types for secure implementations. Tech. rep. MSR--TR--2008--118 Microsoft Research.  Bengtson J. Bhargavan K. Fournet C. Gordon A. D. and Maffeis S. 2010. Refinement types for secure implementations. Tech. rep. MSR--TR--2008--118 Microsoft Research.","DOI":"10.1109\/CSF.2008.27"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.26"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455828"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706350"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS'10)","author":"Bhargavan K.","unstructured":"Bhargavan , K. , Fournet , C. , and Guts , N . 2010b. Typechecking higher-order security libraries . In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS'10) . 47--62. Bhargavan, K., Fournet, C., and Guts, N. 2010b. Typechecking higher-order security libraries. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS'10). 47--62."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Borgstr\u00f6m J. Gordon A. D. and Pucella R. 2010. Roles stacks histories: A triple for Hoare. J. Function. Program. Cambridge University Press.  Borgstr\u00f6m J. Gordon A. D. and Pucella R. 2010. Roles stacks histories: A triple for Hoare. J. Function. Program. Cambridge University Press.","DOI":"10.1007\/978-1-84882-912-1_4"},{"key":"e_1_2_1_28_1","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Logic and Functional Programming","author":"Cardelli L.","unstructured":"Cardelli , L. 1986. Typechecking dependent types and subtypes . In Foundations of Logic and Functional Programming . Lecture Notes in Computer Science , vol. 306 . Springer , 45--57. Cardelli, L. 1986. Typechecking dependent types and subtypes. In Foundations of Logic and Functional Programming. Lecture Notes in Computer Science, vol. 306. Springer, 45--57."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.20"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.19"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"e_1_2_1_33_1","unstructured":"Constable R. Allen S. Bromley H. Cleaveland W. Cremer J. Harper R. Howe D. Knoblock T. Mendler N. Panangaden P. et al. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall.   Constable R. Allen S. Bromley H. Cleaveland W. Cremer J. Harper R. Howe D. Knoblock T. Mendler N. Panangaden P. et al. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall."},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Links: Web Programming Without Tiers. In Proceedings of 5th International Symposium on Formal Methods for Components and Objects (FMCO)","author":"Cooper E.","year":"2006","unstructured":"Cooper , E. , Lindley , S. , Wadler , P. , and Yallop , J . 2006 . Links: Web Programming Without Tiers. In Proceedings of 5th International Symposium on Formal Methods for Components and Objects (FMCO) . Lecture Notes in Computer Science . Springer-Verlag . Cooper, E., Lindley, S., Wadler, P., and Yallop, J. 2006. Links: Web Programming Without Tiers. In Proceedings of 5th International Symposium on Formal Methods for Components and Objects (FMCO). Lecture Notes in Computer Science. Springer-Verlag."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.012"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)","volume":"4963","author":"de Moura L.","unstructured":"de Moura , L. and Bj\u00f8rner , N . 2008. Z3: An efficient SMT solver . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08) . Lecture Notes in Computer Science , vol. 4963 . Springer, 337--340. de Moura, L. and Bj\u00f8rner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08). Lecture Notes in Computer Science, vol. 4963. Springer, 337--340."},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy.","author":"Dean D.","unstructured":"Dean , D. , Felten , E. , and Wallach , D . 1996. Java security: From HotJava to Netscape and beyond . In Proceedings of the IEEE Symposium on Security and Privacy. Dean, D., Felten, E., and Wallach, D. 1996. Java security: From HotJava to Netscape and beyond. In Proceedings of the IEEE Symposium on Security and Privacy."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_42_1","volume-title":"Elements of Intuitionism","author":"Dummett M. A. E.","unstructured":"Dummett , M. A. E. 1977. Elements of Intuitionism . Clarendon Press . Dummett, M. A. E. 1977. Elements of Intuitionism. Clarendon Press."},{"key":"e_1_2_1_43_1","first-page":"677","article-title":"A compositional logic for proving security properties of protocols","volume":"11","author":"Durgin N.","year":"2003","unstructured":"Durgin , N. , Mitchell , J. C. , and Pavlovic , D. 2003 . A compositional logic for proving security properties of protocols . J. Comput. Secur. (Special Issue of Selected Papers from CSFW-14) 11 , 4, 677 -- 721 . Durgin, N., Mitchell, J. C., and Pavlovic, D. 2003. A compositional logic for proving security properties of protocols. J. Comput. Secur. (Special Issue of Selected Papers from CSFW-14) 11, 4, 677--721.","journal-title":"J. Comput. Secur. (Special Issue of Selected Papers from CSFW-14)"},{"key":"e_1_2_1_44_1","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 Recommendation. http:\/\/www.w3.org\/TR\/2002\/REC-xmldsig-core-20020212\/.   Eastlake D. Reagle J. Solo D. Bartel M. Boyer J. Fox B. LaMacchia B. and Simon E. 2002. XML-signature syntax and processing. W3C Recommendation. http:\/\/www.w3.org\/TR\/2002\/REC-xmldsig-core-20020212\/."},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the International Conference on Formal Engineering Methods (ICFEM'04)","volume":"3308","author":"Filli\u00e2tre J.","unstructured":"Filli\u00e2tre , J. and March\u00e9 , C . 2004. Multi-prover Verification of C Programs . In Proceedings of the International Conference on Formal Engineering Methods (ICFEM'04) . Lecture Notes in Computer Science , vol. 3308 . Springer, 15--29. Filli\u00e2tre, J. and March\u00e9, C. 2004. Multi-prover Verification of C Programs. In Proceedings of the International Conference on Formal Engineering Methods (ICFEM'04). Lecture Notes in Computer Science, vol. 3308. Springer, 15--29."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512558"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the Workshop on Formal and Computational Cryptography (FCC'09)","author":"Fournet C.","year":"2009","unstructured":"Fournet , C. 2009 . On the computational soundness of cryptographic verification by typing . In Proceedings of the Workshop on Formal and Computational Cryptography (FCC'09) . Fournet, C. 2009. On the computational soundness of cryptographic verification by typing. In Proceedings of the Workshop on Formal and Computational Cryptography (FCC'09)."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275500"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.7"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328478"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the Conference on Higher Order Logic Theorem Proving and its Applications, J. J. Joyce and C.-J","author":"Gordon A. D.","unstructured":"Gordon , A. D. 1994. A mechanisation of name-carrying syntax up to alpha-conversion . In Proceedings of the Conference on Higher Order Logic Theorem Proving and its Applications, J. J. Joyce and C.-J . H. Seger, Eds. Lecture Notes in Computer Science, vol. 780 . Springer , 414--426. Gordon, A. D. 1994. A mechanisation of name-carrying syntax up to alpha-conversion. In Proceedings of the Conference on Higher Order Logic Theorem Proving and its Applications, J. J. Joyce and C.-J. H. Seger, Eds. Lecture Notes in Computer Science, vol. 780. Springer, 414--426."},{"key":"e_1_2_1_53_1","volume-title":"Logics and Languages for Reliability and Security: Proceedings of the NATO Summer School Marktoberdorf, J. Esparza, B. Spanfelner, and O. Grumberg, Eds., IOS Press, 73--104","author":"Gordon A. D.","unstructured":"Gordon , A. D. and Fournet , C . 2010. Principles and applications of refinement types . In Logics and Languages for Reliability and Security: Proceedings of the NATO Summer School Marktoberdorf, J. Esparza, B. Spanfelner, and O. Grumberg, Eds., IOS Press, 73--104 . Gordon, A. D. and Fournet, C. 2010. Principles and applications of refinement types. In Logics and Languages for Reliability and Security: Proceedings of the NATO Summer School Marktoberdorf, J. Esparza, B. Spanfelner, and O. Grumberg, Eds., IOS Press, 73--104."},{"key":"e_1_2_1_54_1","volume-title":"Cryptyc: Cryptographic protocol type checker","author":"Gordon A. D.","year":"2002","unstructured":"Gordon , A. D. and Jeffrey , A. S. A . 2002 . Cryptyc: Cryptographic protocol type checker . http:\/\/cryptyc.cs.depaul.edu\/ Gordon, A. D. and Jeffrey, A. S. A. 2002. Cryptyc: Cryptographic protocol type checker. http:\/\/cryptyc.cs.depaul.edu\/"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/959088.959090"},{"key":"e_1_2_1_56_1","article-title":"Types and effects for asymmetric cryptographic protocols","volume":"12","author":"Gordon A. D.","year":"2003","unstructured":"Gordon , A. D. and Jeffrey , A. S. A. 2003 b. Types and effects for asymmetric cryptographic protocols . J. Comput. Secur. 12 , 3\/4, 435--484. Gordon, A. D. and Jeffrey, A. S. A. 2003b. Types and effects for asymmetric cryptographic protocols. J. Comput. Secur. 12, 3\/4, 435--484.","journal-title":"J. Comput. Secur."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_17"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_24"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. R. Findler. Ed., 93--104","author":"Gronski J.","unstructured":"Gronski , J. , Knowles , K. , Tomb , A. , Freund , S. N. , and Flanagan , C . 2006. Sage: Hybrid checking for flexible specifications . In Proceedings of the Scheme and Functional Programming Workshop. R. Findler. Ed., 93--104 . Gronski, J., Knowles, K., Tomb, A., Freund, S. N., and Flanagan, C. 2006. Sage: Hybrid checking for flexible specifications. In Proceedings of the Scheme and Functional Programming Workshop. R. Findler. Ed., 93--104."},{"key":"e_1_2_1_60_1","volume-title":"Semantics of Programming Languages","author":"Gunter C.","unstructured":"Gunter , C. 1992. Semantics of Programming Languages . MIT Press . Gunter, C. 1992. Semantics of Programming Languages. MIT Press."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/1813084.1813099"},{"key":"e_1_2_1_62_1","doi-asserted-by":"crossref","unstructured":"Hubbers E. Oostdijk M. and Poll E. 2003. Implementing a formally verifiable security protocol in Java Card. In Security in Pervasive Computing 213--226.  Hubbers E. Oostdijk M. and Poll E. 2003. Implementing a formally verifiable security protocol in Java Card. In Security in Pervasive Computing 213--226.","DOI":"10.1007\/978-3-540-39881-3_19"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(1:2)2008"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411212"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.13"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_36"},{"key":"e_1_2_1_68_1","unstructured":"Martin-L\u00f6f P. 1984. Intuitionistic Type Theory. Bibliopolis.  Martin-L\u00f6f P. 1984. Intuitionistic Type Theory. Bibliopolis."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_2_1_71_1","unstructured":"Nadalin A. Kaler C. Hallam-Baker P. and Monzillo R. 2004. OASIS Web services security: SOAP message security 1.0. http:\/\/www.oasis-open.org\/committees\/download.php\/5941\/oasis-200401-wss%-soap-message-security-1.0.pdf  Nadalin A. Kaler C. Hallam-Baker P. and Monzillo R. 2004. OASIS Web services security: SOAP message security 1.0. http:\/\/www.oasis-open.org\/committees\/download.php\/5941\/oasis-200401-wss%-soap-message-security-1.0.pdf"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/648083.747139"},{"key":"e_1_2_1_74_1","volume-title":"Logic and Computation: Interactive Proof with Cambridge LCF","author":"Paulson L. C.","unstructured":"Paulson , L. C. 1987. Logic and Computation: Interactive Proof with Cambridge LCF . Cambridge University Press . Paulson, L. C. 1987. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press."},{"key":"e_1_2_1_75_1","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle: A Generic Theorem Prover","author":"Paulson L. C.","year":"1991","unstructured":"Paulson , L. C. 1991 . Isabelle: A Generic Theorem Prover . Lecture Notes in Computer Science , vol. 828 . Springer . Paulson, L. C. 1991. Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828. Springer."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950007002X"},{"key":"e_1_2_1_77_1","volume-title":"Proceedings of the Workshop on Information Technologies and Systems Meetings (WITS'07)","author":"Poll E.","unstructured":"Poll , E. and Schubert , A . 2007. Verifying an implementation of SSH . In Proceedings of the Workshop on Information Technologies and Systems Meetings (WITS'07) . 164--177. Poll, E. and Schubert, A. 2007. Verifying an implementation of SSH. In Proceedings of the Workshop on Information Technologies and Systems Meetings (WITS'07). 164--177."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_2_1_79_1","volume-title":"Proceedings of the Conference on Programming Languages and Systems (ESOP'01)","volume":"2028","author":"Pottier F.","unstructured":"Pottier , F. , Skalka , C. , and Smith , S . 2001. A systematic approach to access control . In Proceedings of the Conference on Programming Languages and Systems (ESOP'01) . Lecture Notes in Computer Science , vol. 2028 . Springer, 30--45. Pottier, F., Skalka, C., and Smith, S. 2001. A systematic approach to access control. In Proceedings of the Conference on Programming Languages and Systems (ESOP'01). Lecture Notes in Computer Science, vol. 2028. Springer, 30--45."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_17"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.032"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_28"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.29"},{"key":"e_1_2_1_88_1","doi-asserted-by":"crossref","unstructured":"Syme D. Granicz A. and Cisternino A. 2007. Expert F&num;. Apress.  Syme D. Granicz A. and Cisternino A. 2007. Expert F&num;. Apress.","DOI":"10.1007\/978-1-4302-0285-1"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.24"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2007.5"},{"key":"e_1_2_1_91_1","volume-title":"Proceedings of the IEEE Symposium on 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 Symposium on Security and Privacy. 178--194 . Woo, T. and Lam, S. 1993. A semantic model for authentication protocols. In Proceedings of the IEEE Symposium on Security and Privacy. 178--194."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159849"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1890028.1890031","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1890028.1890031","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:39Z","timestamp":1750244379000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1890028.1890031"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":93,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1890028.1890031"],"URL":"https:\/\/doi.org\/10.1145\/1890028.1890031","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2010-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-02-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}