Tests and Proofs, May 31-June 1, 2012, Prague, Czech Republic / Published also in LNCS, Volume 7305, 2012, Springer
Model checkers have been remarkably successful in finding flaws in security protocols. In this paper we present an approach to binding specifications of security protocols to actual implementations and show how it can be effectively used to automatically test implementations against putative attack traces found by the model checker. By using our approach we have been able to automatically detect and reproduce an attack witnessing an authentification flaw in the SAML-based Single Sign-On for Google Apps.
Tests and Proofs, May 31-June 1, 2012, Prague, Czech Republic / Published also in LNCS, Volume 7305, 2012, Springer and is available at : http://dx.doi.org/10.1007/978-3-642-30473-6_3