一种改进的NSSK认证协议及其实现方法
|
摘要
为了保障开源的网络通讯产品如实时消息系统、网络电话等能够在高安全领域得以应用,本文对著名的NeedhamSchroeder(NS)认证协议进行改进和优化,优化后的协议通过采用使接收方与密钥分发中心通信、在密钥分发中心返回的消息中添加发送方身份和各方发送的临时值的方式,达到了确保消息新鲜性、通信双方身份及会话中共享密钥可靠性的目的,同时避免了原生NS协议存在的旧消息重传攻击和身份冒充缺陷.利用模态逻辑BAN逻辑,对改进版的协议进行理想化建模、定义初始假设集合及安全目标集合,并在此基础上使用推理规则,证明了该改进协议完全能够达到认证协议的安全目标.通过硬件及其对应的工具包,实现了该认证协议,并在实际应用中验证.
This paper improves and optimizes the famous Needham-Schroeder(NS) authentication protocol in order to ensure that open source network communication products such as real-time messaging system and Internet telephony can be applied in high security field. The optimized protocol achieves the way to ensure that the message is fresh,the identity of both parties,and the purpose of sharing the secret key in the session by adding the sender's identity and the temporary value sent by the parties by communicating the recipient with the secret key distribution center and the message returned by the secret key distribution center.. While avoiding the existence of the original NS protocol retransmission of old messages and identity posing defects. By using the modal logic BAN logic,the improved version of the protocol is ideally modeled,the initial hypothesis set and the security target set are defined. Based on this,the reasoning rule is used to prove that the improved protocol can achieve the security goal of the authentication protocol. Through the hardware and its corresponding toolkit,achieving and verifying authentication protocol in practical.
This paper improves and optimizes the famous Needham-Schroeder(NS) authentication protocol in order to ensure that open source network communication products such as real-time messaging system and Internet telephony can be applied in high security field. The optimized protocol achieves the way to ensure that the message is fresh,the identity of both parties,and the purpose of sharing the secret key in the session by adding the sender's identity and the temporary value sent by the parties by communicating the recipient with the secret key distribution center and the message returned by the secret key distribution center.. While avoiding the existence of the original NS protocol retransmission of old messages and identity posing defects. By using the modal logic BAN logic,the improved version of the protocol is ideally modeled,the initial hypothesis set and the security target set are defined. Based on this,the reasoning rule is used to prove that the improved protocol can achieve the security goal of the authentication protocol. Through the hardware and its corresponding toolkit,achieving and verifying authentication protocol in practical.
引文
[1]Lei Xin-feng,Song Shu-min,Liu Wei-bing,et al.A srvey on computationally sound formal analysis of cryptographic[J].Chinese Journal of Computers,2014,37(5):993-1016.
[2]Hu Xiao-hui,Chen Hui-li,Shi Guang-tian,et al.Formal modeling and verification of CTCS-4 security[J].Computer Engineering and Applications,2014,50(4):81-85.
[3]Liu S M,Ye J Y,Wang Y L.Improvement and security analysis on symmetric key authentication needham-schroeder[J].Applied M echanics&M aterials,2014,513-517:1289-1293.
[4]Lai Y,Chen Y,Zou Q,et al.Design and analysis on trusted netw ork equipment access authentication[J].Simulation M odelling Practice&Theory,2015,51(51):157-169.
[5]Wang Zheng-cai,Xu Dao-yun,Wang Xiao-feng,et al.Reliability analysis and improvement of BAN logic[J].Computer Engineering,2012,38(17):110-115.
[6]Lu Si-qi,Cheng Qing-feng,Zhao Jin-hua.Comparison study of formal verification tools for security protocols[J].Journal of Cryptologic Research,2014,1(6):568-577.
[7]Xue Rui,Feng Deng-guo.A survey on formal analysis of security[J].Journal of Cryptologic Research,2014,1(5):504-512.
[8]Xue Rui,Lei Xin-feng.Present status and trends of researches on analyses of security[J].Bulletin of Chinese Academy of Sciences,2011,(3):287-296.
[9]Shi Guang-tian,Chen Hui-li.Formal analysis and verification of a new improved NSSK protocol[C].Proceedings of the 2014 International Conference on E-Commerce,E-Business and E-Service(EEE 2014),Information Engineering Research Institute,USA,2014:20-24.
[10]Needham R M,Schroeder M D.Using encryption for authentication in large netw orks of computers[J].Communications of the ACM,1978,21(12):993-999.
[11]Wang Kun,Zhou Qing-lei.RFID mutual authentication protocol of new internet of things[J].Journal of Chinese Computer Systems,2015,36(4):732-738.
[12]Cai Da-zhuang,Yang Hai-bo.Research on a secure communication model for IM S assess layer using tw o-stage DH algorithm[J].Journal of Chinese Computer Systems,2016,37(4):782-786.
[13]Shao Fei,Meng Bo.A Non-interactive deniable authentication protocol based on elliptic curve discrete logarithm problem[J].Journal of Chinese Computer Systems,2014,35(1):89-92.
[1]雷新锋,宋书民,刘伟兵,等.计算可靠的密码协议形式化分析综述[J].计算机学报,2014,37(5):993-1016.
[2]胡晓辉,陈慧丽,石广田,等.CTCT-4级安全通信协议的形式化建模与验证[J].计算机工程与应用,2014,50(4):81-85.
[5]王正才,许道云,王晓峰,等.BAN逻辑的可靠性分析与改进[J].计算机工程,2012,38(17):110-115.
[6]陆思奇,程庆丰,赵进华.安全协议形式化分析工具比较研究[J].密码学报,2014,1(6):568-577.
[8]薛锐,雷新锋.安全协议:信息安全保障的灵魂—安全协议分析研究现状与发展趋势[J].中国科学院院刊,2011,(3):287-296.
[11]王坤,周清雷.新物联网下的RFID双向认识协议[J].小型微型计算机系统,2015,36(4):732-738.
[12]才大壮,杨海波.使用两阶段DH算法的IMS接入侧安全通信模型研究[J].小型微型计算机系统,2016,37(4):782-786.
[13]邵飞,孟博.一种基于椭圆曲线离散对数问题的非交互式可否认认证协议[J].小型微型计算机系统,2014,35(1):89-92.
[2]Hu Xiao-hui,Chen Hui-li,Shi Guang-tian,et al.Formal modeling and verification of CTCS-4 security[J].Computer Engineering and Applications,2014,50(4):81-85.
[3]Liu S M,Ye J Y,Wang Y L.Improvement and security analysis on symmetric key authentication needham-schroeder[J].Applied M echanics&M aterials,2014,513-517:1289-1293.
[4]Lai Y,Chen Y,Zou Q,et al.Design and analysis on trusted netw ork equipment access authentication[J].Simulation M odelling Practice&Theory,2015,51(51):157-169.
[5]Wang Zheng-cai,Xu Dao-yun,Wang Xiao-feng,et al.Reliability analysis and improvement of BAN logic[J].Computer Engineering,2012,38(17):110-115.
[6]Lu Si-qi,Cheng Qing-feng,Zhao Jin-hua.Comparison study of formal verification tools for security protocols[J].Journal of Cryptologic Research,2014,1(6):568-577.
[7]Xue Rui,Feng Deng-guo.A survey on formal analysis of security[J].Journal of Cryptologic Research,2014,1(5):504-512.
[8]Xue Rui,Lei Xin-feng.Present status and trends of researches on analyses of security[J].Bulletin of Chinese Academy of Sciences,2011,(3):287-296.
[9]Shi Guang-tian,Chen Hui-li.Formal analysis and verification of a new improved NSSK protocol[C].Proceedings of the 2014 International Conference on E-Commerce,E-Business and E-Service(EEE 2014),Information Engineering Research Institute,USA,2014:20-24.
[10]Needham R M,Schroeder M D.Using encryption for authentication in large netw orks of computers[J].Communications of the ACM,1978,21(12):993-999.
[11]Wang Kun,Zhou Qing-lei.RFID mutual authentication protocol of new internet of things[J].Journal of Chinese Computer Systems,2015,36(4):732-738.
[12]Cai Da-zhuang,Yang Hai-bo.Research on a secure communication model for IM S assess layer using tw o-stage DH algorithm[J].Journal of Chinese Computer Systems,2016,37(4):782-786.
[13]Shao Fei,Meng Bo.A Non-interactive deniable authentication protocol based on elliptic curve discrete logarithm problem[J].Journal of Chinese Computer Systems,2014,35(1):89-92.
[1]雷新锋,宋书民,刘伟兵,等.计算可靠的密码协议形式化分析综述[J].计算机学报,2014,37(5):993-1016.
[2]胡晓辉,陈慧丽,石广田,等.CTCT-4级安全通信协议的形式化建模与验证[J].计算机工程与应用,2014,50(4):81-85.
[5]王正才,许道云,王晓峰,等.BAN逻辑的可靠性分析与改进[J].计算机工程,2012,38(17):110-115.
[6]陆思奇,程庆丰,赵进华.安全协议形式化分析工具比较研究[J].密码学报,2014,1(6):568-577.
[8]薛锐,雷新锋.安全协议:信息安全保障的灵魂—安全协议分析研究现状与发展趋势[J].中国科学院院刊,2011,(3):287-296.
[11]王坤,周清雷.新物联网下的RFID双向认识协议[J].小型微型计算机系统,2015,36(4):732-738.
[12]才大壮,杨海波.使用两阶段DH算法的IMS接入侧安全通信模型研究[J].小型微型计算机系统,2016,37(4):782-786.
[13]邵飞,孟博.一种基于椭圆曲线离散对数问题的非交互式可否认认证协议[J].小型微型计算机系统,2014,35(1):89-92.