%0 Journal Article
%T Time-Dependent Cryptographic Protocol Logic and Its Formal Semantics<br>时间相关密码协议逻辑及其形式化语义
%A LEI Xin-Feng
%A LIU Jun
%A XIAO Jun-Mo
%A <br>雷新锋
%A 刘军
%A 肖军模
%J 软件学报
%D 2011
%I 
%X 在密码协议中,主体的认知与信仰状态是随时间推移而不断变化的.为了在协议分析中体现这种动态性,提出一种时间相关密码协议逻辑.该逻辑基于谓词模态逻辑,通过在谓词及模态词中引入时间参数以体现时间因素,使得逻辑可表达各个主体在协议不同时间点的行为、知识及信仰.给出该逻辑的形式化语义,在避免逻辑语言二义性的同时保证了逻辑的可靠性.该语义基于Kripke 结构,将可能世界建立在主体局部世界与时间局部世界的基础上,使得任一可能世界能够反映协议的一个可能的全过程.该逻辑为密码协议,特别是时间相关密码协议提供了灵活的分析方法,增强了基于逻辑方法的协议分析能力.
%K cryptographic protocol
%K time-dependent
%K predicate modal logic
%K formal semantics<br>密码协议
%K 时间相关
%K 谓词模态逻辑
%K 形式化语义
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=F75B56AFE8D483EEE05ECA8934F39569&yid=9377ED8094509821&vid=BC12EA701C895178&iid=38B194292C032A66&sid=D45762219109E903&eid=2E15A588990CC690&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=33