Skip to Main content Skip to Navigation
Conference papers

Oracle simulation: a technique for protocol composition with long term shared secrets

Hubert Comon 1 Charlie Jacomme 1, 2 Guillaume Scerri 3, 4
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 PETRUS - Personal Trusted cloud
Inria Saclay - Ile de France, DAVID - Données et algorithmes pour une ville intelligente et durable - DAVID
Abstract : 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.
Complete list of metadata

Cited literature [40 references]  Display  Hide  Download
Contributor : Charlie Jacomme <>
Submitted on : Monday, August 10, 2020 - 5:09:06 PM
Last modification on : Tuesday, February 23, 2021 - 3:28:08 AM
Long-term archiving on: : Monday, November 30, 2020 - 5:21:44 PM


Files produced by the author(s)


  • HAL Id : hal-02913866, version 1


Hubert Comon, Charlie Jacomme, Guillaume Scerri. Oracle simulation: a technique for protocol composition with long term shared secrets. ACM CCS 2020, Nov 2020, Orlando, United States. pp.1427-1444. ⟨hal-02913866⟩



Record views


Files downloads