密码协议的Promela语言建模及分析  

Promela modeling and analysis for security protocol

作　　者：龙士工[1] 王巧丽[1] 李祥[1] 

机构地区：[1]贵州大学计算机软件与理论研究所,贵州贵阳550025

出　　处：《计算机应用》2005年第7期1548-1550,共3页journal of Computer Applications

基　　金：贵州省自然科学基金资助项目(20043029)

摘　　要：给出了利用SPIN模型检测分析密码协议的一般方法。作为一个实例,对NeedhamSchroeder公钥密码协议用Promela语言建模,并利用SPIN进行了分析验证,发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析。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.

关 键 词：密码协议 模型检测 SPIN PROMELA 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]