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

针对AVISPA工具在分析某些消息需要依靠具有特定属性的信道传递的安全协议或服务中存在的问题, 提出了一种基于抽象通道的扩展方法。抽象通道具有相关的安全性质保证如认证性, 能够对提供安全性质保证的底层服务建模, 并基于密码机制和标签等实现了抽象通道。利用扩展后的AVISPA工具分析有无消息源认证机制的Diffie-Hellman密钥交换协议的安全性, 表明了方法的有效性, 并且能够简化协议建模过程和增强AVISPA工具协议描述分析能力。

Extension of AVISPA based on concept of channels

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.