Verifying the correctness of cryptographic protocols using "Convince"

Abstract

The paper describes Convince, a tool being developed to facilitate the modeling and analysis of cryptographic protocols, particularly those supporting authentication. Convince uses a belief logic to facilitate the analysis and proof of desired properties of these protocols. Convince incorporates in its front-end a commercial computer aided software engineering tool, StP/OMT, so that an analyst can model a protocol using a combination of familiar graphical and textual notations. Convince uses a Higher Order Logic theorem prover with automated support, so as to minimize the need for specialized theorem proving knowledge. The paper describes how an analyst can use Convince to rapidly construct models of authentication protocols, and outlines a strategy for verifying their correctness. It discusses the integration of StP/OMT with the theorem proving component and practical analysis techniques based on experience acquired through analyzing several published protocols.