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

Formally Analyzing Security Protocol Using Approximation of Tree Language

作　　者：刘楠[1] 朱文也[1] 祝跃飞[1] 陈晨[1] 

机构地区：[1]信息工程大学信息工程学院,郑州450002

出　　处：《计算机科学》2010年第1期176-180,共5页Computer Science

基　　金：国家高技术研究发展计划(863)(2007AA01Z471)资助

摘　　要：利用形式化方法或工具自动化分析实用安全协议十分必要,定理证明技术因其可解决无限状态系统的验证备受关注,但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础,以项重写形式化定义协议模型,以树自动机模拟协议攻击者知识集,给出攻击者知识集可达项逼近求解的算法,并根据上述模型讨论秘密性和认证性的验证方法,最后以Needham-Schroeder公钥认证协议为例验证模型的有效性,并指出下一步研究方向。Formal method and automated tools are both necessary and efficient for analyzing practical security protocols. Theorem proving theory has been studied intensively because it can verify infinite-state system. But there are still limitations when verifying large scale system automatically. A formal model for security protocols was proposed based on theorem proving and rewriting approximation theory. It utilizes term rewriting system and tree automata to model protocol and the knowledge of intruder. An automatic generated approximation algorithm was designed to calculate the fix-point tree automata. In this model, secrecy and authentication were discussed. By a case of studY, NSPK was analyzed effectively.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]