Formal Research of Kerberos Protocol Based on Spi Calculus
基于Spi演算的Kerberos认证协议形式化研究

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