Automatic verification of cryptographic protocols with SETHEO

Abstract

In this paper, we describe, how the automated theorem prover SETHEO is used for automatic verification of safety properties of cryptographic protocols. The protocols and their properties are specified using the so-called BAN logic, a multi-sorted modal logic capable of expressing beliefs about secure communication. The resulting formulas and inference rules are transformed into first order predicate logic and processed by the prover SETHEO. Proofs found by SETHEO are then automatically converted into a human-readable form. Experiments with several well-known protocols (e.g., Kerberos, Secure RPC handshake, and CCITT509) revealed very good results: the required properties of the protocols (as described in the literature) could be shown automatically within a few seconds of run-time.