Formal Verification of the xDAuth Protocol
Service-oriented architecture offers a flexible paradigm for information flow among collaborating organizations. As information moves out of an organization boundary, various security concerns may arise, such as confidentiality, integrity, and authenticity that needs to be addressed. Moreover, verif...
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Article |
| Published: |
Institute of Electrical and Electronics Engineers (IEEE)
2016
|
| Subjects: |
| _version_ | 1825721066678386688 |
|---|---|
| author | Alam, Q. Tabbasum, S. Malik, S.U.R. Alam, M. Ali, T. Akhunzada, A. Khan, S.U. Vasilakos, A.V. Buyya, R. |
| author_facet | Alam, Q. Tabbasum, S. Malik, S.U.R. Alam, M. Ali, T. Akhunzada, A. Khan, S.U. Vasilakos, A.V. Buyya, R. |
| author_sort | Alam, Q. |
| collection | UM |
| description | Service-oriented architecture offers a flexible paradigm for information flow among collaborating organizations. As information moves out of an organization boundary, various security concerns may arise, such as confidentiality, integrity, and authenticity that needs to be addressed. Moreover, verifying the correctness of the communication protocol is also an important factor. This paper focuses on the formal verification of the xDAuth protocol, which is one of the prominent protocols for identity management in cross domain scenarios. We have modeled the information flow of xDAuth protocol using high-level Petri nets to understand the protocol information flow in a distributed environment. We analyze the rules of information flow using Z language, while Z3 SMT solver is used for the verification of the model. Our formal analysis and verification results reveal the fact that the protocol fulfills its intended purpose and provides the security for the defined protocol specific properties, e.g., secure secret key authentication, and Chinese wall security policy and secrecy specific properties, e.g., confidentiality, integrity, and authenticity. |
| first_indexed | 2024-03-06T05:44:42Z |
| format | Article |
| id | um.eprints-18188 |
| institution | Universiti Malaya |
| last_indexed | 2024-03-06T05:44:42Z |
| publishDate | 2016 |
| publisher | Institute of Electrical and Electronics Engineers (IEEE) |
| record_format | dspace |
| spelling | um.eprints-181882017-11-09T03:28:18Z http://eprints.um.edu.my/18188/ Formal Verification of the xDAuth Protocol Alam, Q. Tabbasum, S. Malik, S.U.R. Alam, M. Ali, T. Akhunzada, A. Khan, S.U. Vasilakos, A.V. Buyya, R. QA75 Electronic computers. Computer science Service-oriented architecture offers a flexible paradigm for information flow among collaborating organizations. As information moves out of an organization boundary, various security concerns may arise, such as confidentiality, integrity, and authenticity that needs to be addressed. Moreover, verifying the correctness of the communication protocol is also an important factor. This paper focuses on the formal verification of the xDAuth protocol, which is one of the prominent protocols for identity management in cross domain scenarios. We have modeled the information flow of xDAuth protocol using high-level Petri nets to understand the protocol information flow in a distributed environment. We analyze the rules of information flow using Z language, while Z3 SMT solver is used for the verification of the model. Our formal analysis and verification results reveal the fact that the protocol fulfills its intended purpose and provides the security for the defined protocol specific properties, e.g., secure secret key authentication, and Chinese wall security policy and secrecy specific properties, e.g., confidentiality, integrity, and authenticity. Institute of Electrical and Electronics Engineers (IEEE) 2016 Article PeerReviewed Alam, Q. and Tabbasum, S. and Malik, S.U.R. and Alam, M. and Ali, T. and Akhunzada, A. and Khan, S.U. and Vasilakos, A.V. and Buyya, R. (2016) Formal Verification of the xDAuth Protocol. IEEE Transactions on Information Forensics and Security, 11 (9). pp. 1956-1969. ISSN 1556-6013, DOI https://doi.org/10.1109/TIFS.2016.2561909 <https://doi.org/10.1109/TIFS.2016.2561909>. https://doi.org/10.1109/TIFS.2016.2561909 doi:10.1109/TIFS.2016.2561909 |
| spellingShingle | QA75 Electronic computers. Computer science Alam, Q. Tabbasum, S. Malik, S.U.R. Alam, M. Ali, T. Akhunzada, A. Khan, S.U. Vasilakos, A.V. Buyya, R. Formal Verification of the xDAuth Protocol |
| title | Formal Verification of the xDAuth Protocol |
| title_full | Formal Verification of the xDAuth Protocol |
| title_fullStr | Formal Verification of the xDAuth Protocol |
| title_full_unstemmed | Formal Verification of the xDAuth Protocol |
| title_short | Formal Verification of the xDAuth Protocol |
| title_sort | formal verification of the xdauth protocol |
| topic | QA75 Electronic computers. Computer science |
| work_keys_str_mv | AT alamq formalverificationofthexdauthprotocol AT tabbasums formalverificationofthexdauthprotocol AT maliksur formalverificationofthexdauthprotocol AT alamm formalverificationofthexdauthprotocol AT alit formalverificationofthexdauthprotocol AT akhunzadaa formalverificationofthexdauthprotocol AT khansu formalverificationofthexdauthprotocol AT vasilakosav formalverificationofthexdauthprotocol AT buyyar formalverificationofthexdauthprotocol |