~/bend-docscommunity

proofs/crypto/aes/api.bend checks

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

11 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
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 ./gcm.bend as GP
import ./aead.bend as AD

Laws

law aes128_encrypt provedsource · line 38 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}

law aes128_decrypt provedsource · line 63 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}

law aes128_roundtrip provedsource · line 87 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

law aes128_forgery provedsource · line 111 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @ne:(@_:{[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}

law aes256_encrypt provedsource · line 151 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}

law aes256_decrypt provedsource · line 176 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}

law aes256_roundtrip provedsource · line 200 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

law aes256_forgery provedsource · line 224 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @ne:(@_:{[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}

law aes128_encrypt_l provedsource · line 271 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_encrypt(key, nonce, aad, pt) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}

law aes128_decrypt_l provedsource · line 297 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_decrypt(key, nonce, aad, ct) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_open(key, nonce, aad, ct) : Maybe<&2, List<&2, U32>>}

law aes128_roundtrip_l provedsource · line 323 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {open128(key, nonce, aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_encrypt(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

law aes128_forgery_t provedsource · line 349 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t:List<&2, U32> -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}

law aes128_forgery_l provedsource · line 392 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t:List<&2, U32> -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_tag(key, nonce, aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_decrypt(key, nonce, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}

law aes256_encrypt_l provedsource · line 421 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_encrypt(key, nonce, aad, pt) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}

law aes256_decrypt_l provedsource · line 447 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_decrypt(key, nonce, aad, ct) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_open(key, nonce, aad, ct) : Maybe<&2, List<&2, U32>>}

law aes256_roundtrip_l provedsource · line 473 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {open256(key, nonce, aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_encrypt(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

law aes256_forgery_t provedsource · line 499 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+n0:U32 -> @+n1:U32 -> @+n2:U32 -> @+n3:U32 -> @+n4:U32 -> @+n5:U32 -> @+n6:U32 -> @+n7:U32 -> @+n8:U32 -> @+n9:U32 -> @+n10:U32 -> @+n11:U32 -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t:List<&2, U32> -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}

law aes256_forgery_l provedsource · line 542 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> @+nonce:List<&2, U32> -> @+hn:{List.length(&2, U32, nonce) == 12n : Nat} -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t:List<&2, U32> -> @+ht:{List.length(&2, U32, t) == 16n : Nat} -> @ne:(@_:{t == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.aes_tag(key, nonce, aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_decrypt(key, nonce, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}

Definitions

def valid_of source · line 19 · 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}

def open128 source · line 24 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @m:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, U32>>

Decrypt what an encryption returned (None stays None).

def open256 source · line 31 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @m:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, U32>>

def no_len source · line 267 · raw

@-G:Type -> @+n:Nat -> @+m:Nat -> @+h:{n == m : Nat} -> @+hf:{Nat.is_eq(n, m) == False{} : Bool} -> G