{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T12:46:30Z","timestamp":1772023590051,"version":"3.50.1"},"reference-count":12,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/csfw.2002.1021815","type":"proceedings-article","created":{"date-parts":[[2005,8,24]],"date-time":"2005-08-24T23:23:34Z","timestamp":1124925814000},"page":"165","source":"Crossref","is-referenced-by-count":8,"title":["A formal analysis of ome properties of kerberos 5 using MSR"],"prefix":"10.1109","author":[{"given":"F.","family":"Butler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I.","family":"Cervesato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.D.","family":"Jaggard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Scedrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref4","article-title":"Mechanising BAN Kerberos by the Inductive Method","year":"1998","journal-title":"Proc of CAV98 - Tenth International Conference on Computer Aided Verification"},{"key":"ref3","first-page":"361","article-title":"Kerberos Version IV: Inductive Analysis of the Secrecy Goals","year":"0"},{"key":"ref10","author":"neuman","year":"2001","journal-title":"The Kerberos Network Authentication Service (V5)"},{"key":"ref6","article-title":"Typed MSR: Syntax and Examples","author":"cervesato","year":"0"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/32.713329"},{"key":"ref5","first-page":"1337","article-title":"Formal Analysis of the Kerberos Authentication System","volume":"3","author":"bella","year":"1997","journal-title":"J Universal Comp Sci"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/RISP.1993.287633"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.17487\/rfc1510"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1999.779762"},{"key":"ref2","article-title":"Using Isabelle to Prove Properties of the Kerberos Authentication System","author":"bella","year":"1997","journal-title":"Proc of DIMACS'97 Workshop on Design and Formal Verification of Security Protocols (CD-ROM)"},{"key":"ref9","first-page":"141","article-title":"Automated Analysis of Cryptographic Protocols Using Mur?","author":"mitchell","year":"1997","journal-title":"Proc of the IEEE Symposium on Security and Privacy IEEE Computer Society Press"},{"key":"ref1","article-title":"Inductive Verification of Cryptographic Protocols","author":"bella","year":"2000"}],"event":{"name":"15th IEEE Computer Security Foundations Workshop CSFW-15","location":"Cape Breton, NS, Canada","acronym":"CSFW-02"},"container-title":["Proceedings 15th IEEE Computer Security Foundations Workshop. CSFW-15"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/7957\/21985\/01021815.pdf?arnumber=1021815","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,10]],"date-time":"2017-03-10T16:38:22Z","timestamp":1489163902000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1021815\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":12,"URL":"https:\/\/doi.org\/10.1109\/csfw.2002.1021815","relation":{},"subject":[]}}