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

• 作者: 吴名欢 程小辉
• 来源期刊: 桂林理工大学学报
• 学科: 工学
• 关键词: Casper/FDR 协议形式化分析方法 串空间
• 年，卷（期）: 2014,（2）
• 所属期刊栏目: 信息科学与自动控制
• 页码范围: 338-344
• 页数: 7页
• 分类号: TP391.41
• 字数: 6679字
• 语种: 中文
• DOI: 10.3969/j.issn.1674-9057.2014.02.022

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	程小辉	桂林理工大学信息科学与工程学院	91	420	10.0	16.0
2	吴名欢	桂林理工大学信息科学与工程学院	10	24	3.0	4.0