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

### License

BSD License

### History

September 28, 2018
  added the CryptHOL tutorial for game-based cryptography (revision 489a395764ae)

### Topics

- Computer science/Security/Cryptography

### Session Game_Based_Crypto

- Diffie_Hellman
- IND_CCA2
- IND_CCA2_sym
- IND_CPA
- IND_CPA_PK
- IND_CPA_PK_Single
- SUF_CMA
- Pseudo_Random_Function
- Pseudo_Random_Permutation
- Guessing_Many_One
- Unpredictable_Function
- Security_Spec
- Elgamal
- Hashed_Elgamal
- RP_RF
- PRF_UHF
- PRF_IND_CPA
- PRF_UPF_IND_CCA
- Cryptographic_Constructions
- Game_Based_Crypto
- CryptHOL_Tutorial

### Depends on

- CryptHOL

### Used by

- CRYSTALS-Kyber_Security
- Constructive Cryptography in HOL: the Communication Modeling Aspect
- Multi-Party Computation

## Cite

×

Game_Based_Crypto-AFP

    @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{https://isa-afp.org/entries/Game_Based_Crypto.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- May 11, 2017 : Isabelle2016-1