Protocol Verification



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.


Documentation

Some basic documentation describing the framework and usage of the software.

Download

As an example, we provide an encoding of the Challenge-Response protocol in Prolog.

The source code for the compiler is contained in this zip file.