| 具有时限约束的安全协议分析技术研究 |
| |
| 引用本文： | 董荣胜,彭勋,郭云川,古天龙.具有时限约束的安全协议分析技术研究[J].计算机科学,2005,32(1):80-85. |
| |
| 作者姓名： | 董荣胜 彭勋 郭云川 古天龙 |
| |
| 作者单位： | 桂林电子工业学院计算机系,桂林,541004;桂林电子工业学院计算机系,桂林,541004;桂林电子工业学院计算机系,桂林,541004;桂林电子工业学院计算机系,桂林,541004 |
| |
| 基金项目： | 国家自然科学基金(60243002) |
| |
| 摘 要： | 本文指出了现有时限责任分析技术中存在的缺陷，提出了一种基于Kailar逻辑的安全协议时限责任分析框架。通过该分析框架对一个具有时限性要求的安全电子投递协议进行分析，发现了协议存在的时限问题，修改了协议并给出了修改后的协议满足时限性要求的证明。
|
| 关 键 词： | 形式化方法 时限责任 安全协议 |
On the Analysis of Secure Protocols with Temporal Properties |
| |
| DONG Rong-Sheng,PENG Xun,GUO Yun-Chuan,GU Tian-Long Schoo of Computer Science,Guilin University of Electronic Technology,Guilin.On the Analysis of Secure Protocols with Temporal Properties[J].Computer Science,2005,32(1):80-85. |
| |
| Authors: | DONG Rong-Sheng PENG Xun GUO Yun-Chuan GU Tian-Long Schoo of Computer Science Guilin University of Electronic Technology Guilin |
| |
| Affiliation: | DONG Rong-Sheng,PENG Xun,GUO Yun-Chuan,GU Tian-Long Schoo1 of Computer Science,Guilin University of Electronic Technology,Guilin 541004 |
| |
| Abstract: | 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. |
| |
| Keywords: | Formal methods Temporal accountability Security protocol |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
