| 面向命题投影时序逻辑的安全协议模型检测 |
| |
| 引用本文： | 杨琛,段振华,王小兵.面向命题投影时序逻辑的安全协议模型检测[J].西安交通大学学报,2010,44(8). |
| |
| 作者姓名： | 杨琛 段振华 王小兵 |
| |
| 作者单位： | 1. 西安电子科技大学计算理论与技术研究所,710071,西安;武汉大学软件工程国家重点实验室,430072,武汉
2. 西安电子科技大学计算理论与技术研究所,710071,西安 |
| |
| 基金项目： | 国家自然科学基金重大国际合作项目，国家自然科学基金资助项目，国家重点基础研究发展规划资助项目，武汉大学软件工程国家重点实验室开放基金资助项目，中央高校基本科研业务费专项资金资助项目 |
| |
| 摘 要： | 针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.
|
| 关 键 词： | 模型检测 协议验证 时序逻辑 安全协议 |
Model-Checking Security Protocol with Propositional Projection Temporal Logic |
| |
| YANG Chen,DUAN Zhenhua,WANG Xiaobing.Model-Checking Security Protocol with Propositional Projection Temporal Logic[J].Journal of Xi'an Jiaotong University,2010,44(8). |
| |
| Authors: | YANG Chen DUAN Zhenhua WANG Xiaobing |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
