基于安全协议操作语义模型的组合协议分析及验证  

Formal analysis and verification for compositional protocols based on operational semantics of security protocol

作　　者：高三海[1] 董荣胜[1] 

机构地区：[1]桂林电子科技大学计算机与控制学院,广西桂林541004

出　　处：《桂林电子科技大学学报》2007年第5期378-382,共5页Journal of Guilin University of Electronic Technology

基　　金：广西自然科学基金(054205);广西研究生教育创新计划资助项目(2007105950812M17)

摘　　要：协议的可组合性问题是安全协议形式化分析及验证领域的一个公开问题。通过提出采用安全协议的操作语义模型对组合协议进行形式分析和验证,建立了Yahalom和Denning-Sacco组合协议的操作语义模型,并用基于操作语义模型的自动化验证工具Scyther验证了其安全性,发现了一个针对Yahalom协议机密性的组合攻击。结果表明,操作语义模型是分析与验证组合协议的一种可行方法。Compositionality of security protocol is an open issue in the area of security protocol formal analysis and verification. This paper proposes a new approach for formal analyzing and verifying the compositionality of security protocol. The compositional protocol of Yahalom and Denning-Sacco is modeled as operational semantics model. Its properties are automatically verified by Scyther, which is a tool based on the operational semantics of security protocol. As a result, a new multi-protocol attack to the security of Yahalom protocol is found, which indicates that it is effective in analyzing and checking the property of compositional protocols by operational semantics of security protocol.

关 键 词：组合协议 协议分析 操作语义模型 Scyther 

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