CS逻辑的分析及改进

The analysis and the modification of the CS logic

较之以往的形式化分析工具BAN及BAN类逻辑,CS逻辑是一种将时间与逻辑结构相结合的逻辑,是第一个用来分析与时间相关的Timed--release公钥协议的逻辑,本文分析了原始CS逻辑的某些推理规则的缺陷,并对其作了改进及扩展,使其能够更好地反映Timed--release公钥协议的特性,并对一个具体的Timed-release公钥协议用扩展后的推理规则进行了有效的形式化分析.

Compared with the existed analysis tools BAN and BAN-like, the CS Logic is a logic that combining time and logic structure. It is the first logic to be used to analyse Timed-release Cryptographic protocols that related to time. Some defects of the inference rules in former CS logic were analysed, modified and expanded to reflect the characters of Timed-release cryptographic protocols better. And finally, a specific Timed-release cryptographic protocol was analysed effectively by using these improved inference rules.