| NSPK协议的Spin模型检测 |
| |
| 引用本文： | 陈道喜,张广泉,陈冬火. NSPK协议的Spin模型检测[J]. 微电子学与计算机, 2008, 25(10) |
| |
| 作者姓名： | 陈道喜 张广泉 陈冬火 |
| |
| 作者单位： | 苏州大学计算机科学与技术学院,江苏,苏州,215006 |
| |
| 基金项目： | 江苏省高校自然科学基金，重庆市自然科学基金 |
| |
| 摘 要： | NSPK协议是一个经典的认证密码协议.通过建立该协议的Promela模型,采用线性时序逻辑描述模型性质,并用模型检测工具Spin进行验证,进而生成入侵者的攻击序列.
|
| 关 键 词： | 模型检测 NSPK协议 Spin |
Model Checking of the NSPK Protocol with Spin |
| |
| CHEN Dao-xi,ZHANG Guang-quan,CHEN Dong-huo. Model Checking of the NSPK Protocol with Spin[J]. Microelectronics & Computer, 2008, 25(10) |
| |
| Authors: | CHEN Dao-xi ZHANG Guang-quan CHEN Dong-huo |
| |
| Abstract: | NSPK protocol is a classic authentication cryptographic protocol. Through establishing the Promela models of the protocol, and using linear temporal logic to describe the properties of models, at last, using the model checking tools Spin to verify the properties, and then we find the sequence of the intruder attack. |
| |
| Keywords: | model checking NSPK protocol Spin |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
