| 基于UPPAAL的NS密码协议模型检测分析 |
| |
| 引用本文： | 李忠慧,张广泉. 基于UPPAAL的NS密码协议模型检测分析[J]. 重庆师范大学学报(自然科学版), 2009, 26(4): 78-081. DOI: 10.3969/J.ISSN.1672-6693.2009.04.016 |
| |
| 作者姓名： | 李忠慧 张广泉 |
| |
| 作者单位： | 重庆师范大学,数学与计算机科学学院,重庆,400047;盐城师范学院,信息科学与技术学院,江苏,盐城,224002;重庆师范大学,数学与计算机科学学院,重庆,400047 |
| |
| 基金项目： | 重庆市自然科学基金项目 |
| |
| 摘 要： | 形式化分析方法是目前密码协议分析的主流方法。然而，典型的密码协议形式化验证方法没有考虑时间因素，这个选择使得分析简单化。本文提出了运用基于时间自动机的模型检测工具UPPAAL分析密码协议的方法，并对著名的Needham—Schroeder协议（简称NS协议）的简单版本进行了分析。在对NS协议进行建模时，考虑消息实际传输需花费时间，引入消息的时间信息，从而构建NS协议的时间自动机模型。该方法利用UPPAAL的检查引擎所用的先进技术使其克服了一般时间自动机应用存在的状态空间爆炸问题。实验结果UPPAAL给出了NS协议认证失败的一种可能之一。分析结果表明，入侵者可以轻松地对NS公钥协议进行有效攻击。从而证明UPPAAL工具可以成功检测出NS协议的缺陷。
|
| 关 键 词： | UPPAAL 密码协议 模型检测 |
Model Checking of the NS Cryptographic Protocol and Analysis Based on the UPPAAL |
| |
| LI Zhong-hui,ZHANG Guang-quan. Model Checking of the NS Cryptographic Protocol and Analysis Based on the UPPAAL[J]. Journal of Chongqing Normal University:Natural Science Edition, 2009, 26(4): 78-081. DOI: 10.3969/J.ISSN.1672-6693.2009.04.016 |
| |
| Authors: | LI Zhong-hui ZHANG Guang-quan |
| |
| Affiliation: | LI Zhong-hui1,2,ZHANG Guang-quan1(1.College of Mathematics & Computer Science,Chongqing Normal University,Chongqing 400047,2.College of Information Science , Technology,Yancheng Teachers University,Yancheng Jiangsu 224002,China) |
| |
| Abstract: | Formal analysis methods are currently the mainstream method of cryptographic protocol analysis.Typically,the methods for formal verification of security protocols do not take time into account,and this choice also simplifies the analysis.A methodology is presented here by using a model checker of formal methods based on timed automaton,UPPAAL,to analyze a simplified version of the well known Needham-Schroeder Public-Key Protocol(NS for short).Since the actual sending of the message takes time,timeliness of ... |
| |
| Keywords: | UPPAAL |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《重庆师范大学学报(自然科学版)》浏览原始摘要信息 |
|
点击此处可从《重庆师范大学学报(自然科学版)》下载全文 |
|
