改進的云用戶雙向認證協(xié)議方案的形式化分析

1、 中國科技論文在線 AS |º A | B (5 由(4和(5以及隨機數(shù)驗證規(guī)則 5，可得 AS |º A |º B (6 160 3.4.3 證明目標 G3 由 A4 以及消息新鮮性規(guī)則 15，可得 AS |º #(C (7 規(guī)則 15 證明，若 AS 相信級聯(lián)消息(B,C是新鮮的，那么 AS 相信 C 是新鮮的。 由 A5 以及信仰規(guī)則 9，可得 165 AS |º A | C (8 由(7和(8以及隨機數(shù)驗證規(guī)則 5，可得 AS |º A |º C (9 因此由以上推導過程中的式(4、(5、(6、(7、(8、(9可知，

2、在前提條件都滿足的情況 下協(xié)議達到了目標 G2，G3。 170 綜上所述， 改進的協(xié)議能夠完成協(xié)議的目標， 在此基礎上證明了改進的協(xié)議具備正確性、 可實現(xiàn)性、目標可達性。 4 結論 BAN 邏輯是推理構造方法中最著名的形式化邏輯模型，它通過認證協(xié)議運行過程中消 息的接收和發(fā)送， 從最初的基礎條件推理出協(xié)議運行必須達到的安全目標。 本文運用此模型 175 形式化分析和推理了一個改進的云用戶雙向認證協(xié)議， 證明了改進協(xié)議能夠達到協(xié)議要求的 目標，具備了協(xié)議的正確性、可實現(xiàn)性以及目標可達性。但是 BAN 邏輯推理也具有一定的 局限性，并不能給出協(xié)議的機密性和認證性，所以下一步工作的目標是通過通信順序

3、進程 （Communicating Sequential Process, CSP）來對改進協(xié)議進行建模及形式化分析。 180 參考文獻 (References 1 馮登國，張敏，張妍，徐震. 云計算安全研究 J. 軟件學報, 2011, 22(1：71-83. FENG D G, ZHANG M, ZHANG Y, XU Z. Study on Cloud Computing SecurityJ, Journal of Software,2011,22(1:71-83. 2 NEEDHAM R, SCHROEDER M. Using Encryption for Authentication

4、 in Large Networks of ComputersJ.Communications of the ACM, 1978, 21(12:993-999. 3 CHOW R, JAKOBSSON M, MASUOKA R, et al. Authentication in the clouds: a framework and its application to mobile usersA. Proceedings of the 2010 ACM workshop on Cloud computing security workshopC.ACM, 2010: 1-6. 4 NAYAK

5、 S K, MOHAPATRA S, MAJHI B. An Improved Mutual Authentication Framework for Cloud ComputingJ. International Journal of Computer Applications, 2012, 52. 5 詹麗 , 姚國祥 , 強衡暢 . 改進的基于 smartcard 的云用戶雙向認證方案 J. 計算機工程與設計 , 2014, 35(2: 440-444. ZHAN L, YAO G Y, QIANG H C. Improved mutual authentication scheme b

6、ased on smartcard for cloud computingJ. Computer Engineering and Design, 2014, 35(2:440-444. 6 BURROWS M, ABADI M, NEEDHAM R M. A logic of authenticationJ. Mathematical and Physical 185 190 195 -6- 中國科技論文在線 Sciences, 1989, 426(1871: 233-271. 7 李建華. 網(wǎng)絡安全協(xié)議的形式化分析與驗證M. 北京：機械工業(yè)出版社，2010. LI J H. Formal anal