Computer Science ›› 2016, Vol. 43 ›› Issue (4): 140-144.doi: 10.11896/j.issn.1002-137X.2016.04.028

Previous Articles     Next Articles

Cloud Services Cross-domain Authentication Protocol Formal Analysis and Verification Based on Fragment Model Check

CHEN Hong-song, WANG Gang and FU Zhong-chuan   

  • Online:2018-12-01 Published:2018-12-01

Abstract: Aiming at the cross-domain authentication problem in multi-cloud services,a cloud service security authentication scheme based on SAML(Security Assert Markup Language)protocol was proposed.The key techniques and mechanism were clarified,and the abstract model of cloud service security authentication protocol was built.Using the combination of Casper and FDR software,cloud service authentication protocol was formally analyzed and verified by model checking method.By dividing the protocol to do model checking separately,the state space explosion problem in security protocol formal analysis and verification was resolved.The experiment results from model checking software prove that the proposed cross-domain authentication scheme is effective and security.

Key words: Cloud services,Authentication protocol,Formal analysis,Model checking

[1] Mishra A,Jain R,Durresi A.Cloud computing:networking and communication challenges[J].IEEE Communications Magazine,2012,0(9):24-25
[2] Grosse E,Howie J,Ransome J,et al.Cloud Computing Round-table[J].IEEE Security & Privacy,2010,8(6):17-23
[3] Feng Deng-guo,Zhang Min,Zhang Yan,et al.Study on CloudComputing Security [J].Journal of Software,2011,2(1):71-83(in Chinese) 冯登国,张敏,张妍,等.云计算安全研究[J].软件学报,2011,2(1):71-83
[4] Armbrust M,Fox A,Griffith R,et al.Above the Clouds:ABerkeley View of Cloud Computing[EB/OL].http://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-28.pdf
[5] Nordbotten N A.XML and Web Services Security Standards[J].IEEE Communications Surveys & Tutorials,2009,1(3):4-21
[6] Harding P,Johansson L,Klingenstein N.Dynamic Security Assertion Markup Language:Simplifying Single Sign-On[J].IEEE Security & Privacy,2008,6(2):83-85
[7] Marques Jr A P,Ravn A P,Srba J,et al.Model-checking web services business activity protocols[J].International Journal on Software Tools for Technology Transfer,2013,15(2):125-147
[8] Sheng Q Z,Maamar Z,Yahyaoui H,et al.Separating operational and control behaviors:A new approach to Web services mode-ling[J].IEEE Internet Computing,2010,14(3):68-76
[9] Zech P.Risk-based security testing in cloud computing environments[C]∥2011 IEEE Fourth International Conference on Software Testing,Verification and Validation (ICST).IEEE,2011:411-414
[10] Lin Chuang,Su Wen-bo,Meng Kun,et al.Cloud computing security:architecture,mechanism and model evaluation[J].Chinese Journal of Computers,2013,36(9):1765-1784(in Chinese) 林闯,苏文博,孟坤,等.云计算安全:架构,机制与模型评价[J].计算机学报,2013,36(9):1765-1784
[11] Chen Hong-song,Bhargava B,Fu Zhong-chuan.Multilabels-Based Scalable Access Control for Big Data Applications[J].IEEE Cloud Computing,2014,1(3):65-71
[12] Dalal A,Jeff K,Alessandra R,et al.Elaborating Requirements Using Model Checking and Inductive Learning[J].IEEE Transactions on Software Engineering,2012,9(3):361-383
[13] Gavin L.Breaking and fixing the Needham Schroeder public-key protocol using FDR[J].Software Concepts and Tools,1996,7:993-999
[14] Gavin L.Casper:a compiler for the analysis of security protocols[J].Journal of Computer Security,1998,6(1):53-58

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!