Formal Modeling and Analyzing Kerberos Protocol

Author

Li, Qin ; Yang, Fan ; Zhu, Huibiao ; Zhu, Longfei

Author_Institution

Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China

Volume

7

fYear

2009

fDate

March 31 2009-April 2 2009

Firstpage

813

Lastpage

819

Abstract

Kerberos protocol is one of the popular security protocols used to authenticate the identities of the communication participants. The key distribution mechanism in this protocol is suitable for other secure applications. We formalize the protocol using CSP methods. Based on the formal model, the mechanism of the protocol is exposed to us clearly. Principles and tools support the verification of the formal model. In that way, we can prove that the system protected by the protocol is indeed secure as it declared. The reasons for security can be fixed out formally as a reference to analyzing other protocols.

Keywords

communicating sequential processes; cryptographic protocols; formal verification; CSP method; Kerberos protocol; communicating sequential processes; cryptography; formal model verification; key distribution mechanism; security protocol; Authentication; Computer science; Cryptographic protocols; Information analysis; Network servers; Protection; Public key; Public key cryptography; Security; Testing; Formal Methods; Kerberos Protocol; Security;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science and Information Engineering, 2009 WRI World Congress on

Conference_Location

Los Angeles, CA

Print_ISBN

978-0-7695-3507-4

Type

conf

DOI

10.1109/CSIE.2009.64

Filename

5170428