Affiliations: [a] Sandia National Labs, P.O. Box 969, Livermore, CA 94551, USA. Tel.: +1 925 294 4909; Fax: +1 925 294 3271; E-mail: [email protected] | [b] Computer Science Department, Stanford University, Stanford, CA 94305, USA. E-mail: [email protected] | [c] Kestrel Institute, Palo Alto, CA 94304, USA. E-mail: [email protected]
Note: [*] Partially supported by the Kestrel Institute, ONR MURI “Semantic Consistency in Information Exchange”, N00014-97-1-0505, and ONR Grant “Games and Security in Systems of Autonomous Agents”, N0014-00-C-0495.
Abstract: We present a logic for proving security properties of protocols that use nonces (randomly generated numbers that uniquely identify a protocol session) and public-key cryptography. The logic, designed around a process calculus with actions for each possible protocol step, consists of axioms about protocol actions and inference rules that yield assertions about protocols composed of multiple steps. Although assertions are written using only steps of the protocol, the logic is sound in a stronger sense: each provable assertion about an action or sequence of actions holds in any run of the protocol that contains the given actions and arbitrary additional actions by a malicious attacker. This approach lets us prove security properties of protocols under attack while reasoning only about the sequence of actions taken by honest parties to the protocol. The main security-specific parts of the proof system are rules for reasoning about the set of messages that could reveal secret data and an invariant rule called the “honesty rule”.
