Formal Verification of the xDAuth Protocol
Document Type
Article
Publication Date
1-1-2016
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.
Keywords
Cross domain access control framework, Formal methods, High-level Petri nets (HLPN), Information security, Modeling, Verification, SMT, Service oriented architecture (SOA), xDAuth protocol, Z3
Divisions
fsktm
Publication Title
IEEE Transactions on Information Forensics and Security
Volume
11
Issue
9
Publisher
Institute of Electrical and Electronics Engineers (IEEE)