Deciding cryptographic protocol adequacy with HOL

Abstract

A cryptographiCprotocolis an algorithm involving exchanges of encrypted information carried out by principals in a distributed environment. It is intended to produce secure communications, even if every message can be read by, or originate with, every principal. This paper gives a definitional tIOL formalization of a "belief logic" based on the full Gong, Needham, and Yahalom [2] logic for analyzing whether protocols achieve desired communication conditions. This gives the "belief logic" a sound formal basis. The paper also sketches the algorithm for a possible HOL tactic automatically constructing proofs that protocols achieve desired communication conditions if they do achieve them.