摘要
首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的Andrew secure RPC协议进行了形式化分析与验证,然后指出了安全缺陷。
With the popularization of network,security protocol are becoming more and more important.ln 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.
出处
《计算机工程与应用》
CSCD
北大核心
2007年第13期153-155,158,共4页
Computer Engineering and Applications
