A belief logic for analyzing security of web protocols

Many useful transactions on the web are implemented as a sequence of interactions that a user performs with multiple collaborating providers. Safety of such transactions requires the user to not only trust individual providers and communication channels, but also the web protocols that manage security of these transactions. A protocol can be trusted for a particular usage, if the guarantees that it provides its participants are considered acceptable in the context. An important set of approaches for cryptographic protocol analysis are based on the so-called BAN logic which is used to reason about beliefs established at protocol participants. In this paper, we attempt at providing a similar approach for web protocols. The new logic extends BAN and supports key concepts that simplify security analysis of web protocols. It also takes into account additional challenges introduced due to browser-based interaction. Through examples of two leading cross-domain identity and access management protocols, we demonstrate efficacy of our analysis in establishing precisely what a protocol achieves, in deciding whether it can be trusted for a particular need and in proposing fixes that improve trust levels.