Full Program »
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 - extending the well-known BAN logic to do reasoning 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 but having coverage for a wider-range of protocols and the ability of automated attack generation. 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.
Author(s):
Apurva Kumar
IBM Research
India