proofs/crypto/aes/gcm.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend as Gcm

14 imports

import Base
import ../../../src/crypto/aes/types.bend as T
import ../../../src/crypto/aes/aes.bend as A
import ../../../src/crypto/aes/gcm.bend as I
import ../../../src/crypto/subtle.bend as Subtle
import ../../../spec/crypto/aes/aes.bend as S
import ../../../spec/crypto/aes/gcm.bend as G
import ../../../spec/crypto/subtle.bend as Eq
import ../subtle/laws.bend as EqLaws
import ../subtle/proof.bend as EqProof
import ./ghash_defs.bend as D
import ./ghash_bits.bend as B
import ./ghash.bend as H
import ./cipher.bend as C

Definitions

def cb source · line 23 · raw

@q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+c:U32 -> List<&2, U32>

The counter block nonce || [c]_32.

def nonce source · line 29 · raw

@q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> List<&2, U32>

The 96-bit nonce.

def bytes_of_ok source · line 34 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.bytes_of(st) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st) : List<&2, U32>}

def xor_ok source · line 39 · raw

@+xs:List<&2, U32> -> @+ks:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.xor_bytes(xs, ks) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.xor_bytes(xs, ks) : List<&2, U32>}

def keystream_ok source · line 49 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+c:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.keystream(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, q0, q1, q2, c) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.ciph(nk, nr, key, cb(q0, q1, q2, c)) : List<&2, U32>}

def inc_ok source · line 55 · raw

@+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+c:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.inc32(cb(q0, q1, q2, c)) == cb(q0, q1, q2, U32.inc(c)) : List<&2, U32>}

def gctr_ok source · line 64 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+xs:List<&2, U32> -> @+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+c:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.gctr(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, xs, q0, q1, q2, c) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, xs, cb(q0, q1, q2, c)) : List<&2, U32>}

Counter mode from counter c (a whole block per counter; a last partial block uses the leftmost bytes of its keystream block).

def hash_key_ok source · line 121 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.hash_key(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)})) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.hash_key(nk, nr, key) : Word(128n)}

def tag_ok source · line 126 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.tag(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, q0, q1, q2, aad, c) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.tag(nk, nr, key, nonce(q0, q1, q2), aad, c) : List<&2, U32>}

The tag: GCTR from J0 over GHASH of A, C and their lengths.

def seal_ok source · line 135 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.seal_core(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, q0, q1, q2, aad, pt) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.seal(nk, nr, key, nonce(q0, q1, q2), aad, pt) : List<&2, U32>}

GCM-AE: C = GCTR(inc32(J0), P), T = the tag of C.

def accept_ok source · line 142 · raw

@+ok:Bool -> @+p:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.accept(ok, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.accept(ok, p) : Maybe<&2, List<&2, U32>>}

def open_checked_ok source · line 150 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.open_checked(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, q0, q1, q2, aad, c, t) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open_checked(nk, nr, key, nonce(q0, q1, q2), aad, c, t) : Maybe<&2, List<&2, U32>>}

GCM-AD with the tag compared by subtle.eq (equal to list equality).

def open_split_ok source · line 158 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> @+n:Nat -> @+short:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.open_split(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, q0, q1, q2, aad, input, n, short) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open_split(nk, nr, key, nonce(q0, q1, q2), aad, input, n, short) : Maybe<&2, List<&2, U32>>}

def open_ok source · line 165 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+q0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+q2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+aad:List<&2, U32> -> @+input:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.open_core(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, q0, q1, q2, aad, input) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, nonce(q0, q1, q2), aad, input) : Maybe<&2, List<&2, U32>>}