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

Formal specification and verification of andrew secure RPC protocol based on strand spaces model

作　　者：周清雷[1] 赵琳[1] 赵东明[1] 

机构地区：[1]郑州大学信息工程学院,郑州450052

出　　处：《计算机工程与应用》2007年第13期153-155,158,共4页Computer Engineering and Applications

摘　　要：首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的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.

关 键 词：安全协议 串空间 ANDREW SECURE RPC协议 

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