next up previous
Next: The Weakest Precondition Calculus Up: A Weakest Precondition Calculus Previous: Needham-Schroeder key distribution protocol


  In this paper we presented a weakest precondition calculus for the verification of authentication of authentication protocols. The benefits of this approach to protocol verification include automatic generation of protocol preconditions, analysis of only recipient beliefs, and detailed specification of the protocol steps. In this section we present some of our thoughts on the benefits and drawbacks of this approach. We then present a brief discussion outlining an approach to formal protocol derivation as a derivative of this work.

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