Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets
Hubert Comon, Charlie Jacomme, Guillaume Scerri · 2020
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.