proofs/crypto/aes/proof.bend checks

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

15 imports

import Base
import ../../lib/logic.bend as L
import ../../../src/crypto/aes/types.bend as T
import ../../../src/crypto/aes/aes.bend as A
import ../../../src/crypto/aes/gcm.bend as GI
import ../../../src/crypto/aesgcm.bend as GCM
import ../../../spec/crypto/aes/aes.bend as S
import ../../../spec/crypto/aes/gcm.bend as G
import ./laws.bend as Laws
import ./sbox.bend as SB
import ./inverse.bend as INV
import ./cipher.bend as C
import ./gcm.bend as GP
import ./aead.bend as AD
import ./api.bend as API

Laws

law open128_same provedsource · line 160 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+m:Maybe<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/laws.open128(key, nonce, aad, m) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/api.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}

law open256_same provedsource · line 199 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+m:Maybe<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/laws.open256(key, nonce, aad, m) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/api.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}

Definitions

def seal_nonce_bad source · line 31 · raw

@+sched:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule -> @+nonce:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.seal_nonce(sched, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}

A nonce that is not 12 bytes long: None.

def open_nonce_bad source · line 62 · raw

@+sched:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule -> @+nonce:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool} -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.open_nonce(sched, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}

def seal_key_bad source · line 93 · raw

@+m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule> -> @+nonce:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.seal_key(m, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}

def open_key_bad source · line 100 · raw

@+m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule> -> @+nonce:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool} -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.open_key(m, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}

def valid_of source · line 108 · raw

@+key:List<&2, U32> -> @+w:Nat -> @+h:{List.length(&2, U32, key) == w : Nat} -> @+v:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.valid_length(w) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.valid_length(List.length(&2, U32, key)) == True{} : Bool}

A key of w bytes, w one of 16, 24, 32, passes the length check.