Abstract
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 authentication flaw in the SAML-based Single Sign-On for Google Apps.
This work has partially been supported by the FP7-ICT Project SPaCIoS (no. 257876) and by the project SIAM funded in the context of the FP7 EU “Team 2009 - Incoming” COFUND action.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics (2009)
Armando, A., Carbone, R., Compagna, L., Cuellar, J., Abad, L.T.: Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In: Proc. of ACM FMSE 2008 (2008)
Armando, A., Carbone, R., Compagna, L., Cuellar, J., Pellegrino, G., Sorniotti, A.: From Multiple Credentials to Browser-Based Single Sign-On: Are We More Secure? In: Camenisch, J., Fischer-Hübner, S., Murayama, Y., Portmann, A., Rieder, C. (eds.) SEC 2011. IFIP AICT, vol. 354, pp. 68–79. Springer, Heidelberg (2011)
Armando, A., Carbone, R., Compagna, L., Li, K., Pellegrino, G.: Model-checking driven security testing of web-based applications. In: Proc. of ICSTW 2010 (2010)
Armando, A., Compagna, L.: Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 210–225. Springer, Heidelberg (2002)
AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v.1 (2008), http://www.avantssar.eu
Backes, M., Mödersheim, S., Pfitzmann, B., Viganò, L.: Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 428–445. Springer, Heidelberg (2006)
Bau, J., Bursztein, E., Gupta, D., Mitchell, J.: State of the art: Automated black-box web application vulnerability testing. In: 2010 IEEE Symposium on Security and Privacy, SP (2010)
Blanchet, B.: Automatic verification of cryptographic protocols: A logic programming approach. In: Proc. of PPDP 2003 (2003) (invited talk)
Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and fixing PKCS#11 security tokens. In: ACM Conf. on CSS
Büchler, M., Oudinet, J., Pretschner, A.: Security Mutants for Property-Based Testing. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 69–77. Springer, Heidelberg (2011)
Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0 (November 17, 1997), www.cs.york.ac.uk/~jac/papers/drareview.ps.gz
Dadeau, F., Héandam, P.-C., Kheddam, R.: Mutation-based test generation from security protocols in HLPSL. In: ICST 2011 (2011)
Doupé, A., Cova, M., Vigna, G.: Why Johnny Can’t Pentest: An Analysis of Black-Box Web Vulnerability Scanners. In: Kreibich, C., Jahnke, M. (eds.) DIMVA 2010. LNCS, vol. 6201, pp. 111–131. Springer, Heidelberg (2010)
Fraser, G., Wotawa, F., Ammann, P.: Testing with model checkers: a survey. Softw. Test., Verif. Reliab. 19 (2009)
Hondo, M., Nagaratnam, N., Nadalin, A.: Securing web services. IBM Systems Journal 41(2), 228–241 (2002)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131–160. Springer, Heidelberg (2000)
Lowe, G.: A hierarchy of authentication specifications. In: Proc. of the 10th IEEE CSFW 1997 (1997)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 167–181. Springer, Heidelberg (1996)
Marrero, W., Clarke, E.M., Jha, S.: Model checking for security protocols. tech. report cmu-scs-97-139. Technical report, CMU (May 1997)
Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. of ACM CCS 2001 (2001)
OASIS. SAML V2.0 (2005), http://docs.oasis-open.org/security/saml/v2.0/
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: Modelling and Analysis of Security Protocols. Addison Wesley (2000)
Salas, P.A.P., Krishnan, P., Ross, K.J.: Model-based security vulnerability testing. In: Australian Software Engineering Conf., pp. 284–296 (2007)
Salas, P.A.P., Krishnan, P.: Testing privacy policies using models. In: Proc. of SEFM 2008 (2008)
Salaün, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: Proc. of ICWS 2004 (2004)
Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols. Theoretical Computer Science 283(2), 419–450 (2002)
Tretmans, G.J., Brinksma, H.: Torx: Automated model-based testing. In: First European Conf. on Model-Driven Software Engineering
Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing. Technical report, University of Waikato, New Zealand
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A., Pellegrino, G., Carbone, R., Merlo, A., Balzarotti, D. (2012). From Model-Checking to Automated Testing of Security Protocols: Bridging the Gap. In: Brucker, A.D., Julliand, J. (eds) Tests and Proofs. TAP 2012. Lecture Notes in Computer Science, vol 7305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30473-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-30473-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30472-9
Online ISBN: 978-3-642-30473-6
eBook Packages: Computer ScienceComputer Science (R0)