基于时间戳私钥签名技术的Nayak-T协议安全性分析
|
摘要
随着信息网络的快速发展,云服务走进人们视野,云环境下信息安全问题成为人们关注的焦点。Nayak协议是一种云环境下基于口令身份认证,实现双向认证和会话密钥交换的协议。针对Nayak协议存在的中间人攻击,提出改进协议Nayak-T。Nayak-T协议在消息项内增加时间戳并更改加密手段,通过双重加密的手段来保证双方通信安全。利用四通道并行建模法对Nayak-T协议建模,运用SPIN对该协议进行验证,验证结果得出Nayak-T协议安全的结论。模型优化策略分析表明,采用静态分析、类型检查、语法重定序模型优化策略的模型检测效率最佳,可运用于类似复杂协议的形式化分析与验证。
With the rapid development of information networks,cloud services step into people's vision and the problems of information security in the cloud environment become a focus.Nayak protocol is a password authentication scheme based on the bidirectional authentication and session key agreement in the cloud environment.Targeting at man-in-the-middle attacks existing in Nayak protocol,we put forward an improved Nayak-T protocol.Nayak-T protocol adds in time stamp and changes their encryption ways inside message options to ensure the security of two-way communication through double encryption.We use the four channels parallel modeling method to model Nayak-T protocol and adopt SPIN to verify the security of this protocol.Analysis of modeling optimization strategies proves that the model testing that adopts static analysis,type checking and syntax reordering are most efficient.This method can be applied to the formal analysis and verification of similar complicated protocols.
With the rapid development of information networks,cloud services step into people's vision and the problems of information security in the cloud environment become a focus.Nayak protocol is a password authentication scheme based on the bidirectional authentication and session key agreement in the cloud environment.Targeting at man-in-the-middle attacks existing in Nayak protocol,we put forward an improved Nayak-T protocol.Nayak-T protocol adds in time stamp and changes their encryption ways inside message options to ensure the security of two-way communication through double encryption.We use the four channels parallel modeling method to model Nayak-T protocol and adopt SPIN to verify the security of this protocol.Analysis of modeling optimization strategies proves that the model testing that adopts static analysis,type checking and syntax reordering are most efficient.This method can be applied to the formal analysis and verification of similar complicated protocols.
引文
[1]Xiao M,Jiang Y,Liu Q.On formal analysis of cryptographic protocols and supporting tool[J].Chinese Journal of Electronics,2010,19(2):223-228.
[2]Clarke E M,Grumberg O,Peled D A.Model checking[M].Cambridge,MA:MIT Press,1999.
[3]Xiao Mei-hua,Ma Cheng-lin,Deng Chun-yan,et al.A novel approach to automatic security protocol analysis based on authentication event logic[J].Chinese Journal of Electronics,2015,24(1):187-192.
[4]Holzmann G J.The model checker SPIN[J].IEEE Transactions on Software Engineering,1997,23(5):279-295.
[5]Xiao Mei-hua,Wan Zi-long,Liu Hong-ling.The formal verification and improvement of simplified SET protocol[J].Journal of Software,2014,9(9):2302-2308.
[6]Nayak S K,Mohapatra S,Majhi B.An improved mutual authentication framework for cloud computing[J].International Journal of Computer Applications,2012,52(5):36-41.
[7]Zhan Li.The research and formal analysis on mutual authentication protocol in cloud computing based on Smartcard[D].Guangzhou:Jinan University,2014.(in Chinese)
[8]Yang Shi-ping.Analysis and research on security protocol and BAN logic[D].Guiyang:Guizhou University,2007.(in Chinese)
[9]Ma Cheng-lin,Xiao Mei-hua,Deng Chun-yan,et al.Security analysis of the kerberos*protocol based on the modified GNY logic[J].Computer&Digital Engineering,2014,24(10):1758-1762.(in Chinese)
[10]Li Jian-wen.Researches on some fundamental problems of linear temporal logic[D].Shanghai:East China Normal University,2014.(in Chinese)
[11]Zhang Shuai.Research on trusted time stamp service system based on authentication[D].Beijing:University of Chinese Academy of Sciences,2016.(in Chinese)
[12]Zhao Jing,Li Xin,Deng Ling-juan,et al.A selection method for user authentication protocols in wireless networks[J].Journal of Computer Research&Development,2015,52(3):671-680.(in Chinese)
[13]Yu Xiao-chen.The design and implementation of dynamic password identity authentication scheme[D].Dalian:Dalian University of Technology,2014.(in Chinese)
[14]Dolev D,Yao A C.On the security of public key protocols[J].IEEE Transactions on Information Theory,1983,29(2):198-208.
[15]Xiong Hao.Study of some key issues on method checking in formal scheme analysis[D].Nanchang:Nanchang University,2008.(in Chinese)
[16]Wang Wan-kuo.The state space reduction based on partial order technology and its application in concurrent system[D].Guiyang:Guizhou University,2015.(in Chinese)
[7]詹丽.云计算中基于Smartcard的双向认证安全协议的研究及形式化分析[D].广州:暨南大学,2014.
[8]杨世平.安全协议及其BAN逻辑分析研究[D].贵阳:贵州大学,2007.
[9]马成林,肖美华,邓春艳,等.基于改进GNY逻辑的Kerberos*协议安全性分析[J].计算机与数字工程,2014,24(10):1758-1762.
[10]李建文.线性时态逻辑中若干基础问题的研究[D].上海:华东师范大学,2014.
[11]张帅.一种基于身份认证的可信时间戳服务体系研究[D].北京:中国科学院研究生院,2016.
[12]赵婧,李鑫,邓凌娟,等.无线网络中身份认证协议选择方法[J].计算机研究与发展,2015,52(3):671-680.
[13]于晓晨.一种动态口令身份认证方案的设计与实现[D].大连:大连理工大学,2014.
[15]熊昊.模型检测形式化分析中若干关键问题研究[D].南昌:南昌大学,2008.
[16]王万括.并发系统中基于偏序规约的状态空间约简与应用[D].贵阳:贵州大学,2015.
[2]Clarke E M,Grumberg O,Peled D A.Model checking[M].Cambridge,MA:MIT Press,1999.
[3]Xiao Mei-hua,Ma Cheng-lin,Deng Chun-yan,et al.A novel approach to automatic security protocol analysis based on authentication event logic[J].Chinese Journal of Electronics,2015,24(1):187-192.
[4]Holzmann G J.The model checker SPIN[J].IEEE Transactions on Software Engineering,1997,23(5):279-295.
[5]Xiao Mei-hua,Wan Zi-long,Liu Hong-ling.The formal verification and improvement of simplified SET protocol[J].Journal of Software,2014,9(9):2302-2308.
[6]Nayak S K,Mohapatra S,Majhi B.An improved mutual authentication framework for cloud computing[J].International Journal of Computer Applications,2012,52(5):36-41.
[7]Zhan Li.The research and formal analysis on mutual authentication protocol in cloud computing based on Smartcard[D].Guangzhou:Jinan University,2014.(in Chinese)
[8]Yang Shi-ping.Analysis and research on security protocol and BAN logic[D].Guiyang:Guizhou University,2007.(in Chinese)
[9]Ma Cheng-lin,Xiao Mei-hua,Deng Chun-yan,et al.Security analysis of the kerberos*protocol based on the modified GNY logic[J].Computer&Digital Engineering,2014,24(10):1758-1762.(in Chinese)
[10]Li Jian-wen.Researches on some fundamental problems of linear temporal logic[D].Shanghai:East China Normal University,2014.(in Chinese)
[11]Zhang Shuai.Research on trusted time stamp service system based on authentication[D].Beijing:University of Chinese Academy of Sciences,2016.(in Chinese)
[12]Zhao Jing,Li Xin,Deng Ling-juan,et al.A selection method for user authentication protocols in wireless networks[J].Journal of Computer Research&Development,2015,52(3):671-680.(in Chinese)
[13]Yu Xiao-chen.The design and implementation of dynamic password identity authentication scheme[D].Dalian:Dalian University of Technology,2014.(in Chinese)
[14]Dolev D,Yao A C.On the security of public key protocols[J].IEEE Transactions on Information Theory,1983,29(2):198-208.
[15]Xiong Hao.Study of some key issues on method checking in formal scheme analysis[D].Nanchang:Nanchang University,2008.(in Chinese)
[16]Wang Wan-kuo.The state space reduction based on partial order technology and its application in concurrent system[D].Guiyang:Guizhou University,2015.(in Chinese)
[7]詹丽.云计算中基于Smartcard的双向认证安全协议的研究及形式化分析[D].广州:暨南大学,2014.
[8]杨世平.安全协议及其BAN逻辑分析研究[D].贵阳:贵州大学,2007.
[9]马成林,肖美华,邓春艳,等.基于改进GNY逻辑的Kerberos*协议安全性分析[J].计算机与数字工程,2014,24(10):1758-1762.
[10]李建文.线性时态逻辑中若干基础问题的研究[D].上海:华东师范大学,2014.
[11]张帅.一种基于身份认证的可信时间戳服务体系研究[D].北京:中国科学院研究生院,2016.
[12]赵婧,李鑫,邓凌娟,等.无线网络中身份认证协议选择方法[J].计算机研究与发展,2015,52(3):671-680.
[13]于晓晨.一种动态口令身份认证方案的设计与实现[D].大连:大连理工大学,2014.
[15]熊昊.模型检测形式化分析中若干关键问题研究[D].南昌:南昌大学,2008.
[16]王万括.并发系统中基于偏序规约的状态空间约简与应用[D].贵阳:贵州大学,2015.