A Machine-Checked Formalization of the Generic Model and the Random Oracle Model

Gilles Barthe; J.G. Cederquist; Sabrina Tarento

doi:10.1007/978-3-540-25984-8_29

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model

Gilles Barthe, J.G. Cederquist, Sabrina Tarento

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

22 Citations (Scopus)

66 Downloads (Pure)

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	https://doi.org/10.1007/978-3-540-25984-8_29
Publication status	Published - Jul 2004
Event	2nd International Joint Conference on Automated Reasoning, IJCAR 2004 - Cork, Ireland Duration: 4 Jul 2004 → 8 Jul 2004

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer-Verlag
Volume	3097

Conference

Conference	2nd International Joint Conference on Automated Reasoning, IJCAR 2004
Period	4/07/04 → 8/07/04
Other	July 4-8, 2004

Keywords

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

Access to Document

10.1007/978-3-540-25984-8_29

tk80l2ablg7unu0k

http://eprints.eemcs.utwente.nl/secure2/755/01/Barthe04machine.pdf

Cite this

@inproceedings{a7b7ee67682d4d85b1a05dcacf37caa2,

title = "A Machine-Checked Formalization of the Generic Model and the Random Oracle Model",

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.",

keywords = "METIS-220259, IR-48633, SCS-Cybersecurity, EWI-755",

author = "Gilles Barthe and J.G. Cederquist and Sabrina Tarento",

note = "Imported from DIES; null ; Conference date: 04-07-2004 Through 08-07-2004",

year = "2004",

month = jul,

doi = "10.1007/978-3-540-25984-8_29",

language = "Undefined",

isbn = "3-540-22345-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "385--399",

editor = "David Basin and Micha{\"e}l Rusinowitch",

booktitle = "2nd International Joint Conference on Automated Reasoning, IJCAR",

}

Barthe, G, Cederquist, JG & 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. Lecture Notes in Computer Science, vol. 3097, Springer, Berlin, pp. 385-399, 2nd International Joint Conference on Automated Reasoning, IJCAR 2004, 4/07/04. https://doi.org/10.1007/978-3-540-25984-8_29

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. / Barthe, Gilles; Cederquist, J.G.; Tarento, Sabrina.

2nd International Joint Conference on Automated Reasoning, IJCAR. ed. / David Basin; Michaël Rusinowitch. Berlin : Springer, 2004. p. 385-399 (Lecture Notes in Computer Science; Vol. 3097).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Machine-Checked Formalization of the Generic Model and the Random Oracle Model

AU - Barthe, Gilles

AU - Cederquist, J.G.

AU - Tarento, Sabrina

N1 - Imported from DIES

PY - 2004/7

Y1 - 2004/7

N2 - 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.

AB - 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.

KW - METIS-220259

KW - IR-48633

KW - SCS-Cybersecurity

KW - EWI-755

U2 - 10.1007/978-3-540-25984-8_29

DO - 10.1007/978-3-540-25984-8_29

M3 - Conference contribution

SN - 3-540-22345-2

T3 - Lecture Notes in Computer Science

SP - 385

EP - 399

BT - 2nd International Joint Conference on Automated Reasoning, IJCAR

A2 - Basin, David

A2 - Rusinowitch, Michaël

PB - Springer

CY - Berlin

Y2 - 4 July 2004 through 8 July 2004

ER -