, Universally Composable Security: A New Paradigm for Cryptographic Protocols, 2000.
Universal Composition with Joint State, Advances in Cryptology -CRYPTO 2003, ser. Lecture Notes in Computer Science, D. Boneh, pp.265-281, 2003. ,
The Reactive Simulatability (RSIM) Framework for Asynchronous Systems, Inf. Comput, vol.205, issue.12, pp.1685-1720, 2007. ,
GNUC: A New Universal Composability Framework, Journal of Cryptology, vol.28, issue.3, pp.423-508, 2015. ,
Conditional reactive simulatability, Int. J. Inf. Sec, vol.7, issue.2, pp.155-169, 2008. ,
iUC: Flexible Universal Composability Made Simple, Tech. Rep, 2019. ,
Constructive cryptography -A new paradigm for security definitions and proofs, TOSCA, ser, vol.6993, pp.33-56, 2011. ,
Less is more: relaxed yet composable security notions for key exchange, International Journal of Information Security, vol.12, issue.4, pp.267-297, 2013. ,
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
State separation for code-based game-playing proofs, ASIACRYPT (3), ser, vol.11274, pp.222-249, 2018. ,
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
The Secure Shell (SSH) Transport Layer Protocol ,
A Framework for Universally Composable Diffie-Hellman Key Exchange, IEEE 38th Symposium on Security and Privacy, pp.881-900, 2017. ,
Analysis of Key Wrapping APIs: Generic Policies, Computational Security, pp.281-295, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01417123
Formal Computational Unlinkability Proofs of RFID Protocols, Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17, pp.100-114, 2017. ,
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
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. ,
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. ,
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. ,
A Compositional Logic for Proving Security Properties of Protocols, J. Comput. Secur, vol.11, issue.4, pp.677-721, 2003. ,
Probabilistic Polynomial-Time Semantics for a Protocol Security Logic," in Automata, Languages and Programming, ser. Lecture Notes in Computer Science, pp.16-29, 2005. ,
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. ,
,
Analysis of the SSH Key Exchange Protocol," in Cryptography and Coding, ser. Lecture Notes in Computer Science, pp.356-374, 2011. ,
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. ,
CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols," in Dagstuhl seminar "Formal Protocol Verification Applied, 2007. ,
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
Verifying Privacy-Type Properties in a Modular Way, 2012 IEEE 25th Computer Security Foundations Symposium, pp.95-109, 2012. ,
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
,
, ?s,?) , ? r , 1 ? ) = 1}
, = 3 P ?so,?s,?ra,?ro {A O(?so,?ro
, ?s , ? ra , 1 ? ) = 1}
, , 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 , ?)