| This dissertation presents a formalism for modeling, simulating and analyzing cryptographic protocols. The approach integrates logic and process calculus components, providing an expressive message passing semantics and sophisticated constructs for modeling the behavior of principals. Moreover, the specification of a common set of inference rules governing communication, reduction and information analysis supports formal proofs about message passing, the knowledge and behavior of principals, and protocol properties. The power of the formalism is introduced with a detailed analysis of the Needham-Schroeder public key authentication protocol. To further illustrate its power, a detailed study of the Clipper and NetBill protocols is also included. The Clipper system was developed by NSA as part of the Escrowed Encryption Standard by a presidential directive in 1993. NetBill is an e-commerce system being developed and tested by Carnegie Mellon University since 1995. |
