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.
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)