密码协议安全性证明系统解析器的设计与实现

• 作者: 李安乐 祝跃飞 陈楠 顾纯祥
• 来源期刊: 计算机应用研究
• 关键词: 可证明安全 自动化 进程演算
• 年，卷（期）: 2010,（9）
• 页码范围: 3529-3532
• 分类号: TP309
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2010.09.089

摘要

可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定,利用计算机辅助构造游戏序列进而实现自动化证明是当前一种可行的方法.为此提出一种基于进程演算的密码协议形式化描述模型,定义了描述密码协议安全性证明中攻击游戏的语法规则,并借助工具LEX和YACC,设计出解析器程序,将密码协议及其安全性的形式化描述解析为自动化安全性证明系统的初始数据结构,并用实例来说明这种方法的可行性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	祝跃飞	解放军信息工程大学信息工程学院	62	440	13.0	16.0
2	顾纯祥	解放军信息工程大学信息工程学院	10	33	4.0	5.0
3	陈楠	解放军信息工程大学信息工程学院	4	9	2.0	3.0
4	李安乐	解放军信息工程大学信息工程学院	1	0	0.0	0.0