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

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

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

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