一种新的安全协议形式化验证方法

摘要

形式化方法能有效检验安全协议的安全性,BAN类逻辑的发展极大地促进了这一领域的研究,但是现有的BAN类逻辑仍然存在许多问题.在分析现有BAN类逻辑的基础上,提出一种新的安全协议形式化验证方法,实现现有BAN类逻辑的验证功能,并使安全协议验证工作简单可行,便于实现机器自动验证.为安全协议形式化验证提供了一种新的途径.