Casper/FDR和串空间在物联网通信协议中的形式化分析  

Formal analysis on Casper /FDR and strand space for Internet of things protocol

作　　者：吴名欢[1] 程小辉[1] 

机构地区：[1]桂林理工大学信息科学与工程学院,广西桂林541004

出　　处：《桂林理工大学学报》2014年第2期338-344,共7页Journal of Guilin University of Technology

基　　金：国家自然科学基金项目(61262075);广西高等学校重大科研项目(20120120012)

摘　　要：通过应用实例研究了如何用Casper/FDR和串空间两种分析方法对通信协议进行形式化分析:用Casper/FDR对协议的有穷状态进行穷举验证,当发现协议漏洞时会自动给出攻击的迹,但是此方法会产生状态爆炸的问题;串空间方法正好可以解决状态爆炸问题,用串空间对协议的各种状态进行证明,但是如果发现了协议漏洞,该方法不能给出攻击者的迹。Casper/FDR method and strand space method are studied with application examples. These examples show how to use these methods to analyze protocol. The Casper/FDR method can verify the status of the protocol, and the number of status is limited. When a loophole of the protocol is found, the tracks of attacker will be automatically given. This method will produce a state explosion problem. However, strand space method can solve this problem. Strand space for a variety of state protocol is proved. If a loophole in the protocol appears, the tracks of attacker cannot be found.

关 键 词：CASPER FDR 协议形式化分析方法 串空间 

分 类 号：TP391.41[自动化与计算机技术—计算机应用技术]