The aim of this work is to develop methods for verifying protocol correctness that will aid protocol designers at the beginning of the design process, rather than later, after the protocol is already in use. The focus is on determining what each party in a transaction can be proved to believe. The tool should be usable by protocol designers, not mathematicians. The tool is meant to be used to iteratively refine a protocol design.
At the same time, human factors were very important to the tool's developers. The tool provides a common front end to a variety of back end formal methods engines. The front end consists of a ``software through pictures'' user interface, allowing the user to view the software as a set of interacting objects. The back end uses a version of belief logic whose libraries have been inspected on the source code level by members of the theorem-proving community. The back end receives the protocol specification through an intermediate language produced by the front end. Feedback is returned to the front end and displayed to the user.
To model a protocol, the user inputs a description consisting of beliefs, assumptions, and initial conditions from which the tool produces high level, graphical diagrams. The user can then see what goals are reachable. As a demonstration of the system, a somewhat simplified version of public key Kerberos was modeled. The usual problems in verification, insufficient initial conditions and wrong associations of messages and assumptions were experienced. The whole analysis took three days of tool use.
This tool provides a way to clearly specify the assumptions in a cryptographic protocol. It decreases the analysis time through automation, and it places formal methods in the designer's hands.