Using automated model analysis for reasoning about security of web protocols
Apurva Kumar · 2012
Interoperable identity and trust management infrastructure plays an important role in enabling integrations in cloud computing environments. In the past decade or so, several web-based workflows have emerged as de-facto standards for user identity and resource access across enterprises. Establishing correctness of such web protocols is of immense importance to a large number of common business transactions on the web. In this paper, we propose a framework for analyzing security in web protocols. A novel aspect of our proposal is bringing together two contrasting styles used for security protocol analysis. We use the inference construction style, in which the well-known BAN logic has been extended to reason about web protocols, in conjunction with, an attack construction style that performs SAT based model-checking to rule out certain active attacks. The result is an analysis method that shares simplicity and intuitive appeal of belief logics, at the same time covers a wider range of protocols, along with an ability to automatically find attacks. To illustrate effectiveness, case study of a leading web identity and access management protocol is presented, where application of our analysis method results in a previously unreported attack being identified.