[1]黎波涛,罗军舟.不可否认协议形式化分析的SVO逻辑方法[J].东南大学学报(自然科学版),2005,35(5):688-691.[doi:10.3969/j.issn.1001-0505.2005.05.007]
 Li Botao,Luo Junzhou.Formal analysis of non-repudiation protocols with SVO logic[J].Journal of Southeast University (Natural Science Edition),2005,35(5):688-691.[doi:10.3969/j.issn.1001-0505.2005.05.007]
点击复制

不可否认协议形式化分析的SVO逻辑方法()
分享到:

《东南大学学报(自然科学版)》[ISSN:1001-0505/CN:32-1178/N]

卷:
35
期数:
2005年第5期
页码:
688-691
栏目:
计算机科学与工程
出版日期:
2005-09-20

文章信息/Info

Title:
Formal analysis of non-repudiation protocols with SVO logic
作者:
黎波涛 罗军舟
东南大学计算机科学与工程系, 南京 210096
Author(s):
Li Botao Luo Junzhou
Department of Computer Science and Engineering, Southeast University, Nanjing 210096, China
关键词:
不可否认 公平性 SVO逻辑 形式化分析
Keywords:
non-repudiation fairness SVO logic formal analysis
分类号:
TP393
DOI:
10.3969/j.issn.1001-0505.2005.05.007
摘要:
使用SVO逻辑对Zhou-Gollmann的公平不可否认协议的一个改进协议进行了形式化分析.在分析该协议的过程中,分析了使用SVO逻辑分析不可否认协议时存在的一些问题,这是分析过程无法发现Zhou-Gollmann不可否认协议的原因.这些问题包括协议目标的确定,协议时限性的描述与分析,协议初始假设集的确定等.分析协议时,不仅需要证明协议的最终目标,还需要证明中间目标.通过对SVO逻辑的语法进行扩展,使其具有显式的时间描述能力,从而能够分析不可否认协议的时限性.
Abstract:
A new improvement of Zhou-Gollmann’s fair non-repudiation protocol is analyzed with SVO logic. Some problems in the analysis of non-repudiation protocols using SVO logic, which are the causes why the flaw of Zhou-Gollmann’s fair non-repudiation cannot be discovered, are discussed. These problems include determination of protocol goals, analysis of timeliness property of protocols and premise set establishment. In the analysis, both the final goals and the intermediary goals need to be proved. By extending the syntax of SVO logic, a time description method is added into it and, thus the timeliness of non-repudiation protocols can be analyzed.

参考文献/References:

[1] Kremer S, Markowitch O,Zhou J.An intensive survey of non-repudiation protocols [J]. Computer Communications,2002,25(17):1606-1621.
[2] Zhou J,Gollmann D.A fair non-repudiation protocol [A].In:Proceedings of 1996 IEEE Symposium on Security and Privacy [C].Los Alamitos,CA,1996.55-61.
[3] Zhou J,Gollmann D.Towards verification of non-repudiation protocols [A].In: Proceedings of 1998 International Refinement Workshop and Formal Methods Pacific [C].Canberra,Australia,1998.370-380.
[4] Schneider S.Formal analysis of a non-repudiation protocol [A].In: Proceedings of 11th IEEE Computer Security Foundations Workshop [C].Rockport,Massachusetts,USA,1998.54-65.
[5] Kim K,Park S,Baek J.Improving fairness and privacy of Zhou-Gollmann’s fair non-repudiation protocol [A].In: Proceedings of 2000 IEEE International Conference on Communication [C].New Orleans,USA,2000.1743-1747.
[6] Li Botao,Luo Junzhou.On timeliness of a fair non-repudiation protocol [A].In: Proceedings of the 3rd International Conference on Information Security(InfoSecu’04) [C].Shanghai,2004.99-107.
[7] Syverson P F,van Oorscho P C.On unifying some cryptographic protocol logics [A].In:Proceedings of 1994 IEEE Computer Society Symposium on Security and Privacy [C].Los Alamitos,CA,1994.14-28.
[8] Syverson P F,van Oorschot P C. A unified cryptographic protocol logic [M].TR:NRL Publication 5540-227,1996.
[9] Burrows M,Abadi M,Needham R.A logic of authentication [J].ACM Transactions in Computer Systems,1990,8(1):18-36.

相似文献/References:

[1]屠昊,纪其进,董永强.自适应虚拟队列算法AVQ的公平性研究[J].东南大学学报(自然科学版),2005,35(4):528.[doi:10.3969/j.issn.1001-0505.2005.04.007]
 Tu Hao,Ji Qijin,Dong Yongqiang.Study on fairness of adaptive virtual queue algorithm[J].Journal of Southeast University (Natural Science Edition),2005,35(5):528.[doi:10.3969/j.issn.1001-0505.2005.04.007]
[2]冯径,徐攀,王锦洲,等.一种多策略要素的数据访问调度算法[J].东南大学学报(自然科学版),2012,42(5):820.[doi:10.3969/j.issn.1001-0505.2012.05.005]
 Feng Jing,Xu Pan,Wang Jinzhou,et al.Multi-policy element scheduling algorithm for data access[J].Journal of Southeast University (Natural Science Edition),2012,42(5):820.[doi:10.3969/j.issn.1001-0505.2012.05.005]

备注/Memo

备注/Memo:
基金项目: 江苏省“网络与信息安全”重点实验室计划资助项目(BM20033201)、江苏省高技术研究资助项目(BG2004036).
作者简介: 黎波涛(1976—),男,博士生,lepert@seu.edu.cn; 罗军舟(联系人),男,博士,教授,博士生导师,jluo@seu.edu.cn.
更新日期/Last Update: 2005-09-20