SAT-based Model-Checking of Security Protocols: Contact and Contributors

Contact

	to contact the SATMC team.

Contributors to SATMC tool development

Luca Compagna
- Affiliation: Università degli Studi di Genova
- Topics covered:
  - SATMC system design: architecture, approach, and implementation.
  - Translators from IF (v.1 and v.2) to SATE.
  - Reduction to SAT: variants of linears and graphplan-based encoding techniques; abstraction/refinement strategy.
  - Reduction to Logic Programming (with the collaboration of Yuliya Lierler).
- Period: Since May 2001
- Currently at: SAP Research - Security and Trust
- E-mail:

Alessandro Armando
- Affiliation: Università degli Studi di Genova
- Topics covered:
  - SATMC system design: architecture, approach, and implementation of the first prototype.
  - Definition of the SATE planning language.
- Period: Since May 2001
- Currently at: Artificial Intelligence Laboratory
- E-mail:

Roberto Carbone
- Affiliation: Università degli Studi di Genova
- Topics covered: Extension of SATMC to support the analysis of complex properties expressed as LTL formulae
- Period: Since October 2004
- Currently at: Artificial Intelligence Laboratory
- E-mail:

Jacopo Mantovani
- Affiliation: Università degli Studi di Genova
- Topics covered: Translator from IF v.2 to SATE
- Period: October 2003 - July 2005
- Currently at: AizoOn c/o Siemens IA AS MES
- E-mail:

Cristina Frà
- Affiliation: Università degli Studi di Genova
- Topics covered: Optimized Intruder Model for SATMC
- Period: July 2003 - March 2004
- Currently at: Telecom Italia Lab
- E-mail:

Pierre Ganty
- Affiliation: Université Libre de Bruxelles
- Topics covered: First version of the Graphplan-based Encoding
- Period: October 2002 - September 2003
- Currently at: Service des Systèmes Distribués
- E-mail:

Graham Steel
- Affiliation: Laboratoire Spécification et Vérification
- Topics covered: New termination check for SATMC
- Period: Since May 2008
- Currently at: Laboratoire Spécification et Vérification