一种安全协议的形式化分析方法  

Formal Analysis Method of Security Protocol

作　　者：王昕[1] 袁超伟[1] 

机构地区：[1]北京邮电大学信息与通信工程学院,北京100876

出　　处：《计算机工程》2010年第7期82-83,86,共3页Computer Engineering

摘　　要：对快速、高效的形式化分析安全协议进行研究,提出"信任域"的概念。采用与图形化相结合的分析方法,使得协议流程的推导过程清晰、直观。该方法直接分析协议参与主体的信任域,简化分析过程和步骤。实验结果表明,与传统方法相比,该方法更快速、直观,并能为分析协议的冗余性提供具体方法和依据。This paper researches on quick and efficient formal analysis of security protocol, and presents the concept of trust domain. Diagrammatic analysis is adopted, which makes deduction of protocol more clear and intuitive. This method analyzes the trust domain of protocol entity directly, which makes analysis easier. Experimental results show that the method is faster and more intuitive compared with traditional methods. It provides ways and basis for finding redundancies of security protocols.

关 键 词：形式化分析 安全协议 BAN逻辑 NSSK协议 

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