{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T13:30:58Z","timestamp":1773408658571,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,3,18]],"date-time":"2008-03-18T00:00:00Z","timestamp":1205798400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-05-1-0818N00014-01-1-0795N00014-04-1-0725N00014-07-1-1039"],"award-info":[{"award-number":["N00014-05-1-0818N00014-01-1-0795N00014-04-1-0725N00014-07-1-1039"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000121","name":"Division of Mathematical Sciences","doi-asserted-by":"publisher","award":["DMS-0239996CNS-0429689CNS-0753492CNS-0524059"],"award-info":[{"award-number":["DMS-0239996CNS-0429689CNS-0753492CNS-0524059"]}],"id":[{"id":"10.13039\/100000121","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["DMS-0239996CNS-0429689CNS-0753492CNS-0524059"],"award-info":[{"award-number":["DMS-0239996CNS-0429689CNS-0753492CNS-0524059"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,3,18]]},"DOI":"10.1145\/1368310.1368326","type":"proceedings-article","created":{"date-parts":[[2008,5,15]],"date-time":"2008-05-15T18:35:39Z","timestamp":1210876539000},"page":"87-99","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Computationally sound mechanized proofs for basic and public-key Kerberos"],"prefix":"10.1145","author":[{"given":"B.","family":"Blanchet","sequence":"first","affiliation":[{"name":"Sup\u00e9rieure & INRIA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. D.","family":"Jaggard","sequence":"additional","affiliation":[{"name":"Rutgers University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Scedrov","sequence":"additional","affiliation":[{"name":"University of Pennsylvania"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.-K.","family":"Tsay","sequence":"additional","affiliation":[{"name":"University of Pennsylvania"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,3,18]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"LNCS","volume-title":"First IFIP","author":"Abadi M.","year":"2000","unstructured":"M. Abadi and P. Rogaway . Reconciling two views of cryptography (the computational soundness of formal encryption) . In First IFIP , volume 1872 of LNCS . Springer , Aug. 2000 . M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). In First IFIP, volume 1872 of LNCS. Springer, Aug. 2000."},{"key":"e_1_3_2_1_2_1","volume-title":"Password-Based Authenticated Key Exchange in the Three-Party Setting. IEE Proc. Information Security, 153(1)","author":"Abdalla M.","year":"2006","unstructured":"M. Abdalla , P.-A. Fouque , and D. Pointcheval . Password-Based Authenticated Key Exchange in the Three-Party Setting. IEE Proc. Information Security, 153(1) , 2006 . M. Abdalla, P.-A. Fouque, and D. Pointcheval. Password-Based Authenticated Key Exchange in the Three-Party Setting. IEE Proc. Information Security, 153(1), 2006."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11863908_23"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/948109.948140"},{"key":"e_1_3_2_1_6_1","volume-title":"DIMACS'97","author":"Bella G.","year":"1997","unstructured":"G. Bella and L. C. Paulson . Using Isabelle to Prove Properties of the Kerberos Authentication System . In DIMACS'97 , Workshop on Design and Formal Verification of Security Protocols (CD-ROM) , 1997 . G. Bella and L. C. Paulson. Using Isabelle to Prove Properties of the Kerberos Authentication System. In DIMACS'97, Workshop on Design and Formal Verification of Security Protocols (CD-ROM), 1997."},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","volume-title":"ESORICS'98","author":"Bella G.","year":"1998","unstructured":"G. Bella and L. C. Paulson . Kerberos Version IV: Inductive Analysis of the Secrecy Goals . In ESORICS'98 , volume 1485 of LNCS . Springer , 1998 . G. Bella and L. C. Paulson. Kerberos Version IV: Inductive Analysis of the Secrecy Goals. In ESORICS'98, volume 1485 of LNCS. Springer, 1998."},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","volume-title":"CRYPTO'96","author":"Bellare M.","year":"1996","unstructured":"M. Bellare , R. Canetti , and H. Krawczyk . Keying hash functions for message authentication . In CRYPTO'96 , volume 1109 of LNCS . Springer , 1996 . M. Bellare, R. Canetti, and H. Krawczyk. Keying hash functions for message authentication. In CRYPTO'96, volume 1109 of LNCS. Springer, 1996."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647096.716997"},{"key":"e_1_3_2_1_10_1","volume-title":"Limitations of the Kerberos Authentication System. In USENIX Conference Proceedings","author":"Bellovin S. M.","year":"1991","unstructured":"S. M. Bellovin and M. Merritt . Limitations of the Kerberos Authentication System. In USENIX Conference Proceedings , Winter 1991 . S. M. Bellovin and M. Merritt. Limitations of the Kerberos Authentication System. In USENIX Conference Proceedings, Winter 1991."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.16"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11818175_32"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2007.19"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.040"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_20"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.05.005"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_12"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.9"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102124"},{"key":"e_1_3_2_1_23_1","unstructured":"IETF. Public Key Cryptography for Initial Authentication in Kerberos 1996--2006. RFC 4556. Preliminary versions available as a sequence of Internet Drafts at http:\/\/tools.ietf.org\/wg\/krb-wg\/draft-ietf-cat-kerberos-pk-init\/.  IETF. Public Key Cryptography for Initial Authentication in Kerberos 1996--2006. RFC 4556. Preliminary versions available as a sequence of Internet Drafts at http:\/\/tools.ietf.org\/wg\/krb-wg\/draft-ietf-cat-kerberos-pk-init\/."},{"key":"e_1_3_2_1_24_1","volume-title":"Computationally Sound Mechanized Proof of PKINIT for Kerberos. Abstract presented at FCC'07","author":"Jaggard A. D.","unstructured":"A. D. Jaggard , A. Scedrov , and J.-K. Tsay . Computationally Sound Mechanized Proof of PKINIT for Kerberos. Abstract presented at FCC'07 . A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Computationally Sound Mechanized Proof of PKINIT for Kerberos. Abstract presented at FCC'07."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102126"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/288090.288117"},{"key":"e_1_3_2_1_27_1","series-title":"LNCS","volume-title":"FM'99","author":"Lincoln P. D.","year":"1999","unstructured":"P. D. Lincoln , J. C. Mitchell , M. Mitchell , and A. Scedrov . Probabilistic polynomial-time equivalence and security protocols . In FM'99 , volume 1708 of LNCS . Springer , Sept. 1999 . P. D. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security protocols. In FM'99, volume 1708 of LNCS. Springer, Sept. 1999."},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","volume-title":"TACAS'96","author":"Lowe G.","year":"1996","unstructured":"G. Lowe . Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR . In TACAS'96 , volume 1055 of LNCS . Springer , 1996 . G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In TACAS'96, volume 1055 of LNCS. Springer, 1996."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA465466"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00095-X"},{"key":"e_1_3_2_1_31_1","unstructured":"Microsoft. Security Bulletin MS05-042. http:\/\/www.microsoft.com\/technet\/security\/bulletin\/MS05-042.mspx August 2005.  Microsoft. Security Bulletin MS05-042. http:\/\/www.microsoft.com\/technet\/security\/bulletin\/MS05-042.mspx August 2005."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.044"},{"key":"e_1_3_2_1_33_1","first-page":"201","volume-title":"7th USENIX Security Symp.","author":"Mitchell J. C.","year":"1998","unstructured":"J. C. Mitchell , V. Shmatikov , and U. Stern . Finite-State Analysis of SSL 3.0 . In 7th USENIX Security Symp. , pages 201 -- 216 , 1998 . J. C. Mitchell, V. Shmatikov, and U. Stern. Finite-State Analysis of SSL 3.0. In 7th USENIX Security Symp., pages 201--216, 1998."},{"key":"e_1_3_2_1_34_1","volume-title":"July","author":"Neuman C.","year":"2005","unstructured":"C. Neuman , T. Yu , S. Hartman , and K. Raeburn . The Kerberos Network Authentication Service (V5) , July 2005 . http:\/\/www.ietf.org\/rfc\/rfc4120. C. Neuman, T. Yu, S. Hartman, and K. Raeburn. The Kerberos Network Authentication Service (V5), July 2005. http:\/\/www.ietf.org\/rfc\/rfc4120."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"K. Raeburn. Encryption and Checksum Specifications for Kerberos 5. http:\/\/www.ietf.org\/rfc\/rfc3961.txt Feb. 2005.  K. Raeburn. Encryption and Checksum Specifications for Kerberos 5. http:\/\/www.ietf.org\/rfc\/rfc3961.txt Feb. 2005.","DOI":"10.17487\/rfc3961"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74835-9_15"},{"key":"e_1_3_2_1_37_1","volume-title":"TGC'07","author":"Roy A.","year":"2007","unstructured":"A. Roy , A. Datta , and J. C. Mitchell . Formal proofs of cryptographic security of Diffie-Hellman-based protocols . In TGC'07 , Nov. 2007 . To appear. A. Roy, A. Datta, and J. C. Mitchell. Formal proofs of cryptographic security of Diffie-Hellman-based protocols. In TGC'07, Nov. 2007. To appear."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.10"}],"event":{"name":"Asia CCS '08: Asia CCS'08 ACM Symposium on Information, Computer and Communications Security","location":"Tokyo Japan","acronym":"Asia CCS '08","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2008 ACM symposium on Information, computer and communications security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1368310.1368326","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1368310.1368326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:57:46Z","timestamp":1750255066000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1368310.1368326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3,18]]},"references-count":38,"alternative-id":["10.1145\/1368310.1368326","10.1145\/1368310"],"URL":"https:\/\/doi.org\/10.1145\/1368310.1368326","relation":{},"subject":[],"published":{"date-parts":[[2008,3,18]]},"assertion":[{"value":"2008-03-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}