2012 • In Proceedings of 18th International Conference "Tools and Algorithms for the Construction and Analysis of Systems", as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012.
[en] The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of Services. The platform supports application-level specification languages (such as BPMN and our custom languages) and features three validation backends (CL-AtSe, OFMC, and SATMC), which provide a range of complementary automated reasoning techniques (including service orchestration, compositional reasoning, model checking, and abstract interpretation). We have applied the platform to a large number of industrial case studies, collected into the AVANTSSAR Library of validated problem cases. In doing so, we unveiled a number of problems and vulnerabilities in deployed services. These include, most notably, a serious flaw in the SAML-based Single Sign-On for Google Apps (now corrected by Google as a result of our findings). We also report on the migration of the platform to industry.
Disciplines :
Computer science
Identifiers :
UNILU:UL-CONFERENCE-2012-439
Author, co-author :
Armando, Alessandro
Arsac, Wihem
Avanesov, Tigran ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
Publication date :
2012
Event name :
18th International Conference, TACAS 2012,
Event place :
Tallinn, Estonia
Event date :
March 24 - April 1, 2012
Main work title :
Proceedings of 18th International Conference "Tools and Algorithms for the Construction and Analysis of Systems", as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012.
Publisher :
Springer Berlin Heidelberg
ISBN/EAN :
978-3-642-28755-8
Pages :
267-282
Peer reviewed :
Peer reviewed
Commentary :
7214 2012
Proceedings of 18th International Conference, TACAS 2012, Lecture Notes in Computer Science
Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: Verification of Stateful Processes. In: Proc. CSF 2011, pp. 33-47. IEEE CS Press (2011)
Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, 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) (Pubitemid 41431740)
Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics 19(4), 403-429 (2009)
Armando, A., Carbone, R., Compagna, L., Cuéllar, 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 Advances in Information and Communication Technology, vol. 354, pp. 68-79. Springer, Heidelberg (2011)
Armando, A., Carbone, R., Compagna, L., Cuéllar, J., Tobarra Abad, L.: Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In: Proc. FMSE 2008. ACM Press (2008)
Arora, C., Turuani, M.: Validating Integrity for the Ephemerizer's Protocol with CL-Atse. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds.) Formal to Practical Security. LNCS, vol. 5458, pp. 21-32. Springer, Heidelberg (2009)
Arsac, W., Compagna, L., Kaluvuri, S., Ponta, S.E.: Security Validation Tool for Business Processes. In: Proc. SACMAT 2011, pp. 143-144. ACM (2011)
Arsac, W., Compagna, L., Pellegrino, G., Ponta, S.E.: Security Validation of Business Processes via Model-Checking. In: Erlingsson, Ú., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 29-42. Springer, Heidelberg (2011)
AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v.1 (2008)
AVANTSSAR. Deliverable 5.4: Assessment of the AVANTSSAR Validation Platform (2010)
AVANTSSAR. Deliverable 6.2.3: Migration to industrial development environments: lessons learned and best practices (2010)
AVANTSSAR. Deliverable 2.3: ASLan++ specification and tutorial (2011)
AVISPA: Automated Validation of Internet Security Protocols and Applications, http://www.avispa-project.org
Basin, D., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. IJIS 4(3), 181-208 (2005)
Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R.: TulaFale: A Security Tool for Web Services. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 197-222. Springer, Heidelberg (2004) (Pubitemid 39749529)
Bhargavan, K., Fournet, C., Gordon, A.: Verified Reference Implementations of WS-Security Protocols. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 88-106. Springer, Heidelberg (2006) (Pubitemid 44849753)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. CSFW 2001, pp. 82-96. IEEE CS Press (2001)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Automatic validation of protocol narration. In: Proc. CSFW 2003, pp. 126-140. IEEE CS Press (2003)
Boichut, Y., Heam, P.-C., Kouchnarenko, O.: TA4SP: Tree Automata based on Automatic Approximations for the Analysis of Security Protocols (2004)
Boichut, Y., Heam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay Technique to Automatically Verify Security Protocols. In: Proc. AVIS 2004. ENTCS (2004)
Brucker, A., Mödersheim, S.: Integrating Automated and Interactive Protocol Verification. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 248-262. Springer, Heidelberg (2010)
Chevalier, Y., Compagna, L., Cuéllar, J., Hankes Drielsma, P., Mantovani, J., Mödersheim, S., Vigneron, L.: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In: Proc. SAPS 2004, pp. 193-205 (2004)
Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Automatic Composition of Services with Security Policies. In: Proc. WSCA, pp. 529-537. IEEE CS Press (2008)
Comon-Lundh, H., Cortier, V.: New Decidability Results for Fragments of First-order Logic and Application to Cryptographic protocols. TR LSV-03-3, Laboratoire Specification and Verification, ENS de Cachan, France (2003)
Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 2(29) (1983)
Hodkinson, I., Reynolds, M.: Temporal Logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 655-720. Elsevier (2006)
Lucchi, R., Mazzara, M.: A pi-calculus based semantics for WS-BPEL. J. Log. Algebr. Program. 70(1), 96-118 (2007)
Marconi, A., Pistore, M.: Synthesis and Composition of Web Services. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 89-157. Springer, Heidelberg (2009)
Mödersheim, S.: Algebraic Properties in Alice and Bob Notation. In: Proc. Ares 2009, pp. 433-440. IEEE CS Press (2009)
Mödersheim, S.: Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases. In: Proc. CCS 17, pp. 351-360. ACM Press (2010)
Mödersheim, S., Viganò, L.: Secure Pseudonymous Channels. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 337-354. Springer, Heidelberg (2009)
Mödersheim, S., Viganò, L.: The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols. In: Aldini, A., Barth, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 5705, pp. 166-194. Springer, Heidelberg (2009)
OASIS. Web Services Business Process Execution Language Version 2.0. (April 11, 2007), http://docs.asis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.pdf
Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277-286. Springer, Heidelberg (2006)
von Oheimb, D., Mödersheim, S.: ASLan++ - A Formal Security Specification Language for Distributed Systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 1-22. Springer, Heidelberg (2011)
Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314-328. Springer, Heidelberg (1999)
WSO2. Web Services Framework for PHP (2006), http://wso2.org/projects/ wsf/php
