基于spi演算的kerberos认证协议形式化研究

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