BAN逻辑的可靠性分析与改进

doi:10.3969/j.issn.1000-3428.2012.17.031

计算机工程 ›› 2012, Vol. 38 ›› Issue (17): 110-115. doi: 10.3969/j.issn.1000-3428.2012.17.031

BAN逻辑的可靠性分析与改进

王正才，许道云，王晓峰，唐郑熠，韦立

(贵州大学计算机科学与信息学院，贵阳 550025)

收稿日期:2011-10-11 修回日期:2011-12-05 出版日期:2012-09-05 发布日期:2012-09-03
作者简介:王正才(1977－)，男，博士研究生、CCF会员，主研方向：信息安全，网络安全；许道云，教授、博士生导师；王晓峰、唐郑熠、韦立，博士研究生
基金资助:
国家自然科学基金资助项目(60863005, 61011130038)；贵州大学自然科学青年科研基金资助项目((2009)021)；贵州大学研究生创新基金资助项目(省研理工2010005, 校研理工2011033)

Reliability Analysis and Improvement of BAN Logic

WANG Zheng-cai, XU Dao-yun, WANG Xiao-feng, TANG Zheng-yi, WEI Li

(College of Computer Science & Information, Guizhou University, Guiyang 550025, China)

Received:2011-10-11 Revised:2011-12-05 Online:2012-09-05 Published:2012-09-03

摘要/Abstract

摘要： BAN逻辑的推理过程中可能引入错误的推理条件，导致不安全的协议被验证为安全的。为解决该问题，对消息的形式化描述方式进行改进，在消息含义推理规则中加上一个隐含但不能被忽略的条件，以增强验证的可靠性，通过对发送和推理的消息单元进行限定，使消息新鲜性判定规则适用于更多类型的协议安全性验证。

关键词: BAN逻辑, 安全协议, 形式化, 非形式化, 消息新鲜性, 推理

Abstract: Because an error condition may be added in BAN logic reasoning process, unsafe protocol can be verified safe. In order to solve the problem, this paper improves the formal description of message. An implicit but essential condition is added in the message-meaning inference rule, so that reliability of verification is enhanced. By defining message units of sending and reasoning, freshness rule is suitable to more kinds of protocols in safety verification.

Key words: BAN logic, security protocol, formalization, informalization, message freshness, reasoning

中图分类号:

TP309.2

王正才, 许道云, 王晓峰, 唐郑熠, 韦立. BAN逻辑的可靠性分析与改进[J]. 计算机工程, 2012, 38(17): 110-115.

WANG Zheng-Cai, HU Dao-Yun, WANG Xiao-Feng, TANG Zheng-Yi, HUI Li. Reliability Analysis and Improvement of BAN Logic[J]. Computer Engineering, 2012, 38(17): 110-115.

http://www.ecice06.com/CN/Y2012/V38/I17/110

参考文献

[1] Menezes A, van Oorschot P, Vanstone S. Handbook of Applied Cryptography[M]. New York, USA: CRC Press, 1996.
[2] Nessett D M. Factors Affecting Distributed System Security[J]. IEEE Transactions on Software Engineering, 1987, SE-13(2): 233-248.
[3] Schneier B. Why Cryptography Is Harder than It Looks[J]. Information Security Bulletin, 1997, 2(2): 31-36.
[4] Dolev D, Yao Chi-Chih. On the Security of Public Key Protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208.
[5] Nessett D. A Critique of the Burrows, Abbadi and Needham Logic[J]. Operating Systems Review, 1990, 24(2): 35-38.
[6] Burrows M, Abadi M, Needham R. A Logic of Authentication[J]. ACM Transactions on Computer Systems, 1990, 8(1): 18-36.
[7] Gong Li, Needham R, Yahalom R. Reasoning About Belief in Cryptographic Protocols[C]//Proceedings of IEEE Symposium on Research in Security and Privacy. [S. l.]: IEEE Press, 1990: 234-248.
[8] Cohen M, Dam M. A Completeness Result for BAN Logic[EB/OL]. [2011-06-22]. http://www.access.ee.kth.se/reports/ 2007/13.pdf.
[9] Abdelmajid N T, Hossain M A. Improved Kerberos Security Protocol Evaluation Using Modified BAN Logic[C]//Proc. of the 10th International Conference on Computer and Information Technology. [S. l.]: IEEE Press, 2010: 1610-1615.
[10] 郑东, 王常杰, 王育民. 一种BAN-逻辑的修正[J]. 电子科学学刊, 2000, 22(4): 579-584.
[11] 卿斯汉. 安全协议[M]. 北京: 清华大学出版社, 2005.
[12] 冯彬. 关于BAN 逻辑分析的改进[J]. 中国科学院研究生院学报, 2002, 19(3): 306-310.
[13] Abadi M, Tuttle M. A Semantics for a Logic of Authentication[C]// Proc. of the 10th Annual ACM Symposium on Principles of Distributed Computing. [S. l.]: ACM Press, 1991: 201-216.
[14] Halpern J Y, Pucella R, van Meyden R. Revisiting the Foundations of Authentication Logics[Z]. 2003.
[15] Pucella R. Reasoning About Resource-bounded Knowledge: Theory and Application to Security Protocol Analysis[D]. Ithaca, USA: Cornell University, 2004.
[16] Syverson P F. Towards a Strand Semantics for Authentication Logics[J]. Electronic Notes in Theoretical Computer Science, 1999, 20: 143-157.
[17] 卿斯汉. 密码学与计算机网络安全[M]. 北京: 清华大学出版社, 2001.

选择文件类型/文献管理软件名称

选择包含的内容

BAN逻辑的可靠性分析与改进

Reliability Analysis and Improvement of BAN Logic

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	宋华伟, 屈晓娟, 杨欣, 万方杰. 基于改进YOLOv5的火焰烟雾检测[J]. 计算机工程, 2023, 49(6): 250-256.
[2]	熊中敏, 曾旗, 卢鹏, 王振华, 郑宗生. 基于残差注意力多尺度关系网络的逻辑推理[J]. 计算机工程, 2023, 49(6): 227-233,241.
[3]	郭奕裕, 周箩鱼. 安全帽佩戴检测网络模型的轻量化设计[J]. 计算机工程, 2023, 49(4): 312-320.
[4]	王旖旎, 高永彬, 万卫兵, 杨淑群, 郭茹燕. 结合外部知识库与适应性推理的场景图生成模型[J]. 计算机工程, 2022, 48(9): 230-238.
[5]	周文康, 王行甫. 一种基于AHP和FIS的WSN路由算法[J]. 计算机工程, 2022, 48(3): 131-138,161.
[6]	高峰, 姚光涛, 顾进广. 基于改进多嵌入空间的实时语义数据流推理[J]. 计算机工程, 2022, 48(2): 55-64.
[7]	邹品荣, 肖锋, 张文娟, 张万玉, 王晨阳. 面向视觉问答的多模块协同注意模型[J]. 计算机工程, 2022, 48(2): 250-260.
[8]	刘先锋, 梁赛, 李强, 张锦. 基于深度强化学习的云边协同DNN推理[J]. 计算机工程, 2022, 48(11): 30-38.
[9]	闫倩倩, 缪炜恺. 轨道交通控制软件中基于场景的需求分析方法[J]. 计算机工程, 2021, 47(8): 284-293,300.
[10]	李鑫柏, 吴鑫然, 岳昆. 基于贝叶斯网的开放世界知识图谱补全[J]. 计算机工程, 2021, 47(6): 104-114.
[11]	杨锦翔, 熊焰, 黄文超. 基于强化学习的安全协议形式化验证优化研究[J]. 计算机工程, 2021, 47(12): 141-146.
[12]	黄靖淞, 左颢睿, 张建林. 轻量化目标检测算法研究及应用[J]. 计算机工程, 2021, 47(10): 236-241.
[13]	李世宝, 李贺, 赵庆帅, 殷乐乐, 刘建航, 黄庭培. 融合外部语义知识的中文文本蕴含识别[J]. 计算机工程, 2021, 47(1): 44-49.
[14]	夏锐, 钱振江, 刘苇. 一种基于Isabelle/HOL的安全通信协议验证方法[J]. 计算机工程, 2021, 47(1): 146-153.
[15]	黄廷辉, 丁勇, 李思骏. 基于MT6D的物联网轻量级安全协议研究[J]. 计算机工程, 2020, 46(9): 117-122.

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

BAN逻辑的可靠性分析与改进

Reliability Analysis and Improvement of BAN Logic

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价