云用戶雙向認(rèn)證協(xié)議的形式化分析與研究.pdf

1、隨著信息網(wǎng)絡(luò)的快速發(fā)展，云服務(wù)走進(jìn)人們的視野，與此同時(shí)，因云環(huán)境的開放性等特點(diǎn)給云計(jì)算的安全帶來極大挑戰(zhàn)。大多數(shù)用戶不選擇云計(jì)算系統(tǒng)，其根本原因就是擔(dān)心云計(jì)算不能保證個(gè)人隱私安全和數(shù)據(jù)安全。云安全協(xié)議是保障云環(huán)境下通信安全的重要手段，面對(duì)云計(jì)算所面臨的安全性挑戰(zhàn)，云安全協(xié)議的設(shè)計(jì)需更加復(fù)雜。Nayak協(xié)議是一種云環(huán)境下基于口令身份認(rèn)證方案，實(shí)現(xiàn)雙向認(rèn)證和會(huì)話密鑰交換的協(xié)議，該協(xié)議不依賴數(shù)字證書，通過共享簡(jiǎn)單易于記憶的口令來進(jìn)行認(rèn)證與密鑰

2、交換，以其簡(jiǎn)單、高效且易于部署的特點(diǎn)得到了廣泛應(yīng)用。但因方案一般選擇易于記憶的口令，導(dǎo)致基于口令的身份認(rèn)證機(jī)制容易受到字典攻擊、中間人攻擊、內(nèi)部人員輔助攻擊等威脅，這意味著Nayak協(xié)議面臨著嚴(yán)峻的安全考驗(yàn)。
　　本文以Nayak協(xié)議為研究對(duì)象，采用形式化方法分析Nayak協(xié)議，針對(duì)Nayak協(xié)議存在的中間人攻擊，對(duì)協(xié)議進(jìn)行改進(jìn)。本文的主要工作如下：
　?。?）運(yùn)用模型檢測(cè)技術(shù)對(duì)Nayak協(xié)議進(jìn)行分析與驗(yàn)證。采用對(duì)稱密鑰密碼

3、體系對(duì)Nayak協(xié)議進(jìn)行加密，基于Dolev-Yao攻擊者模型，提出四通道并行建模法描述攻擊者能力。運(yùn)用SPIN模型驗(yàn)證工具，分析結(jié)果表明采用對(duì)稱密鑰密碼體系對(duì)Nayak協(xié)議加密不安全。
　?。?）分析Nayak協(xié)議所存在的缺陷與安全隱患，提出基于時(shí)間戳私鑰簽名技術(shù)的Nayak-T協(xié)議。Nayak-T協(xié)議在消息項(xiàng)內(nèi)增加時(shí)間戳并更改加密手段，通過雙重加密的手段來保證雙方通信安全，利用四通道并行建模法對(duì)Nayak-T協(xié)議建模，運(yùn)用SP