论文部分内容阅读
该文应用了标准时序逻辑来描述密码协议，模拟了入侵者行为，刻画了系统需求正确性。这种途径利用了时序逻辑比ＦＳＭ、Ｐｅｔｒｉ网等模型更易于刻画协议活性性质的特点，该方法将密码系统状态间的关联性和时序逻辑的可达性相对应。该途径从形式上规定密码设备的构成成分以及有关的密码操作，使用了时序逻辑的常量和状态不变量来表达这些构成成分。有关的密码操作表达为状态转换，加密协议应保留的必要特性表达为临界不变性表达式，然后验证这些不变性表达式。整个验证都在统一的逻辑框架体系下进行，形式化程度较高。该文旨在从不同角度探索协议认证性分析方法，为研究规范化、简洁化的形式化分析工具提供一些借鉴。