ASPASyA stands for Automated tool for Security Protocols Analysis based on a Symbolic Approach. It is a tool aimed to verification of security properties of communication protocols by means of symbolic model checking. It is based on cIP calculus for protocol specification and the associated PL-Logic for properties validation.

Technical documents

• G. Baldi, A. Bracciali, G. Ferrari, E. Tuosto "A Coordination-based Methodology for Security Protocol Verification". Proceedings of the 2nd International Workshop on Security Issues with Petri Nets and other Computational Models, June 2004, Volume 121, ENTCS [PDF] (the presentation to the workshop is here)
• PhD thesis of Andrea Bracciali (see here)
• Part II of Emilio Tuosto's PhD Thesis (see here or here)
• ASPASyA: an Automated tool for Security Protocols Analysis based on a Symbolic Approach [PDF] [Gzipped PS]
• Security Protocols Verification by Means of Symbolic Model Checking [PDF] [Gzipped PS]

Ongoing activity

• Optimization of the OCAML implementation.
• Refinement of technical documentation.
• Integration with the other tools (HAL, STA, Mobility Workbench).
• Verification of additional protocols.
• Extension to secure component composition.

Contacts

• Andrea Bracciali
• Gianluigi Ferrari
• Emilio Tuosto