~/bend-docscommunity

proofs/crypto/aes/laws.bend open laws/TODOs

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

8 imports
import Base
import ../../../src/crypto/aes/types.bend as T
import ../../../src/crypto/aes/sbox.bend as B
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

Laws

law Sbox.value openits proof in laws_crypto.bend does not pass the checker (fails)source · line 43 · raw

@+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.sbox(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sbox(x) : U32}

The constant-time S-box circuit is FIPS 197's S-box (the inverse in GF(2^8), {00} to {00}, then the affine map), on every input.

law Inverse.unit openits proof in laws_crypto.bend does not pass the checker (fails)source · line 50 · raw

@+x:U32 -> @+h:{U32.is_eq(U32.and(255, x), 0) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mul(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.inverse(x)) == 1 : U32}

The specification's inverse (a^254) is the multiplicative inverse of FIPS 197 section 4.4: a * a^-1 = {01} for every nonzero byte, and {00} goes to {00} (5.1.1); so S.sbox is "inverse, then affine map".

law Inverse.zero openits proof in laws_crypto.bend does not pass the checker (fails)source · line 55 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.inverse(0) == 0 : U32}

law Cipher.value openits proof in laws_crypto.bend does not pass the checker (fails)source · line 60 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.encrypt(nk, nr, key, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.encrypt(nk, nr, key, s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

The implementation's cipher with its expanded key is FIPS 197's Cipher with KeyExpansion, for every Nk, Nr, key and state.

law Block.value openits proof in laws_crypto.bend does not pass the checker (fails)source · line 69 · raw

@+key:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.valid_length(List.length(&2, U32, key)) == True{} : Bool} -> @+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @+b3:U32 -> @+b4:U32 -> @+b5:U32 -> @+b6:U32 -> @+b7:U32 -> @+b8:U32 -> @+b9:U32 -> @+b10:U32 -> @+b11:U32 -> @+b12:U32 -> @+b13:U32 -> @+b14:U32 -> @+b15:U32 -> {block_with(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand_key(key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.aes(key, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.state_of([b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15])))} : Maybe<&2, List<&2, U32>>}

The byte API: a key of 16, 24 or 32 bytes encrypts a 16-byte block with AES under the key's Nk = length/4 and Nr = Nk + 6 (FIPS 197 Figure 4).

law Block.aes128 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 92 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 16n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nk(key) == 4n : Nat}

A 16-, 24-, 32-byte key is AES-128 (Nk = 4, Nr = 10), AES-192 (6, 12), AES-256 (8, 14).

law Block.aes192 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 97 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 24n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nk(key) == 6n : Nat}

law Block.aes256 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 102 · raw

@+key:List<&2, U32> -> @+h:{List.length(&2, U32, key) == 32n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nk(key) == 8n : Nat}

law Gcm.seal openits proof in laws_crypto.bend does not pass the checker (fails)source · line 111 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+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/aes/gcm.seal_core(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule{nr, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.expand(nk, nr, key)}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{n0, n1, n2, n3}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{n4, n5, n6, n7}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{n8, n9, n10, n11}, aad, pt) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.seal(nk, nr, key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) : List<&2, U32>}

The implementation's GCM-AE / GCM-AD, for every expanded key, 96-bit nonce, AAD and input.

law Gcm.open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 131 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+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> -> @+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)}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{n0, n1, n2, n3}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{n4, n5, n6, n7}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{n8, n9, n10, n11}, aad, input) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, input) : Maybe<&2, List<&2, U32>>}

law Aead.roundtrip openits proof in laws_crypto.bend does not pass the checker (fails)source · line 153 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, iv, aad, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.seal(nk, nr, key, iv, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

AEAD correctness of the specification: opening the sealed message gives it back; C || T with T other than the tag of C is rejected.

law Aead.forgery openits proof in laws_crypto.bend does not pass the checker (fails)source · line 162 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, 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.tag(nk, nr, key, iv, aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, iv, 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 Api128.encrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 190 · 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 Api128.decrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 209 · 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 Api128.roundtrip openits proof in laws_crypto.bend does not pass the checker (fails)source · line 229 · 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>>}

decrypt(encrypt(x)) == Some(x).

law Api128.forgery openits proof in laws_crypto.bend does not pass the checker (fails)source · line 249 · 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>>}

A wrong tag gives None.

law Api128.bad_key openits proof in laws_crypto.bend does not pass the checker (fails)source · line 286 · raw

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

A key of another length is rejected.

law Api128.bad_key_open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 294 · raw

@+key:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, key), 16n) == False{} : Bool} -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes128_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}

law Api128.bad_nonce openits proof in laws_crypto.bend does not pass the checker (fails)source · line 303 · raw

@+key:List<&2, U32> -> @+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/aesgcm.aes128_gcm_encrypt(key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}

A nonce other than 12 bytes is rejected.

law Api128.bad_nonce_open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 311 · raw

@+key:List<&2, U32> -> @+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/aesgcm.aes128_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}

law Api256.encrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 321 · 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 Api256.decrypt openits proof in laws_crypto.bend does not pass the checker (fails)source · line 340 · 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 Api256.roundtrip openits proof in laws_crypto.bend does not pass the checker (fails)source · line 360 · 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>>}

decrypt(encrypt(x)) == Some(x).

law Api256.forgery openits proof in laws_crypto.bend does not pass the checker (fails)source · line 380 · 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>>}

A wrong tag gives None.

law Api256.bad_key openits proof in laws_crypto.bend does not pass the checker (fails)source · line 417 · raw

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

A key of another length is rejected.

law Api256.bad_key_open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 425 · raw

@+key:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool} -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.aes256_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}

law Api256.bad_nonce openits proof in laws_crypto.bend does not pass the checker (fails)source · line 434 · raw

@+key:List<&2, U32> -> @+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/aesgcm.aes256_gcm_encrypt(key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}

A nonce other than 12 bytes is rejected.

law Api256.bad_nonce_open openits proof in laws_crypto.bend does not pass the checker (fails)source · line 442 · raw

@+key:List<&2, U32> -> @+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/aesgcm.aes256_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}

Definitions

def block_with source · line 17 · raw

@m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.Schedule> -> @block:List<&2, U32> -> Maybe<&2, List<&2, U32>>

One block with an optional expanded key (the byte API in one call).

def open128 source · line 25 · 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 32 · raw

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