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

操作语义模型是一种用来分析安全协议的新模型,它以操作语义学为基础,结合了多种协议分析模型的优点,能直接分析多个协议的组合问题.本文在对安全协议操作语义模型进行研究的基础上,构建了一个基于结构化操作语义的安全协议分析框架,给出了该框架中的协议规格,协议运行,威胁模型和安全性质等形式化定义.最后,以经典的Needham Schroeder Lowe 协议为例,用该分析框架分析了其机密性和认证性.

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

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.