主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
雷新锋,刘军,肖军模.时间相关密码协议逻辑及其形式化语义.软件学报,2011,22(3):534-557
时间相关密码协议逻辑及其形式化语义
Time-Dependent Cryptographic Protocol Logic and Its Formal Semantics
投稿时间:2008-06-23  修订日期:2009-03-30
DOI:10.3724/SP.J.1001.2011.03732
中文关键词:  密码协议  时间相关  谓词模态逻辑  形式化语义
英文关键词:cryptographic protocol  time-dependent  predicate modal logic  formal semantics
基金项目:国家自然科学基金(60873260, 60903210); 国家高技术研究发展计划(863)(2009AA01Z414); 国家重点基础研究发展计划(973)(2007CB311202); 江苏省自然科学基金(BK2008090)
作者单位E-mail
雷新锋 中国科学院 软件研究所 信息安全国家重点实验室,北京 100190
解放军理工大学 通信工程学院,江苏 南京 210007 
leixinfeng@is.iscas.ac.cn 
刘军 解放军理工大学 通信工程学院,江苏 南京 210007  
肖军模 解放军理工大学 通信工程学院,江苏 南京 210007  
摘要点击次数: 3784
全文下载次数: 3930
中文摘要:
      在密码协议中,主体的认知与信仰状态是随时间推移而不断变化的.为了在协议分析中体现这种动态性,提出一种时间相关密码协议逻辑.该逻辑基于谓词模态逻辑,通过在谓词及模态词中引入时间参数以体现时间因素,使得逻辑可表达各个主体在协议不同时间点的行为、知识及信仰.给出该逻辑的形式化语义,在避免逻辑语言二义性的同时保证了逻辑的可靠性.该语义基于Kripke 结构,将可能世界建立在主体局部世界与时间局部世界的基础上,使得任一可能世界能够反映协议的一个可能的全过程.该逻辑为密码协议,特别是时间相关密码协议提供了灵活的分析方法,增强了基于逻辑方法的协议分析能力.
英文摘要:
      In cryptographic protocols, the agent’s epistemic and doxastic states are changeable over time. To model these dynamics, a time-dependent cryptographic protocol logic is proposed. Our logic is based on the predicate modal logic and the time factor can be expressed in it by invoking a time variable as a parameter of predicates and modal operators. This makes it possible to model every agent’s actions, knowledges and beliefs at different time points. We also give the formal semantics of our logic to avoid the ambiguity of its language and make the logic sound. The semantics is based on the kripke structure and the possible world in it is built both on the local world of agent and the specific world of time. This makes every possible world can give a global view of each point of the protocol. Our logic provides a flexible method for analyzing the cryptographic protocols, especially the time-dependent cryptographic protocols, and increases the power of the logical method for analyzing protocols.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利