一种基于通道的AVISPA扩展方法研究  

Extension of AVISPA based on concept of channels

作　　者：刘威[1,2] 郭渊博[1,2] 

机构地区：[1]解放军信息工程大学网络空间安全学院,郑州450001 [2]解放军信息工程大学数学工程与先进计算国家重点实验室,郑州450001

出　　处：《计算机应用研究》2013年第12期3783-3785,3803,共4页Application Research of Computers

基　　金：国家部委基金资助项目(9140C130103120C13062)

摘　　要：针对AVISPA工具在分析某些消息需要依靠具有特定属性的信道传递的安全协议或服务中存在的问题,提出了一种基于抽象通道的扩展方法。抽象通道具有相关的安全性质保证如认证性,能够对提供安全性质保证的底层服务建模,并基于密码机制和标签等实现了抽象通道。利用扩展后的AVISPA工具分析有无消息源认证机制的Diffie-Hellman密钥交换协议的安全性,表明了方法的有效性,并且能够简化协议建模过程和增强AVISPA工具协议描述分析能力。For the transmission of some of protocol messages relies on channels with particular security properties, this paper proposed an extension of AVISPA based on abstract channels. It supplied security guarantees such as authentication by abstract channels, and with which it could model the underlying services providing security guarantees. It realized abstract channels with cryptography schemes and labels, and validated the model by verifying Diffie-Hellman key exchange protocol with message origin authentication using extended AVISPA automatically. The extension can simplify protocol modeling and enhance the power of the mechanized tool AVISPA.

关 键 词：安全协议 形式化分析 安全属性 抽象通道 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]