| As distributed computing becomes increasingly prevalent, driving a demand for security and privacy in distributed communication, cryptographic protocols are becoming increasingly valuable components of computational environments. While informal understandings of "security and privacy" abound, the task of provably ensuring that these properties hold necessitates a more systematic approach. Many formal methods for the analysis of security protocols have been developed recently, but few of them are designed to be both practically applicable and capable of proving strong results about security. To be effective as well as practically useful, a formal method for the analysis of cryptographic protocols must be expressive, it must have a formal semantics, it must be intuitive in its application, and it must be automatable.; We present a formal method for analysis of key distribution protocols that meets all these criteria. We focus our analysis on the capabilities and knowledge of a powerful adversary, who has total control over network traffic. Using this paradigm, we give a precise definition of the security and authenticity requirements of a protocol. From this definition, we further define the idea of an attack on a protocol: an adversary can attack a protocol if it is able to violate secrecy or authenticity with a priori knowledge of only session-independent information.; By grounding our reasoning in the adversary's knowledge, we are able to develop a logical system describing how the adversary may use a protocol to extend its knowledge, thereby possibly mounting an attack on the protocol. This system can be naturally formulated as a problem of logic programming, which allows us to produce an automated inference tool for analyzing protocols. This system exists in a fragment of linear logic; we show that our system is logically sound and complete with respect to this fragment. Thus, we have an analysis technique that is valuable not only for uncovering flaws in protocols (demonstrating their insecurity) but also for proving security. |
