Verified Implementations of the Information Card Federated Identity-Management Protocol - Bhargavan, Karthik; Fournet, Cédric; Gordon, Andy; Swamy, Nikhil (ASIACCS '08 Proceedings of the 2008 ACM symposium on Information, computer and communications security, 2008)
We describe reference implementations for selected configurations of the user authentication protocol defined by the Information Card Profile V1.0. Our code can interoperate with existing implementations of the client, identity provider, and relying party roles of the protocol. We derive formal proofs of security properties for our code using an automated theorem prover. Hence, we obtain the most substantial examples of verified implementations of cryptographic protocols to date, and the first for any federated identity-management protocols. Moreover, we present a tool that downloads security policies from services and token servers and compiles them to a verifiably secure client proxy.