Formal Specification and Verification of Andrew secure RPC protocol Based on Strand Spaces Model

Computer Engineering and Applications ›› 2007, Vol. 43 ›› Issue (13): 153-155.

• 网络、通信与安全 • Previous Articles Next Articles

Formal Specification and Verification of Andrew secure RPC protocol Based on Strand Spaces Model

Received:2006-06-05 Revised:1900-01-01 Online:2007-05-01 Published:2007-05-01

基于串空间模型的Andrew RPC协议的分析与验证

周清雷赵琳赵东明

郑州大学信息工程学院郑州大学信息工程学院

通讯作者: 赵琳

Abstract

Abstract: With the popularization of network, security protocol are becoming more and more important. In this paper, a model of strand spaces, a current leading branch of formal automatic verifying, is described in detail. A methodology is presented by using strand spaces to analyze the Andrew secure RPC protocol, and some security bug is discovered.

Key words: strand spaces, Andrew secure RPC protocol, security protocol

摘要： 本文首先介绍了当前安全协议形式化验证的前沿方向串空间理论，并运用串空间模型对改进后的Andrew secure RPC协议进行了形式化分析与验证，然后指出了安全缺陷。

关键词: 串空间, Andrew secure RPC协议, 安全协议

周清雷赵琳赵东明. 基于串空间模型的Andrew RPC协议的分析与验证[J]. 计算机工程与应用, 2007, 43(13): 153-155.

[1]	LI Qian1, WANG Zheng1, MA Jianfen1, LI Na2. Lightweight mobile payment protocol fairness analysis [J]. Computer Engineering and Applications, 2018, 54(19): 82-87.
[2]	QIANG Xiaohui, CHEN Bo, CHEN Guokai. Analysis and detection for HeartBleed vulnerability of OpenSSL [J]. Computer Engineering and Applications, 2016, 52(9): 88-95.
[3]	YU Lei1, WEI Shimin1, ZHUO Zepeng2. Research on consistence of strand parameters for protocol principals in authentication test theory [J]. Computer Engineering and Applications, 2015, 51(13): 86-91.
[4]	HU Xiaohui1, CHEN Huili1, SHI Guangtian2, CHEN Yong1. Formal modeling and verification of CTCS-4 security protocol [J]. Computer Engineering and Applications, 2014, 50(4): 81-85.
[5]	YU Lei, WEI Shimin. Analysis on properties for principals’ keys on construction of test components [J]. Computer Engineering and Applications, 2013, 49(6): 114-117.
[6]	FAN Yutao1, SU Guiping2. Formal analysis method suitable to security protocols with timestamp [J]. Computer Engineering and Applications, 2012, 48(36): 116-120.
[7]	YAO Huazhen1, LIU Chuanju1, LI Xiaomin2. Authentication protocol based on AES and NTRU for RFID [J]. Computer Engineering and Applications, 2012, 48(35): 80-84.
[8]	DENG Fan1，DENG Shaofeng1，ZHANG Wenzheng2. Standardized design of security protocols [J]. Computer Engineering and Applications, 2011, 47(18): 122-126.
[9]	WANG Tao，WANG Li-bin，MA Chang-she. Design and implementation of generic high efficient RFID authorization protocol model [J]. Computer Engineering and Applications, 2010, 46(4): 72-75.
[10]	FENG Yong¹，LIANG Hao². Efficient anonymous authentication scheme in VANETs [J]. Computer Engineering and Applications, 2010, 46(23): 126-128.
[11]	WU Chang¹，XIAO Mei-hua¹，LUO Min²，LIU Qiao-wei¹，XIONG Hao¹. Effective automatic generation of security protocol’s verification model [J]. Computer Engineering and Applications, 2010, 46(2): 79-82.
[12]	LI Ting-yuan1，2，QIN Zhi-guang1，LIU Xiao-dong2，ZHANG Xuan-fang2. Formal analysis of Needham-Schroeder protocol with authentication test methods [J]. Computer Engineering and Applications, 2010, 46(19): 100-102.
[13]	CHEN Li，GUO Qing-pu. New compound electronic commerce security protocol [J]. Computer Engineering and Applications, 2010, 46(11): 14-17.
[14]	LI Yuan-jie^1,2,GAO Wei-xun¹,YANG Fan¹,CAO Qi-ying³. Research on broadcast security protocol of ubiquitous computing [J]. Computer Engineering and Applications, 2009, 45(19): 34-36.
[15]	ZHANG Chao,HAN Ji-hong,WANG Ya-di,ZHU Yu-na. Improved first-order logic model for security protocols [J]. Computer Engineering and Applications, 2008, 44(26): 95-98.

Formal Specification and Verification of Andrew secure RPC protocol Based on Strand Spaces Model

基于串空间模型的Andrew RPC协议的分析与验证

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics