### Abstract

Most approaches to the formal analyses of cryptographic protocols make the perfect cryptography 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-checked account of the Generic Model and the Random Oracle Model.

Original language | Undefined |
---|---|

Title of host publication | 2nd International Joint Conference on Automated Reasoning, IJCAR |

Editors | David Basin, Michaël Rusinowitch |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 385-399 |

Number of pages | 15 |

ISBN (Print) | 3-540-22345-2 |

DOIs | |

Publication status | Published - Jul 2004 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer-Verlag |

Volume | 3097 |

### Keywords

- METIS-220259
- IR-48633
- SCS-Cybersecurity
- EWI-755

## Cite this

Barthe, G., Cederquist, J. G., & Tarento, S. (2004). A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In D. Basin, & M. Rusinowitch (Eds.),

*2nd International Joint Conference on Automated Reasoning, IJCAR*(pp. 385-399). (Lecture Notes in Computer Science; Vol. 3097). Berlin: Springer. https://doi.org/10.1007/978-3-540-25984-8_29