基于时间戳私钥签名技术的Nayak-T协议安全性分析

计算机工程与科学

基于时间戳私钥签名技术的Nayak-T协议安全性分析

肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1

（1.华东交通大学软件学院，江西南昌 330013；2.池州职业技术学院，安徽池州 247100）

收稿日期:2017-07-10 修回日期:2017-09-16 出版日期:2017-12-25 发布日期:2017-12-25
基金资助:
国家自然科学基金（61163005，61562026）;江西省自然科学基金(20161BAB202063）；江西省对外科技合作项目（20151BDH80005）;江西省主要学科学术和技术带头人资助计划（2017BCB22015）

Security analysis of Nayak-T protocol

based on time stamp and private key signature

XIAO Mei-hua1,MEI Ying-tian1,2,LI Wei1,LI Ya-nan1,ZHONG Xiao-mei1,SONG Zi-fan1

(1.School of Software,East China Jiaotong University,Nanchang 330013;

2.Chizhou Vocational and Technical College,Chizhou 247100,China)

Received:2017-07-10 Revised:2017-09-16 Online:2017-12-25 Published:2017-12-25

摘要/Abstract

摘要：

随着信息网络的快速发展，云服务走进人们视野，云环境下信息安全问题成为人们关注的焦点。Nayak协议是一种云环境下基于口令身份认证，实现双向认证和会话密钥交换的协议。针对Nayak协议存在的中间人攻击，提出改进协议Nayak-T。Nayak-T协议在消息项内增加时间戳并更改加密手段，通过双重加密的手段来保证双方通信安全。利用四通道并行建模法对Nayak-T协议建模，运用SPIN对该协议进行验证，验证结果得出Nayak-T协议安全的结论。模型优化策略分析表明，采用静态分析、类型检查、语法重定序模型优化策略的模型检测效率最佳，可运用于类似复杂协议的形式化分析与验证。

关键词: Nayak协议, Nayak-T协议, 模型检测, 私钥签名, 时间戳

Abstract:

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.

Key words: Nayak protocol, Nayak-T protocol, model checking, private key signature, time stamp

肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学.

XIAO Mei-hua1,MEI Ying-tian1,2,LI Wei1,LI Ya-nan1,ZHONG Xiao-mei1,SONG Zi-fan1.

Security analysis of Nayak-T protocol

based on time stamp and private key signature

[J]. Computer Engineering & Science.

[1]	刘子源, 马占有, 李霞, 高滢囡, 何娜娜, 黄瑞祺. 基于模糊测度的模糊分支时态逻辑模型检测[J]. 计算机工程与科学, 2024, 46(04): 676-683.
[2]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[3]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[4]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[5]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[6]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[7]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[8]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[9]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.
[10]	程道雷,肖美华,刘欣倩,梅映天,李伟. 运用SPIN对开放授权协议OAuth 2.0的分析与验证[J]. J4, 2015, 37(11): 2121-2127.
[11]	马占有1，2，李永明1. 广义可能性决策过程的计算树逻辑模型检测[J]. J4, 2015, 37(11): 2162-2168.
[12]	刘姣，雷丽晖. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法[J]. J4, 2015, 37(10): 1884-1889.
[13]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[14]	周璇,汪学明. 微支付协议Millicent的改进与模型检测[J]. J4, 2012, 34(12): 22-26.
[15]	陈国彬1，任〓强2,张广泉2,3. 一种基于抽象与精化技术的Web服务组合验证方法[J]. J4, 2011, 33(9): 76-80.