时间相关密码协议逻辑及其形式化语义

摘要：

在密码协议中,主体的认知与信仰状态是随时间推移而不断变化的.为了在协议分析中体现这种动态性,提出一种时间相关密码协议逻辑.该逻辑基于谓词模态逻辑,通过在谓词及模态词中引入时间参数以体现时间因素,使得逻辑可表达各个主体在协议不同时间点的行为、知识及信仰.给出该逻辑的形式化语义,在避免逻辑语言二义性的同时保证了逻辑的可靠性.该语义基于Kripke结构,将可能世界建立在主体局部世界与时间局部世界的基础上,使得任一可能世界能够反映协议的一个可能的全过程.该逻辑为密码协议,特别是时间相关密码协议提供了灵活的分析方法,增强了基于逻辑方法的协议分析能力.

关键词：密码协议、时间相关、谓词模态逻辑、形式化语义

所属期刊栏目：22

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金60873260,60903210;国家高技术研究发展计划8632009AA01Z414;国家重点基础研究发展计划9732007CB311202;江苏省自然科学基金BK2008090

在线出版日期：2011-05-04（万方平台首次上网日期，不代表论文的发表时间）

页数：共24页

页码：534-557