Proving a WS-Federation passive requestor profile

Abstract

Currently, influential industrial players are in the process of realizing identity federation, in particular the authentication of browser users across administrative domains. WS-Federation is a joint protocol framework for Web Services clients and browser clients. While browser-based federation protocols, including Microsoft Passport, OASIS SAML, and Liberty besides WS-Federation, are already widely deployed, their security is still unproven and has been challenged by several analyses. One reason is a lack of cryptographically precise protocol definitions, which impedes explicit design for security as well as proofs. Another reason is that the security properties depend on the browser and even on the browser user. We rigorously formalize a strict instantiation of the current WSFederation Passive Requestor Interop profile and make explicit assumptions for its general use. On this basis, we prove that the protocol provides authenticity and secure channel establishment in a realistic trust scenario. This constitutes the first positive security result for a browser-based identity federation protocol.