| 时间相关密码协议逻辑及其形式化语义 |
| |
| 引用本文： | 雷新锋,刘军,肖军模.时间相关密码协议逻辑及其形式化语义[J].软件学报,2011,22(3):534-557. |
| |
| 作者姓名： | 雷新锋 刘军 肖军模 |
| |
| 作者单位： | 1. 中国科学院软件研究所信息安全国家重点实验室,北京,100190;解放军理工大学通信工程学院,江苏南京,210007
2. 解放军理工大学通信工程学院,江苏南京,210007 |
| |
| 基金项目： | 国家自然科学基金(60873260, 60903210); 国家高技术研究发展计划(863)(2009AA01Z414); 国家重点基础研究发展计划(973)(2007CB311202); 江苏省自然科学基金(BK2008090) |
| |
| 摘 要： | 在密码协议中,主体的认知与信仰状态是随时间推移而不断变化的.为了在协议分析中体现这种动态性,提出一种时间相关密码协议逻辑.该逻辑基于谓词模态逻辑,通过在谓词及模态词中引入时间参数以体现时间因素,使得逻辑可表达各个主体在协议不同时间点的行为、知识及信仰.给出该逻辑的形式化语义,在避免逻辑语言二义性的同时保证了逻辑的可靠性.该语义基于Kripke结构,将可能世界建立在主体局部世界与时间局部世界的基础上,使得任一可能世界能够反映协议的一个可能的全过程.该逻辑为密码协议,特别是时间相关密码协议提供了灵活的分析方法,增强了基于逻辑方法的协议分析能力.
|
| 关 键 词： | 密码协议 时间相关 谓词模态逻辑 形式化语义 |
| 收稿时间： | 2008/6/23 0:00:00 |
| 修稿时间： | 2009/3/30 0:00:00 |
Time-Dependent Cryptographic Protocol Logic and Its Formal Semantics |
| |
| LEI Xin-Feng,LIU Jun and XIAO Jun-Mo.Time-Dependent Cryptographic Protocol Logic and Its Formal Semantics[J].Journal of Software,2011,22(3):534-557. |
| |
| Authors: | LEI Xin-Feng LIU Jun and XIAO Jun-Mo |
| |
| Affiliation: | State Key Laboratory of Information Security, Institute of Software, The Chinese Academy of Sciences, Beijing 100190, China; Institute of Communications Engineering, PLA University of Science and Technology, Nanjing 210007, China;Institute of Communications Engineering, PLA University of Science and Technology, Nanjing 210007, China;Institute of Communications Engineering, PLA University of Science and Technology, Nanjing 210007, China |
| |
| Abstract: | |
| |
| Keywords: | cryptographic protocol time-dependent predicate modal logic formal semantics |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
