Annual Computer Security Applications Conference (ACSAC) 2012

Full Program »

Using Automated Model Analysis for Reasoning about Security of Web Protocols

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.


Apurva Kumar    
IBM Research


Powered by OpenConf®
Copyright©2002-2014 Zakon Group LLC