作　　者： ; ; ; ;

机构地区： 中国科学院研究生院信息安全国家重点实验室

出　　处： 《小型微型计算机系统》 2002年第11期1340-1343,共4页

摘　　要： 文中 ,在密码系统状态间的关联性和时序逻辑的可达性间建立联系 ,探讨了一种基于时序逻辑的密钥分配协议的描述办法 .该途径从形式上规定密码设备的构成成分以及有关的密码操作 ,使用了时序逻辑的常量和状态不变量来表达这些构成成分 .有关的密码操作表达为状态转换 ,加密协议应保留的必要特性表达为临界不变性表达式 ,然后验证这些不变性表达式 .本方法的优点在于可以隐式地刻画攻击者的行为 ,具有形式化程度高等特点 .我们希望能为研究规范化、简洁化的形式化分析工具提供一些借鉴 . In this paper, we made related states contact with the reachability of temporal logic. We proposed formal method to model Key distribution Protocols' properties using the theory of Temporal Logic. It defined encryption device and encryption device and encryption operators in formally. For example, we used temporal logic constants and status invariable to express these factors. Those encryption operators were expressed by states' transitions. Those security conditions were been expressed by some invariant expressions, then proved those expressions. This method can specify intruders' actions stealthily, we argue that using standard temporal logic provides greater formally in the verification results. We hope to provide some help for researching standardization and simplification formal tools.

关 键 词： 时序逻辑 密钥分配协议 协议分析 密码系统

领　　域： [电子电信] [电子电信]