面向命题投影时序逻辑的安全协议模型检测

• 作者: 杨琛 段振华 王小兵
• 来源期刊: 西安交通大学学报
• 关键词: 模型检测 协议验证 时序逻辑 安全协议
• 年，卷（期）: 2010,（8）
• 页码范围: 30-35
• 分类号: TP301
• 语种: 中文

摘要

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王小兵	西安电子科技大学计算理论与技术研究所	60	484	12.0	18.0
3	段振华	西安电子科技大学计算理论与技术研究所	47	363	10.0	16.0
6	杨琛	西安电子科技大学计算理论与技术研究所	4	29	3.0	4.0