Correctness Proof of AES GCM SIV

This repository contains the specification and correctness proof for the reference implementation of AES GCM SIV. Right now it verifies our fork of the code, which has a few verifiability changes (we don't think they change functionality).

Dependencies

Building the proofs requires:

• clang 4.0 (others might work, but we've tested it with this one) to build bitcode for our tools to consume
• llvm4.0 to link the built bitcode
• SAW commit 48e71b4 obtained from github or nightlies, in order to run the proofs
  • ubunutu
  • osx
  • windows
• Z3, a dependency of SAW

Building and running

Run make in the directory you wish to run the proof for.

Specification

The specification is in the cryptol-specs directory.

Proof

• proof.saw the top level proof file that loads the C code and all of the SAW scripts, running the proofs in the process
• GCM_SIV_C.saw main proof file with proofs for
  • key expansion
  • AES_128 encryption
  • gfmul_int (multiplication in a galois field)
  • POLYVAL
  • AES_128_CTR (CTR instantiated with the AES_128 function)
  • GCM_SIV_ENC_2_Keys, the top-level theorem of this proof
• aes_emulation.saw has definitions for state functions, and proofs of row-shifting and substitute-bytes functions
• clmul-emulator.saw contains proofs for functions mul and vcmul_emulator.
• common.saw utility functions to make the SAW proofs pretty