|
Game-based
cryptography
in
HOL
Title: |
Game-based cryptography in HOL |
Authors:
|
Andreas Lochbihler,
S. Reza Sefidgar and
Bhargav Bhatt (bhargav /dot/ bhatt /at/ inf /dot/ ethz /dot/ ch)
|
Submission date: |
2017-05-05 |
Abstract: |
In this AFP entry, we show how to specify game-based cryptographic
security notions and formally prove secure several cryptographic
constructions from the literature using the CryptHOL framework. Among
others, we formalise the notions of a random oracle, a pseudo-random
function, an unpredictable function, and of encryption schemes that are
indistinguishable under chosen plaintext and/or ciphertext attacks. We
prove the random-permutation/random-function switching lemma, security
of the Elgamal and hashed Elgamal public-key encryption scheme and
correctness and security of several constructions with pseudo-random
functions.
Our proofs follow the game-hopping style advocated by
Shoup and Bellare and Rogaway, from which most of the examples have
been taken. We generalise some of their results such that they can be
reused in other proofs. Thanks to CryptHOL's integration with
Isabelle's parametricity infrastructure, many simple hops are easily
justified using the theory of representation independence. |
BibTeX: |
@article{Game_Based_Crypto-AFP,
author = {Andreas Lochbihler and S. Reza Sefidgar and Bhargav Bhatt},
title = {Game-based cryptography in HOL},
journal = {Archive of Formal Proofs},
month = may,
year = 2017,
note = {\url{http://isa-afp.org/entries/Game_Based_Crypto.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
CryptHOL |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|