We formalize the Dolev-Yao model of security protocols using two different notations, one based on multiset rewriting with existentials, and the other based on a process calculus combined with Hoare logic-style logical assertions. The goal is to provide simple formal notations for describing and proving security properties about protocols that use nonces (randomly generated numbers that uniquely identify a protocol session) and public- and symmetric-key cryptography. In the first part of the paper, we formalize the assumptions of the Dolev-Yao model and analyze the complexity of the secrecy problem under various restrictions. We use multiset rewriting to prove that, even for the case where we restrict the size of messages and the depth of message encryption, the secrecy problem is undecidable for the case of an unrestricted number of protocol roles and an unbounded number of new nonces. We also identify several decidable classes, including a DEXP-complete class when the number of nonces is restricted, and an NP-complete class when both the number of nonces and the number of roles is restricted. In the second part of the paper we define a logic, designed around a process calculus with actions for each possible protocol step, that 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.
展开▼
