R. Canetti, Universally Composable Security: A New Paradigm for Cryptographic Protocols, 2000.

R. Canetti and T. Rabin, Universal Composition with Joint State, Advances in Cryptology -CRYPTO 2003, ser. Lecture Notes in Computer Science, D. Boneh, pp.265-281, 2003.

M. Backes, B. Pfitzmann, and M. Waidner, The Reactive Simulatability (RSIM) Framework for Asynchronous Systems, Inf. Comput, vol.205, issue.12, pp.1685-1720, 2007.

D. Hofheinz and V. Shoup, GNUC: A New Universal Composability Framework, Journal of Cryptology, vol.28, issue.3, pp.423-508, 2015.

M. Backes, M. Dürmuth, D. Hofheinz, and R. Küsters, Conditional reactive simulatability, Int. J. Inf. Sec, vol.7, issue.2, pp.155-169, 2008.

J. Camenisch, S. Krenn, R. Küsters, and D. Rausch, iUC: Flexible Universal Composability Made Simple, Tech. Rep, 2019.

U. Maurer, Constructive cryptography -A new paradigm for security definitions and proofs, TOSCA, ser, vol.6993, pp.33-56, 2011.

C. Brzuska, M. Fischlin, N. P. Smart, B. Warinschi, and S. C. Williams, Less is more: relaxed yet composable security notions for key exchange, International Journal of Information Security, vol.12, issue.4, pp.267-297, 2013.

B. Blanchet, Composition Theorems for CryptoVerif and Application to TLS 1.3, 31st IEEE Computer Security Foundations Symposium (CSF'18), pp.16-30, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01947959

C. Brzuska, A. Delignat-lavaud, C. Fournet, K. Kohbrok, and M. Kohlweiss, State separation for code-based game-playing proofs, ASIACRYPT (3), ser, vol.11274, pp.222-249, 2018.

G. Bana and H. Comon-lundh, A computationally complete symbolic attacker for equivalence properties, Proceedings of the 21st ACM Conference on Computer and Communications Security (CCS'14), pp.609-620, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102216

T. Ylonen and C. Lonvick, The Secure Shell (SSH) Transport Layer Protocol

R. Küsters and D. Rausch, A Framework for Universally Composable Diffie-Hellman Key Exchange, IEEE 38th Symposium on Security and Privacy, pp.881-900, 2017.

G. Scerri and S. Ryan, Analysis of Key Wrapping APIs: Generic Policies, Computational Security, pp.281-295, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01417123

H. Comon and A. Koutsos, Formal Computational Unlinkability Proofs of RFID Protocols, Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17, pp.100-114, 2017.

G. Bana, R. Chadha, and A. K. Eeralla, Formal Analysis of Vote Privacy Using Computationally Complete Symbolic Attacker, Computer Security -23rd European Symposium on Research in Computer Security, ESORICS 2018, pp.350-372, 2018.

, IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques

C. Brzuska, M. Fischlin, B. Warinschi, and S. C. Williams, Composability of Bellare-rogaway Key Exchange Protocols, Proceedings of the 18th ACM Conference on Computer and Communications Security, ser. CCS '11, pp.51-62, 2011.

M. Fischlin and F. Günther, Multi-Stage Key Exchange and the Case of Google's QUIC Protocol, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, ser. CCS '14, pp.1193-1204, 2014.

R. Küsters and M. , Composition Theorems Without Pre-established Session Identifiers, Proceedings of the 18th ACM Conference on Computer and Communications Security, ser. CCS '11, pp.41-50, 2011.

N. Durgin, J. Mitchell, and D. Pavlovic, A Compositional Logic for Proving Security Properties of Protocols, J. Comput. Secur, vol.11, issue.4, pp.677-721, 2003.

A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani, Probabilistic Polynomial-Time Semantics for a Protocol Security Logic," in Automata, Languages and Programming, ser. Lecture Notes in Computer Science, pp.16-29, 2005.

C. Cremers, On the Protocol Composition Logic PCL, Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, ser. ASIACCS '08, pp.66-76, 2008.

,

S. C. Williams, Analysis of the SSH Key Exchange Protocol," in Cryptography and Coding, ser. Lecture Notes in Computer Science, pp.356-374, 2011.

D. Cadé and B. Blanchet, From Computationally-Proved Protocol Specifications to Implementations and Application to SSH, Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), vol.4, pp.4-31, 2013.

B. Blanchet, CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols," in Dagstuhl seminar "Formal Protocol Verification Applied, 2007.

V. Cortier and S. Delaune, A method for proving observational equivalence, 2009 22nd IEEE Computer Security Foundations Symposium, pp.266-276, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00426622

M. Arapinis, V. Cheval, and S. Delaune, Verifying Privacy-Type Properties in a Modular Way, 2012 IEEE 25th Computer Security Foundations Symposium, pp.95-109, 2012.

K. G. Paterson, J. C. Schuldt, M. Stam, and S. Thomson, On the Joint Security of Encryption and Signature, Revisited, Advances in Cryptology -ASIACRYPT 2011, ser. Lecture Notes in Computer, pp.161-178, 2011.

, We are given a cryptographic library, and oracle O with support n, and two names k, k not in the support. We are given a A O which is a distinguisher over k ? k . We define a PPTTM A

, ? Splits ? r into three distinct infinite tapes ? so , ? ra , ? ro ? Simulates A O(?so,?ro) (m, ? ra, vol.1

, We denote ? k (? s , ?) the tapes where every bit of ? s which does not correspond to a name of k is set to 0, and similarly ? k c (? s , ?) where all bits for k are set to 0. We then have for any PPTOM A O : |P ?s,?r

O. {a-o,

, ?s,?) , ? r , 1 ? ) = 1}

, = 3 P ?so,?s,?ra,?ro {A O(?so,?ro

, ?s , ? ra , 1 ? ) = 1}

?. ?s, , p.1

, Thanks to the definition of support, the oracle answers the same on ? k (? s , ?) and ? s

, we split ? s in two, to replace independent tapes ? k (? s , ?) and ? k c (? s , ?)