EasyCrypt and Jasmin Tutorial, Šibenik 2022

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

• Introduction to Hoare Logic by Umang Mathur
• Introduction to Provable Security by Michel Abdalla

Prior editions of the tutorial

• SAC 2021
• Indocrypt 2020 - Here is the accompanying video