Formal Verification of the xDAuth Protocol
Abstract
Introduction
THE internet has revolutionized the ways of communication. Before the advent of Service Oriented Architecture (SOA), it was not easy to connect organizations and to achieve interoperability among organizations having heterogeneous environments. The SOA provides the facility in which a function of an application can be called as a service by another application using a particular communication protocol. Moreover, the SOA has benefited both the private and the public sector organizations as it has enabled them to share information within and outside the organizational boundaries [1]. However, as information flows out of an organizationboundary, it has its own security implications and necessary measures are required to make the communication secure [2]–[4]. Some of the major challenges of modern-day information sharing among different organizations are: handling cross domain resource sharing among distinct organizations over HTTP or HTTPS, making a wise decision about which information must be allowed for access by which user, dealing with cross domain access control policies, providing strong privacy protection to user data and the issue of building trust on services offered by unseen organizations [4]–[6]. Different standards and protocols have been developed to address the security concerns mentioned above. Some of the well-known standards and protocols are Shibboleth [7], OAuth 2.0 [8], and OpenID .
All of these standards provide users the facility to Sign-In on a system or a website using a single identity, such as Single Sign On (SSO). This can be used in a distributed system such as a federation of different organizations. The federation can be of universities, public or private sector organizations. The federation with respect to Identity Management Systems (IMS) is a joint venture of two or more trusted organizations. Such organizations are bound together with some business or technical contract in which users from either side can access restricted resources [10]. Although, the identity management frameworks and standards provide the capability of SSO, the frameworks are limited on providing certain features of cross domain security such as Conflict of Interest (CoI). Such standards focus on the format in which information must be written. The specifications level security at both collaborating bodies is still a challenge. As an alternate solution to these standards, an access control framework-xDAuth was presented in [11].
The xDAuth protocol overcomes two of the major issues in the SOA and access control, namely Privacy and Trust. The privacy is handled at two levels: one is at the service requester end by hiding user attributes from the service provider and user authentication credentials from the delegation service. The other level is achieved at the service provider end in which delegation service has no prior knowledge of the published resources and service provider uses pseudonyms for the published resources on the delegation service. Trust is achieved by exposing the unique secret key provided by the delegation service (mediating service) to each service requester and service provider involved in the cross domain resource sharing environment. Detailed information on the xDAuth protocol is provided in Section II of the paper. Security standards and protocols of federations are vulnerable to network attacks, as advocated .
Therefore, an effort must be made to analyze the correctness of the protocols, so as to avoid network attacks. The improvements should be formally verified to ensure that the protocols are free of security problems. Formal methods are applied to check the correctness of the protocol. Formal methods have been found to be very useful in the verification of protocols. Formal methods provide techniques and tools for specifying the system and checking the security properties for system verification [15]–[17], [54]. Some cryptographic protocols such as Needham-Schroeder, TMN, Kerberos and a formal foundation for web security have been successfully verified using Formal methods approaches, which exposed the security flaws [18], [19]. xDAuth is considered as one of the prominent protocol for SOA and cross domain access control scenarios. Therefore, verificationof thecorrectnessofxDAuthprotocolis imperative to avoid network attacks. The correctness of the xDAuth protocol ensures that the protocol is free of security problems.
To the best of our knowledge, this is the first effort made on modeling, analysis and formal verification of the xDAuth protocol.We preferredmodelcheckingthan simulation,testing and deductive verification due to the reason that it consists of an exhaustiveexplorationof the system and can be used to verify finite state concurrent systems, which benefit as automatic verification. We have used High Level Petri Nets (HLPN) and Z language for modeling and analysis of the cross domain access control protocol xDAuth [11]. The HLPN presents a graphical representation of the system and provides the mathematical representation to analyze the behavioral and structural properties of the system. With the help of these two techniques, we are able to understand and analyze the interconnections between the system entities, granular details, and processing of information. Verification of the model is done by translating the HLPN model using bounded model checking techniques through Satisfiability Modulo Theories Library (SMT-Lib) and Z3 solver. The security properties are also translated into the SMT and checked whether the model satisfies the security properties. As the focus of this paper is proving the correctness of xDAuth protocol flow, in the said perspective, we defined certain security properties and verified that the security properties must always be satisfied throughout the system. For each of the system’s behavior, such as the sequence of inputs, outputs, and state changes, we clearly determine that whether a desired security property holds or not.
The proposed method can be applied for the evaluation or verification of other security protocols. We have applied the similar method for the formal analysis and verification of FADE protocol, which is used for the security of files stored on the cloud (complete details can be seen in [55]). Moreover, some of the literature work that depicts the application of the method that we adopt to verify our protocol can be seen
in [56] and [57]. The method can also be applied to other kinds of security protocols, such as OAuth and Shibboleth for the verification. The main contributions of the paper are listed below.
• Detail modeling and analysis of cross domain access control protocol, i.e. xDAuth protocol with the help of HLPN and Z language respectively.
• Formal verification of cross domain access control protocol xDAuth on defined system specifications and security properties, using SMT-Lib and Z3 Solver.
• Proving the correctness of the xDAuth protocol by defining certain security properties and verifying that the security properties must always be satisfied throughout the system.
• We perform the automated verification of the model by following the bounded model checking technique using Satisfiability Modulo Theories Library (SMT-Lib) and Z3 solver. During the analysis of xDAuth, we realized that the formal verification of the security properties, such as confidentiality, integrity and authenticity, is not possible without incorporatingcertain attributes as part of xDAuth protocol. Therefore, we augmented the attributes in xDAuth to verify the security properties. This formal verification technique made us able to augment certain attributes in the xDAuth protocol which are necessary for the verification of the security properties.
• The delegation service (DS) returns a domain key (30-byte public string to uniquely identify the domain) and the secret key (10-byte shared secret between the DS and domain) after the registration process. Our analysis has revealed that the said keys can create a single point of failure, which will lead to the compromise of the whole federation.
