A Formal Analysis of Some Properties of Kerberos 5 Using MSR

Cape Breton, Nova Scotia, Canada June 24-June 26

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/CSFW.2002.1021815

15th IEEE Computer Security Foundatio ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Frederick Butler Articles by Iliano Cervesato Articles by Aaron D. Jaggard Articles by Andre Scedrov

	ASCII Text	x
	Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov, "A Formal Analysis of Some Properties of Kerberos 5 Using MSR," Computer Security Foundations Workshop, IEEE, pp. 175, 15th IEEE Computer Security Foundations Workshop (CSFW'02), 2002.

	BibTex	x
	@article{ 10.1109/CSFW.2002.1021815, author = {Frederick Butler and Iliano Cervesato and Aaron D. Jaggard and Andre Scedrov}, title = {A Formal Analysis of Some Properties of Kerberos 5 Using MSR}, journal ={Computer Security Foundations Workshop, IEEE}, volume = {0}, year = {2002}, issn = {1063-6900}, pages = {175}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2002.1021815}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Security Foundations Workshop, IEEE TI - A Formal Analysis of Some Properties of Kerberos 5 Using MSR SN - 1063-6900 SP EP A1 - Frederick Butler, A1 - Iliano Cervesato, A1 - Aaron D. Jaggard, A1 - Andre Scedrov, PY - 2002 KW - null VL - 0 JA - Computer Security Foundations Workshop, IEEE ER -

Frederick Butler, University of Pennsylvania

Iliano Cervesato, ITT Industries, Inc.

Aaron D. Jaggard, University of Pennsylvania

Andre Scedrov, University of Pennsylvania

We formalize aspects of the Kerberos 5 authentication protocol in the Multi-Set Rewriting formalism (MSR) on two levels of detail. The more detailed formalization reflects the intricate structure of the Kerberos 5 specification, taking into account several protocol features which have not been previously considered. In the abstract formalization, we prove an authentication property about Kerberos 5. We discovered three anomalies, one of which occurs on both levels of detail, while the other two rely on the richer structure of the detailed formalization. We also discuss how the addition of checksums (some of which are in the protocol specification and some of which are not) may eliminate some of these anomalies.

Citation:

Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov, "A Formal Analysis of Some Properties of Kerberos 5 Using MSR," csfw, pp.175, 15th IEEE Computer Security Foundations Workshop (CSFW'02), 2002

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.