Computational Soundness of Formal Encryption in Coq

R.J. Corin

Computational Soundness of Formal Encryption in Coq

R.J. Corin

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

84 Downloads (Pure)

Abstract

We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.

Original language	Undefined
Title of host publication	3rd Workshop on Formal and Computational Cryptography, FCC 2007
Place of Publication	France
Publisher	INRIA
Pages	-
Number of pages	6
ISBN (Print)	not assigned
Publication status	Published - 4 Jul 2007
Event	3rd Workshop on Formal and Computational Cryptography, FCC 2007 - Venice, Italy Duration: 4 Jul 2007 → 5 Jul 2007 Conference number: 3

Publication series

Name
Publisher	INRIA
Number	06472

Workshop

Workshop	3rd Workshop on Formal and Computational Cryptography, FCC 2007
Abbreviated title	FCC
Country/Territory	Italy
City	Venice
Period	4/07/07 → 5/07/07

Keywords

EWI-10233
IR-64106
METIS-241659
SCS-Cybersecurity

Access to Document

Cite this

@inproceedings{683955a4cefb439596606a1f840c6379,

title = "Computational Soundness of Formal Encryption in Coq",

abstract = "We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.",

keywords = "EWI-10233, IR-64106, METIS-241659, SCS-Cybersecurity",

author = "R.J. Corin",

year = "2007",

month = jul,

day = "4",

language = "Undefined",

isbn = "not assigned",

publisher = "INRIA ",

number = "06472",

pages = "--",

booktitle = "3rd Workshop on Formal and Computational Cryptography, FCC 2007",

note = "3rd Workshop on Formal and Computational Cryptography, FCC 2007 ; Conference date: 04-07-2007 Through 05-07-2007",

}

TY - GEN

T1 - Computational Soundness of Formal Encryption in Coq

AU - Corin, R.J.

N1 - Conference code: 3

PY - 2007/7/4

Y1 - 2007/7/4

N2 - We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.

AB - We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.

KW - EWI-10233

KW - IR-64106

KW - METIS-241659

KW - SCS-Cybersecurity

M3 - Conference contribution

SN - not assigned

SP - -

BT - 3rd Workshop on Formal and Computational Cryptography, FCC 2007

PB - INRIA

CY - France

T2 - 3rd Workshop on Formal and Computational Cryptography, FCC 2007

Y2 - 4 July 2007 through 5 July 2007

ER -