基于树语言逼近的安全协议形式化分析

摘要：

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

关键词：安全协议、项重写、树自动机、树语言、逼近、秘密性、认证性

所属期刊栏目：37

分类号：TP309(计算技术、计算机技术)

资助基金：国家高技术研究发展计划8632007AA01Z471

在线出版日期：2010-04-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：176-180