使用构造类别代数描述和验证密码协议

Using construct categorical algebra language for formal description of cryptographic protocol

密码协议必须满足安全属性的需求,对密码协议进行形式化规范需要证明其满足该属性。传统的方法或者不利于验证,或者不利于描述。本文在构造类别代数中引入时序算子,对密码协议以及协议的入侵者进行建模,在此基础上利用时序逻辑推导协议应该满足的安全属性。通过在Equicrpt协议上的应用,说明了这是一种解决密码协议描述和验证的行之有效的方法。

The cryptographic protocol should always satisfy security properties, so the formal specification should give the corresponding proof method. The traditional methods may not be suitable for description or not suitable for verification. In this paper, we introduce temporal logic operator into Construct Categorical Algebra for specification and verification of cryptographic protocol, we modeling both the protocol and the intruder, and deduce its security property with the use of temporal logic. With its application on Equicrypt protocol, we conclude that its an effective method on description and verification of cryptographic protocol.