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

doi:10.3724/SP.J.1087.2005.01548

计算机应用 ›› 2005, Vol. 25 ›› Issue (07): 1548-1550.DOI: 10.3724/SP.J.1087.2005.01548

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

龙士工，王巧丽，李祥

贵州大学计算机软件与理论研究所

收稿日期:2004-12-15 修回日期:2005-04-12 出版日期:2005-07-01 发布日期:2005-07-01
作者简介:龙士工（1967- ），男，湖南石门人，讲师，博士研究生，主要研究方向：计算机网络、信息安全；王巧丽（1979-），女，河南人，硕士研究生，主要研究方向：模型检验与协议分析；李祥（1942-），男，贵州人，教授，主要研究方向：计算机网络、信息安全
基金资助:
贵州省自然科学基金资助项目（20043029）

Promela modeling and analysis for security protocol

LONG Shi-gong，WANG Qiao-li，LI Xiang

Institute of Computer Software and Theory, Guizhou University

Received:2004-12-15 Revised:2005-04-12 Online:2005-07-01 Published:2005-07-01

摘要/Abstract

摘要：

给出了利用SPIN模型检测分析密码协议的一般方法。作为一个实例，对NeedhamSchroeder 公钥密码协议用Promela语言建模，并利用SPIN进行了分析验证，发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析

关键词: 密码协议, 模型检测, SPIN, Promela

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.

Key words: security protocol, model checking, SPIN, Promela

中图分类号:

TP309.2

龙士工，王巧丽，李祥. 密码协议的Promela语言建模及分析[J]. 计算机应用, 2005, 25(07): 1548-1550.

LONG Shi-gong，WANG Qiao-li，LI Xiang. Promela modeling and analysis for security protocol[J]. Journal of Computer Applications, 2005, 25(07): 1548-1550.

[1]	包玉龙, 朱雪阳, 张文辉, 孙鹏飞, 赵颖琪. 物联网应用中访问控制智能合约的形式化验证[J]. 计算机应用, 2021, 41(4): 930-938.
[2]	朱玉娜, 张玉涛, 闫少阁, 范钰丹, 陈韩托. 基于半监督子空间聚类的协议识别方法[J]. 计算机应用, 2021, 41(10): 2900-2904.
[3]	安鑫, 夏近伟, 杨海娇, 欧阳一鸣, 任福继. 基于离散控制器合成的异构多核系统资源管理方法[J]. 计算机应用, 2020, 40(6): 1698-1706.
[4]	毛昕怡, 钮俊, 丁雪儿, 张开乐. 基于模型检测的微服务组合平台QoS验证[J]. 计算机应用, 2020, 40(11): 3267-3272.
[5]	常天佑, 魏强, 耿洋洋. 基于状态转换的PLC程序模型构建方法[J]. 计算机应用, 2017, 37(12): 3574-3580.
[6]	于丽贞徐中伟陈祖希张舒青. 基于梯形逻辑的联锁系统形式化验证方法[J]. 计算机应用, 2013, 33(12): 3419-3422.
[7]	张妤阴建强胡杰. 通用可组合安全计算的信任模型研究[J]. 计算机应用, 2012, 32(05): 1371-1374.
[8]	廖紫骅谭红艳吴尽昭. 基于Groebner基的模型检测技术及其工具实现[J]. 计算机应用, 2009, 29(10): 2841-2843.
[9]	陈晨陈永生. 基于层次单元划分的软件模型检测技术研究[J]. 计算机应用, 2008, 28(8): 2109-2112.
[10]	闫志华李成郑艳萍. 工作流模型检测研究[J]. 计算机应用, 2007, 27(6): 1448-1451.
[11]	文英董荣胜郭云川. 一种提高Ad Hoc网络节点能量效率的DPM模型[J]. 计算机应用, 2007, 27(5): 1095-1098.
[12]	赵宇王亚弟韩继红范钰丹赵琦. 一种基于问题求解理论的密码协议形式模型[J]. 计算机应用, 2007, 27(2): 303-307.
[13]	缪力张大方. 程序模型检测的两阶段框架[J]. 计算机应用, 2007, (12): 3089-3091.
[14]	张频罗贵明 . UML模型检测方法的研究[J]. 计算机应用, 2007, 27(10): 2493-2497.
[15]	姜洋罗贵明 . Petri网模型的扩展与检测[J]. 计算机应用, 2007, 27(1): 183-185.

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

Promela modeling and analysis for security protocol

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics