具有时限约束的安全协议分析技术研究  

On the Analysis of Secure Protocols with Temporal Properties

作　　者：董荣胜[1] 彭勋[1] 郭云川[1] 古天龙[1] 

机构地区：[1]桂林电子工业学院计算机系,桂林541004

出　　处：《计算机科学》2005年第1期80-85,共6页Computer Science

基　　金：国家自然科学基金(60243002)

摘　　要：本文指出了现有时限责任分析技术中存在的缺陷,提出了一种基于Kailar逻辑的安全协议时限责任分析框架。通过该分析框架对一个具有时限性要求的安全电子投递协议进行分析,发现了协议存在的时限问题,修改了协议并给出了修改后的协议满足时限性要求的证明。In this paper,flaws in the temporal accountability logics are analyzed. A new framework based on Kailar's logic is proposed for the analysis of secure protocols that require temporal accountability. Two temporal flaws are de- tected by applying this new framework to analyze a time-critical electronic submission protocol,the protocol is modi- fied and the ability to hold temporal accountability of the protocol is also proved.

关 键 词：时限约束 安全协议分析技术 KAILAR逻辑 形式化方法 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]