The development of SATMC began in the context of this project where we came out with a first prototype of it. In this initial phase SATMC has been experimented against a large number of security protocols drawn from the well-known Clark-Jacob's library (small and medium size protocols). Though a set of well-known authentication protocols were quickly found by state-of-the-art SAT solvers, the time spent to generate the propositional encoding strongly dominated the others so to make the analysis unfeasible for complex protocols.
:
shared-cost RTD (FET open) project funded by the European
Commission under the Information Society Technologies Programme
operating within the Fifth Framework Programme, started on January
1st, 2003 and lasted for three years.
In the context of this project SATMC has been significantly
enhanced and improved gaining up to 2 orders of magnitude in
performance. SATMC is now able to scale up to large scale
Internet security protocols (see the AVISPA library) that are definitely more
complex and challenging than those within the Clark/Jacob library.
Even though the AVISPA project successfully finished in July 2005, the AVISPA partners have agreed to continue their productive collaboration. For instance, new versions of the AVISPA package will be periodically released and the SATMC team will contribute to this task.
During this project SATMC has been extended to support the analysis of complex security requirements expressed as LTL formulae. This feature paves the way to new interesting research directions that we are currently investigating.
:
Automated Validation of Trust and Security of
Service-oriented Architectures, FP7-ICT-2007-1 Project no. 216471, funded by the European
Commission under the Information Society Technologies Programme
operating within the Seventth Framework Programme, started on January
1st, 2008 and lasting for three years.
In the context of this project SATMC will be significantly enhanced and improved to validate the security-relevant aspect of service composition. Services normally employ application-level protocols relying on lower-level security protocols. This is for instance the case of the SAML-based Single Sign-On service for Google Apps that uses SSL/TLS to secure the communication at the transport layer. SATMC has been recently run against the SAML-based Single Sign-On service for Google Apps service discovering a serious vulnerability.