This page is meant as an index to the helper material for the Summer School lecture on Machine-Checked Cryptography with EasyCrypt and Jasmin, which will take place on June 16th.

Contributors: Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Pierre-Yves Strub, Tiago Oliveira

Documentation

  • doc/slides.pdf contains the presentation which explains the example and exercises
  • doc/cheatsheet.pdf contains a new EasyCrypt cheat sheet
  • doc/jasmin.jazz is a Jasmin file recalling the main syntactic features of the language
  • doc/regptr.jazz and doc/regptr.s explain the new reg ptr feature that permits passing around references to stack regions.

Jasmin Files

  • src/example/NbAESEnc.jazz is a Jasmin implementation of AES-based NbPRFEnc with register-based calling convention
  • src/example/NbAESEnc_mem.jazz is a Jasmin implementation of AES-based NbPRFEnc with memory-based calling convention
  • src/aeslib/aes.jinc is reusable code for AES-NI in Jasmin
  • src/aeslib/aes.jazz is the export interface for AES-NI in Jasmin

EasyCrypt Files

Folder proof/example contains the EasyCrypt specs and proofs for the example:

  • .dir-locals.el: Emacs EasyCrypt mode configuration file to extend include path
  • PRFth.eca: formalization of pseudorandom function
  • NbEnc.eca: formalization of syntax, correctness and security of nonce-based encryption
  • NbPRFEnc.ec: nonce-based encryption from a PRF (the main example)
  • NbAESEnc_proof.ec: Correctness and security proof for Jasmin implementation with register calling convention wrt to NbPRFEnc.ec
  • NbAESEnc_ct_proof.ec: Constant-time proof for Jasmin implementation with register calling convention
  • NbAESEnc_mem_proof.ec: Correctness proof for Jasmin implementation with memory calling convention wrt to NbPRFEnc.ec
  • NbAESEnc_mem_ct_proof.ec: Constant-time proof for Jasmin implementation with memory calling convention
  • RPth.eca: formalization of a random permutation (for exercises)
  • PRPth.eca: formalization of pseudorandom permutation and RF/RP switching lemma (for exercises)

Folder proof/aeslib contains the EasyCrypt specs and proofs for AES-NI:

  • .dir-locals.el: Emacs EasyCrypt mode configuration file to extend include path
  • AES_spec.ec: AES specification in both functional and imperative style, equivalence between the two
  • AES_proof.ec: Correctness proof for Jasmin implementation of AES wrt to AES_spec.ec
  • AES_ct_proof.ec: Constant-time proof for Jasmin implementation of AES

Folder extraction contains the EasyCrypt code that is automatically generated from the Jasmin souces (the correctness and constant-time proofs then import these files):

  • extraction/example/NbAESEnc_jazz.ec: EasyCrypt code extracted from src/example/NbAESEnc.jazz
  • extraction/example/NbAESEnc_jazz_ct.ec: EasyCrypt code extracted from src/example/NbAESEnc.jazz for constant-time proof
  • extraction/example/NbAESEnc_mem_jazz.ec: EasyCrypt code extracted from src/example/NbAESEnc.jazz
  • extraction/example/NbAESEnc_mem_jazz_ct.ec: EasyCrypt code extracted from src/example/NbAESEnc.jazz for constant-time proof
  • extraction/aeslib/AES_jazz.ec: EasyCrypt code extracted from src/aeslib/aes.jazz
  • extraction/aeslib/AES_jazz_ct.ec: EasyCrypt code extracted from src/aeslib/aes.jazz for constant-time proof
  • Additional files generated by the Jasmin compilers for array types also appear in this folder.

Folder test contains the wrapper C files for executing the Jasmin examples:

  • test_NbAESEnc.c: C program to test NbAESEnc.s generated from src/example/NbAESEnc.jazz
  • test_NbAESEnc_mem.c: C program to test NbAESEnc_mem.s generated from src/example/NbAESEnc_mem.jazz
  • test_aes.c: C program to test aes.s generated from src/aeslib/aes.jazz

Folder installation constains Docker and shell scripts to set up your own EasyCrypt and Jasmin environments. A pre-built Docker image with only the command-line tools can also be found here.

How-to

Make sure to edit the Makefile so that it can find easycrypt and jasminc.

Then, from root directory:

  • make clean removes olds files
  • make all builds tests and extracts EasyCrypt code
  • make safety checks Jasmin code for safety
  • make test executes the tests
  • make proofs uses EasyCrypt to check all proofs
  • make check runs safety, test and proofs in one go

Calling Jasmin libraries from other programming languages

  • From C: examples in the test directory, compilation instructions in the Makefile
  • From Rust: example and compilation instructions in the bindings/rust directory
  • From Python 3: example and compilation instructions in the bindings/python directory
  • From OCaml: example and compilation instructions in the bindings/ocaml directory

Fun Stuff

  • Folder qproof includes the same example proof extended to cover quantum adversaries. These scripts can be checked using EasyCrypt branch deploy-quantum. Can you spot the differences?

Getting support

The Formosa Zulip Server is the place to go. There is already a significant Q\&A back-log and your questions usually get answers in a short time.

Background reading

Prior editions of the tutorial