Probabilistic Functions and Cryptographic Oracles in Higher-Order Logic

The formalisation accompanying the paper Download Probabilistic functions and cryptographic oracles in higher-order logic (PDF, 480 KB) by Andreas Lochbihler published at ESOP 2016 can be downloaded Download here (ZIP, 252 KB). In the meantime, this formalisation has been superseeded by the entries external page CryptHOL and external page Game-based Cryptography published in the external page Archive of Formal Proofs.

Remarks on the download from this site:

• The formalisation and the examples run with external page Isabelle2016.
• The formalisation builds on the entry external page Coinductive from the external page Archive of Formal Proofs. The folder AFP in the above zip file contains the entry for completeness.
• To run Isabelle on the formalisation and check all the proofs and examples, unzip the above file in a folder and run the following command in a terminal.
  
  isabelle build -D path_to_folder
  
  This will also generate a Download proof document (PDF, 1.1 MB) with all definitions, theorems and proofs in the folder output.
• The examples can be found in the files Elgamal.thy and Hashed_Elgamal.thy and PRF_IND_CPA.thy.
• The formalisation of the subprobability monad is in the file SPMF.thy; generative probabilistic values are located in Generative_Probabilistic_Value.thy and GPV_Bisim.thy.