Reconstruction of potential attack scenarios for using OpenID protocol in cloud environment based on TLA+

Existing model checking tools for security protocols analysis have two drawbacks, when applied to present day cloud-based protocols. Firstly, they do not consider the new features of cloud computing. Secondly, they do not support the reconstruction of potential attack scenarios. Which could provide conclusive descriptions and non refutable proofs regarding the source of the attack, details of steps involved in the occurred attack scenario, exploited vulnerabilities, and generated system damages. In this paper, we use TLA+, a model checking tool of a state-based logic that allows the description of states and state transitions, to generate executable attack scenarios showing with details how the attack scenario was conducted and how the system behaved accordingly. Through the analysis of using OpenID protocol in cloud environment, we found a new attack scenario.