论文部分内容阅读
文中,在密码系统状态间的关联性和时序逻辑的可达性间建立联系,探讨了一种基于时序逻辑的密钥分配协议的描述办法.该途径从形式上规定密码设备的构成成分以及有关的密码操作,使用了时序逻辑的常量和状态不变量来表达这些构成成分.有关的密码操作表达为状态转换,加密协议应保留的必要特性表达为临界不变性表达式,然后验证这些不变性表达式.本方法的优点在于可以隐式地刻画攻击者的行为,具有形式化程度高等特点.我们希望能为研究规范化、简洁化的形式化分析工具提供一些借鉴.