next up previous
Next: Introduction

A Weakest Precondition Calculus
for Analysis of Cryptographic Protocols*

J. Alves-Foss and T. Soule
Laboratory for Applied Logic
Department of Computer Science
University of Idaho


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.

*This project was sponsored in part by the National Security Agency under Grant Number MDA904-96-1-0108. The United States Government is authorized to reproduce and distribute reprints notwithstanding any copyright notation hereon.

Jim Alves-Foss
Fri Aug 1 16:00:31 PDT 1997