CASPA is a tool for automated analysis of cryptographic protocols using a technique called causality-based abstraction. It provides proofs of security for an unbounded number of concurrent protocol executions in a fully mechanized manner.

Fig. 1. The CASPA Tool
the CASPA tool

CASPA comes with an easy to use gui (see Figure 1) and a powerful command line interface. Additionally a translator from the Intermediate Format, the protocol language of AVISPA, to the prot format used is part of the tool. It can display causal graphs using Graphviz, print out traces for any given node as tex file or simply check a protocol for security. The gui allows for on-the-fly modification and reparsing of the loaded protocol.