一种改进的Woo-Lam密码协议模型

提出了一种改进的Woo-Lam密码协议模型，即eWoo-Lam模型。与Woo-Lam模型相比，新模型具有以下特点：增强了模型中关于密码学原语操作的描述语法，使得对密码协议主体行为的描述更加精确，提高了模型在检测协议攻击方面的能力； 引入了匹配运算机制，保障了模型安全性证明的有效性； 提出了七条形式化准则，规范了模型的抽象过程； 扩充了模型基于状态迁移的形式语义，使其更加精确合理； 重新给出了模型安全性的形式定义，使其更具一般性。

Improved Woo-Lam model for cryptographic protocols

An improved Woo-Lam Model for cryptographic protocols,namely eWoo-Lam Model was introduced.Compared with Woo-Lam Model,the new model has such advanced properties as follows: to enhance the syntax of the model for cryptographic primitives,which enables the model to specify the principal actions more precisely and detect the attacks on the protocol more efficiently;to bring in match mechanism,which guarantees the effectiveness for the security analysis of the model;to propose seven formalization principles to normalize the procedure for model abstraction;to extend the state-transition based semantics to make it more rational;to redefine the security properties of the model to make them more generic.