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

来源期刊：桂林理工大学学报2014年第2期

论文作者：吴名欢 程小辉

文章页码：338 - 344

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

摘    要：通过应用实例研究了如何用Casper/FDR和串空间两种分析方法对通信协议进行形式化分析:用Casper/FDR对协议的有穷状态进行穷举验证,当发现协议漏洞时会自动给出攻击的迹,但是此方法会产生状态爆炸的问题;串空间方法正好可以解决状态爆炸问题,用串空间对协议的各种状态进行证明,但是如果发现了协议漏洞,该方法不能给出攻击者的迹。