Formal Research of Kerberos Protocol Based on Spi Calculus
Li Guo · 2004
Abstract With network security drawing the society's attention widely, the formalized verification of security proto- cols turn out to be more and more important. Verification based on Spi calculus is a commendable method of model checking. In this thesis,we introduce Spi calculus and expand its primitives,describing and verifying the authenticity of the Kerberos protocol and pointing out its demerits. Finally,we analyze and show the future developing trend of the formalized research work with the Spi calculus as its base.