论文部分内容阅读
利用形式化方法或工具自动化分析实用安全协议十分必要，定理证明技术因其可解决无限状态系统的验证备受关注，但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础，以项重写形式化定义协议模型，以树自动机模拟协议攻击者知识集，给出攻击者知识集可达项逼近求解的算法，并根据上述模型讨论秘密性和认证性的验证方法，最后以Needham-Schroeder公钥认证协议为例验证模型的有效性，并指出下一步研究方向。