两个认证密钥协商协议的前向安全性分析  

Cryptoanalysis on the Forward Security of Two Authenticated Key Protocols

作　　者：程庆丰[1] 马玉千 CHENG Qingfeng;MA Yuqian(Strategic Support Force Information Engineering University,Zhengzhou 450001,China;State Key Laboratory of Mathematical Engineering and Advanced Computing,Zhengzhou 450001,China)

机构地区：[1]战略支援部队信息工程大学,郑州450001 [2]数学工程与先进计算国家重点实验室,郑州450001

出　　处：《电子与信息学报》2022年第12期4294-4303,共10页Journal of Electronics & Information Technology

基　　金：国家自然科学基金(61872449)。

摘　　要：目前,网络安全及隐私受到广泛关注。前向安全性是Günther在1989年提出的一种认证密钥协商协议(AKA)的安全属性(doi:10.1007/3-540-46885-4_5),该性质经过30年的蓬勃发展已经成为研究领域的热点之一。该文主要分析了MZK20和VSR20两个AKA协议。首先在启发式分析的基础上,利用BAN逻辑分析了MZK20协议不具有弱前向安全性;其次利用启发式分析和Scyther工具证明了VSR20协议不具备前向安全性。最后,在分析VSR20协议设计缺陷的基础上,提出了改进方案,并在eCK模型下证明了改进后协议的安全性;并且,结合Scyther软件证明了改进VSR20协议与VSR20协议相比明显提高了安全性。At present,network security and privacy have attracted extensive attention.Forward security is a security attribute of Authenticated Key Agreement protocol(AKA)proposed by Günther in 1989.Since then,this property has become one of the hot topics.This paper analyzes the security properties of two AKA protocols,MZK20 and VSR20.First,based on heuristic analysis and BAN logic,MZK20 protocol is proved that it does not satisfy weak forward security.Second,using heuristic analysis and Scyther,it is proved that VSR20 protocol does not fulfill forward security.Finally,the enhanced VSR20 protocol is designed and proved more secure than VSR20.The security of the modified VSR20 is verified both by the use of security reduction under eCK model and Scyther.

关 键 词：安全协议形式化工具分析 认证密钥协商协议 前向安全性 

分 类 号：TN918[电子电信—通信与信息系统] TP309[电子电信—信息与通信工程]