Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets

We provide a composition framework together with a variety of composition theorems allowing to split the security proof of an unbounded number of sessions of a compound protocol into simpler goals. While many proof techniques could be used to prove the subgoals, our model is particularly well suited to the Computationally Complete Symbolic Attacker (ccsA) model. We address both sequential and parallel composition, with state passing and long term shared secrets between the protocols. We also provide with tools to reduce multi-session security to single session security, with respect to a stronger attacker. As a consequence, our framework allows, for the first time, to perform proofs in the CCSA model for an unbounded number of sessions. To this end, we introduce the notion of O-simulation: a simulation by a machine that has access to an oracle O. Carefully managing the access to long term secrets, we can reduce the security of a composed protocol, for instance P || Q, to the security of P (resp. Q), with respect to an attacker simulating Q (resp. P) using an oracle O. As demonstrated by our case studies the oracle is most of the time quite generic and simple. These results yield simple formal proofs of composed protocols, such as multiple sessions of key exchanges, together with multiple sessions of protocols using the exchanged keys, even when all the parts share long terms secrets (e.g. signing keys). We also provide with a concrete application to the SSH protocol with (a modified) forwarding agent, a complex case of long term shared secrets, which we formally prove secure.