| 密码协议的Promela语言建模及分析 |
| |
| 引用本文： | 龙士工,王巧丽,李祥. 密码协议的Promela语言建模及分析[J]. 计算机应用, 2005, 25(7): 1548-1550. DOI: 10.3724/SP.J.1087.2005.01548 |
| |
| 作者姓名： | 龙士工 王巧丽 李祥 |
| |
| 作者单位： | 贵州大学,计算机软件与理论研究所,贵州,贵阳,550025;贵州大学,计算机软件与理论研究所,贵州,贵阳,550025;贵州大学,计算机软件与理论研究所,贵州,贵阳,550025 |
| |
| 基金项目： | 贵州省自然科学基金资助项目(20043029) |
| |
| 摘 要： | 给出了利用SPIN模型检测分析密码协议的一般方法。作为一个实例，对Needham Schroeder 公钥密码协议用Promela语言建模，并利用SPIN进行了分析验证，发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析
|
| 关 键 词： | 密码协议 模型检测 SPIN Promela |
| 文章编号： | 1001-9081(2005)07-1548-03 |
| 收稿时间： | 2004-12-15 |
| 修稿时间： | 2005-04-12 |
Promela modeling and analysis for security protocol |
| |
| LONG Shi-Gong,WANG Qiao-li,LI Xiang. Promela modeling and analysis for security protocol[J]. Journal of Computer Applications, 2005, 25(7): 1548-1550. DOI: 10.3724/SP.J.1087.2005.01548 |
| |
| Authors: | LONG Shi-Gong WANG Qiao-li LI Xiang |
| |
| Affiliation: | Institute of Computer Software and Theory, Guizhou University |
| |
| Abstract: | The normal model checking technology to analyse security protocol was introduce. As an example, a model for Needham-Schroeder Public-Key Protocol was constructed by using Promela language. SPIN was used to check and discover an attack upon the protocol. The method is easy to extend to check the security protocol which involves several agents. |
| |
| Keywords: | security protocol model checking SPIN Promela |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用》浏览原始摘要信息 |
|
点击此处可从《计算机应用》下载全文 |
