一种分析Timed-Release公钥协议的扩展逻辑

An Extension Logic of Timed-Release Public Key Protocols Analysis

在Coffey和Saidha提出的CS逻辑 (CS逻辑将时间与逻辑结构相结合 ,可用于形式化分析Timed release公钥协议的时间相关性秘密的安全性 )的基础上 ,提出了CS逻辑的扩展逻辑 ,它更好地反映了Timed release公钥协议的特性 ,并对一个协议实例进行了有效的形式化分析 .

Timed release public key protocol can provide time dependent secrets by using public key cryptographic system through standard time provided by the trusted third party. The formal analysis of this kind of protocols needs special logic system which can reflect its properties. Coffey & Saidha have proposed a logic system to formally analyze the timed release public key protocols, which is called CS logic. CS logic adds the time into logic structure, so it can be used to analyze the security of time dependent secrets of timed release public key cryptographic protocols. This paper presents an extension of CS logic which reflects the properties of timed release public key protocols better, and gives a good formal analysis of a concrete protocol.