Automated Validation of Trust and Security in the Internet of Services

Luca Vigano' (University of Verona, Italy)

The AVANTSSAR Project has developed an automated platform that provides a rigorous technology for the formal specification and Automated VAlidatioN of Trust and Security of Service-oriented ARchitectures. This technology, which is being tuned on a number of relevant industrial case studies so to allow for the migration into the development process for software solutions for the Internet of Services, aims at speeding up the development of new network and service infrastructures, enhance their security and robustness, and increase the public acceptance of emerging IT systems and applications based on them.

I will present some of the main techniques and technologies that are part of the AVANTSSAR Platform and some of the case studies it has been applied on. In particular, to illustrate the platform on the field, I will discuss some of our industrial case studies, including a brief account of our formal analysis of a SAML Web Browser Single Sign-On Protocol. Single-Sign-On (SSO) protocols enable companies to establish a federated environment in which clients sign in the system once and yet are able to access to services offered by different companies. The Security Assertion Markup Language (SAML) Web Browser SSO Profile is the emerging standard in this context. We have provided formal models of the protocol corresponding to one of the most used use case scenarios (the SP-Initiated SSO with Redirect/POST Bindings) and of the implementation used by SAML-based SSO for Google Applications. We have mechanically analyzed these formal models and thereby revealed a severe security flaw in the Google's implementation that allows a dishonest service provider to impersonate a user and get unauthorized access to Google Applications (and viceversa). We have reproduced this attack in an actual deployment of the SAML-based SSO for Google Applications.

I will also present the first results of the SPaCIoS Project that has been combining the AVANTSSAR Platform with techniques and tools for penetration and vulnerability testing to allow for the automated validation of services at provision and consumption time.


Prof. Dr. Luca Vigano' received his Ph.D. in Computer Science from the University of Saarbruecken, Germany, in 1997, and his Habilitation in Computer Science from the University of Freiburg, Germany, in 2003. He held a senior research scientist position at ETH Zurich, Switzerland, from January 2003 to October 2006. Since October 2006, he is an Associate Professor of Computer Science at the University of Verona, where he is the head of the Research Group in Information Security.

His research focuses on formal methods and tools for the specification, verification, and construction of secure systems, and on the theory and applications of non-classical and security logics. On these topics, he has taught several classes, tutorials, and industrial courses, and has co-authored more than 60 publications. He has served as PC-chair and PC-member in several international conferences and workshops, and has participated in the administration and research activity of a number of international and national projects on information security. He is the Project Coordinator of the FP7 project SPaCIoS and was the Project Coordinator of the FP7 project AVANTSSAR.

SESAR lab

Dipartimento di Tecnologie dell'Informazione

Università degli Studi di Milano - 2011.