Formal analysis of key exchange protocols and physical protocols
Benedikt Schmidt · Repository for Publications and Research Data (ETH Zurich) · 2012
A security protocol is a distributed program that might be executed on a network controlled by an adversary.Even in such a setting, the protocol should satisfy the desired security property.Since it is hard to consider all possible executions when designing a protocol, formal methods are often used to ensure the correctness of a protocol with respect to a model of the protocol and the adversary.Many such formal models use a symbolic abstraction of cryptographic operators by terms in a term algebra.The properties of these operators can then be modeled by equations.In this setting, we make the following contributions:1. We present a general approach for the automated symbolic analysis of security protocols that use Diffie-Hellman exponentiation and bilinear pairings to achieve advanced security properties.We model protocols as multiset rewriting systems and security properties as first-order formulas.We analyze them using a novel constraint-solving algorithm that supports both falsification and verification, even in the presence of an unbounded number of protocol sessions.The algorithm exploits the finite variant property and builds on ideas from strand spaces and proof normal forms.We demonstrate the scope and the effectiveness of our algorithm on non-trivial case studies.For example, the algorithm successfully verifies the NAXOS protocol with respect to a symbolic version of the eCK security model.2. We examine the general question of when two agents can create a shared secret.Namely, given an equational theory describing the cryptographic operators available, is there a protocol that allows the agents to establish a shared secret?We examine this question in several settings.First, we provide necessary and sufficient conditions for secret establishment using subterm-convergent theories.This yields a decision procedure for this problem.As a consequence, we obtain impossibility results for symmetric encryption.Second, we use algebraic methods to prove impossibility results for monoidal theories including XOR and abelian groups.Third, we develop a general combination result that enables modular impossibility proofs.For example, the results for symmetric encryption and XOR can be combined to obtain impossibility for the joint theory.3. We develop a framework for the interactive analysis of protocols that establish and rely on properties of the physical world.Our model extends standard, inductive, tracebased, symbolic approaches with location, time, and communication.In particular, communication is subject to physical constraints, for example, message transmission takes time determined by the communication medium used and the distance between nodes.All agents, including intruders, are subject to these constraints and this results in a distributed intruder with restricted, but more realistic, communication capabilities than those of the standard Dolev-Yao intruder.Building on our message theory that includes XOR, we also account for the possibility of overshadowing of message parts.We have formalized our model in Isabelle/HOL and have used it to verify protocols for authenticated ranging, secure time synchronization, and distance bounding.The analysis of distance bounding attacks accounts for overshadowing and distance hijacking attacks.