Journal of Computer Security

Rivest and Lampson have recently introduced SDSI, a Simple Distributed Security Infrastructure. One of the important innovations of SDSI is the use of linked local name spaces. This paper suggests a logical explanation of SDSI’s local name spaces, as a complement to the operational explanation given in the SDSI definition.

We develop an approach to deriving concrete engineering advice for cryptographic protocols from provable-security-style proofs of security. The approach is illustrated with a simple, yet useful protocol. Our main result provides the first published proof of an exact probabilistic relationship between a high-level protocol and multiple cryptographic primitives. This exact relationship enables us to rigorously derive concrete recommendations on the bitlengths of cryptographic keys and on how often principals should rekey. As an additional benefit of our approach, the process of developing our theorem and proof lead us to identify and implement an improvement in our example protocol.

In recent years, a method for analyzing security protocols using the process algebra CSP (Hoare, 1985) and its model checker FDR (Roscoe, 1994) has been developed. This technique has proved remarkably successful, and has been used to discover a number of attacks upon protocols. However, the technique has required producing a CSP description of the protocol by hand; this has proved tedious and error-prone. In this paper we describe Casper, a program that automatically produces the CSP description from a more abstract description, thus greatly simplifying the modelling and analysis process.

Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state systems. Proofs are generated using Isabelle/HOL. The human effort required to analyze a protocol can be as little as a week or two, yielding a proof script that takes a few minutes to run.

Protocols are inductively defined as sets of traces. A trace is a list of communication events, perhaps comprising many interleaved protocol runs. Protocol descriptions incorporate attacks and accidental losses. The model spy knows some private keys and can forge messages using components decrypted from previous traffic. Three protocols are analyzed below: Otway–Rees (which uses shared-key encryption), Needham–Schroeder (which uses public-key encryption), and a recursive protocol (Bull and Otway, 1997) (which is of variable length).

One can prove that event ev always precedes event ev ′ or that property P holds provided X remains secret. Properties can be proved from the viewpoint of the various principals: say, if A receives a final message from B then the session key it conveys is good.