We have implemented a system for automatically finding attacks on cryptographic protocols, through a SitCalc encoding. The basic framework was developed by James Delgrande, Aaron Hunter and Torsten Grote in this paper. The software was written by Wesley May.
In order to analyze a protocol, we create a Prolog program that encodes the structure of the protocol. We then find attacks by iterative deepening search. In order to automate the process, we have written a compiler that automatically translates protocol descriptions into Prolog encodings. The compiler is written in Java.
The source code for the compiler is contained in this zip file.