【摘要】 网络安全已成为世人关注的问题,安全协议的形式化验证显得越来越重要,基于Spi演算的验证是一种很好的模型检测方法。我们介绍了Spi演算并扩展了两个基本原语,描述和验证Kerberos协议的认证性,同时指出了该协议的不足之处,最后分析了基于Spi演算的形式化研究的今后发展方向。更多还原

【Abstract】 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.更多还原