J. Alves-Foss and T. Soule
Laboratory for Applied Logic
Department of Computer Science
University of Idaho
{jimaf,tsoule}@cs.uidaho.edu
This paper present a new approach for the use of belief logics in the analysis of cryptographic protocols. This new approach is based on the concept of the weakest precondition calculus. It generates the necessary preconditions of a protocol, based on the protocol operations and desired goals. In addition, the approach we use overcomes some conceptual problems of belief logic analysis by forcing explicit denotation of internal protocol participant operation. Complete analysis rules and methods are presented, along with exemplary applications. The paper concludes with a discussion of the use of this approach for protocol derivation.