Formal Verification of the xDAuth Protocol

Alam, Q; Tabbasum, S; Malik, SUR; Alam, M; Ali, T; Akhunzada, A; Khan, SU; Vasilakos, AV; Buyya, R

Formal Verification of the xDAuth Protocol

Alam, Q Tabbasum, S Malik, SUR Alam, M Ali, T Akhunzada, A Khan, SU Vasilakos, AV Buyya, R

Permalink

Publisher:: IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
Publication Type:: Journal Article
Citation:: IEEE Transactions on Information Forensics and Security, 2016, 11, (9), pp. 1956-1969
Issue Date:: 2016-09-01

Closed Access

	Filename	Description	Size
	Formal_Verification_of_the_xDAuth_Protocol.pdf	Published version	4.18 MB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Alam, Q
dc.contributor.author	Tabbasum, S
dc.contributor.author	Malik, SUR
dc.contributor.author	Alam, M
dc.contributor.author	Ali, T
dc.contributor.author	Akhunzada, A
dc.contributor.author	Khan, SU
dc.contributor.author	Vasilakos, AV
dc.contributor.author	Buyya, R
dc.date.accessioned	2022-08-10T22:06:33Z
dc.date.available	2022-08-10T22:06:33Z
dc.date.issued	2016-09-01
dc.identifier.citation	IEEE Transactions on Information Forensics and Security, 2016, 11, (9), pp. 1956-1969
dc.identifier.issn	1556-6013
dc.identifier.issn	1556-6021
dc.identifier.uri	http://hdl.handle.net/10453/159857
dc.description.abstract	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.
dc.language	English
dc.publisher	IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
dc.relation.ispartof	IEEE Transactions on Information Forensics and Security
dc.relation.isbasedon	10.1109/TIFS.2016.2561909
dc.rights	info:eu-repo/semantics/closedAccess
dc.subject	08 Information and Computing Sciences, 09 Engineering
dc.subject.classification	Strategic, Defence & Security Studies
dc.title	Formal Verification of the xDAuth Protocol
dc.type	Journal Article
utslib.citation.volume	11
utslib.for	08 Information and Computing Sciences
utslib.for	09 Engineering
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Electrical and Data Engineering
utslib.copyright.status	closed_access	*
dc.date.updated	2022-08-10T22:06:29Z
pubs.issue	9
pubs.publication-status	Published
pubs.volume	11
utslib.citation.issue	9

Abstract:

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.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/159857