基于结构化操作语义的安全协议分析框架研究  

A New Framework Based on Structural Operational Semantics for Analyzing Security Protocol

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

机构地区：[1]桂林电子科技大学计算机系,桂林541004

出　　处：《计算机科学》2007年第8期101-104,176,共5页Computer Science

基　　金：国家自然科学基金项目(60663005);广西自然科学基金项目(0542052)的资助

摘　　要：操作语义模型是一种用来分析安全协议的新模型,它以操作语义学为基础,结合了多种协议分析模型的优点,能直接分析多个协议的组合问题。本文在对安全协议操作语义模型进行研究的基础上,构建了一个基于结构化操作语义的安全协议分析框架,给出了该框架中的协议规格,协议运行,威胁模型和安全性质等形式化定义。最后,以经典的Needham Schroeder Lowe协议为例,用该分析框架分析了其机密性和认证性。Operational semantics of security protocols is a new model for analyzing security protocols,which is based on operational semantics and combines many merits of the current models such as strand spaces model. Further Characteristics of the model is a straightforward handing of parallel of multiple protocols. In this paper, we first study the operational semantics of security protocols, then, based on which a new framework for security protocol is constructed. In this new framework, protocol specification, protocol run, threat model and security requirements are formally defined. Finally, we validate our framework by analyzing the Needham- Schroeder-Lowe protocol.

关 键 词：安全协议 形式化方法 分析框架 操作语义 

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