Authors: Sabrina Tarento, Gilles Barthe
Title: A machine-checker formalization of the generic model and the random oracle model
Abstract: 
Most approaches to the formal analyses of cryptographic protocols make
the perfect cryptographic assumption, i.e the hypothese that there is no
way to obtain knowledge about the plaintext pertaining to a ciphertext
without knowing the key. Ideally, one would prefer to rely on a weaker
hypothesis on the computational cost of gaining information about the
plaintext pertaining to a ciphertext without knowing the key. Such a
view is permitted by the generic model and the random oracle model which
provide non-standard computational models in which one may reason about
the computational cost of breaking a cryptographic scheme. Using the
proof assistant Coq, we provide a machine-checker account of the
Generic Model and the Random Oracle Model.