proofs/crypto/aes/proof.bend source
proofs/crypto/aes/proof.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../../src/crypto/aes/types.bend as Timport ../../../src/crypto/aes/aes.bend as Aimport ../../../src/crypto/aes/gcm.bend as GIimport ../../../src/crypto/aesgcm.bend as GCMimport ../../../spec/crypto/aes/aes.bend as Simport ../../../spec/crypto/aes/gcm.bend as Gimport ./laws.bend as Lawsimport ./sbox.bend as SBimport ./inverse.bend as INVimport ./cipher.bend as Cimport ./gcm.bend as GPimport ./aead.bend as ADimport ./api.bend as API# Generated by tools/generators/aes/proof.py.# Gate for AES and AES-GCM: `bend proofs/crypto/aes/proof.bend` checks every# clause of laws.bend, for every input:# sbox.bend the S-box circuit and the doublings, on all 256 bytes# cipher.bend SubBytes .. AddRoundKey, the rounds, KeyExpansion, Cipher# gf.bend polynomial product mod m == Algorithm 1 (any modulus)# ghash*.bend the word-level GHASH == SP 800-38D's GHASH# gcm.bend GCTR, the tag, GCM-AE and GCM-AD == SP 800-38D# aead.bend open(seal(x)) == Some(x); a wrong tag gives None# The key size stays symbolic (Nk = length/4) so that no key expansion is# ever unfolded at a concrete size.# A nonce that is not 12 bytes long: None.def seal_nonce_bad(+sched: A.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>) -> {GI.seal_nonce(sched, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}: match nonce: case Nil{}: {==} case n0 <> Nil{}: {==} case n0 <> n1 <> Nil{}: {==} case n0 <> n1 <> n2 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: Empty.absurd({GI.seal_nonce(sched, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == None{} : Maybe<&2, List<&2, U32>>}, L.true_false(h)) case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> n12 <> rest: {==}def open_nonce_bad(+sched: A.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>) -> {GI.open_nonce(sched, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}: match nonce: case Nil{}: {==} case n0 <> Nil{}: {==} case n0 <> n1 <> Nil{}: {==} case n0 <> n1 <> n2 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: {==} case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: Empty.absurd({GI.open_nonce(sched, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == None{} : Maybe<&2, List<&2, U32>>}, L.true_false(h)) case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> n12 <> rest: {==}def seal_key_bad(+m: Maybe<&2, A.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>) -> {GI.seal_key(m, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}: match m: case None{}: {==} case Some{s}: seal_nonce_bad(s, nonce, h, aad, pt)def open_key_bad(+m: Maybe<&2, A.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>) -> {GI.open_key(m, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}: match m: case None{}: {==} case Some{s}: open_nonce_bad(s, nonce, h, aad, ct)# A key of w bytes, w one of 16, 24, 32, passes the length check.def valid_of(+key: List<&2, U32>, +w: Nat, +h: {List.length(&2, U32, key) == w : Nat}, +v: {A.valid_length(w) == True{} : Bool}) -> {A.valid_length(List.length(&2, U32, key)) == True{} : Bool}: %Equal.sym(Nat, List.length(&2, U32, key), w, h) : {A.valid_length(_) == True{} : Bool} vdef Laws.Sbox.value(x): SB.sbox_ok(x)def Laws.Inverse.unit(x, h): INV.inverse_unit(x, h)def Laws.Inverse.zero(): INV.inverse_zero()def Laws.Cipher.value(nk, nr, key, s): C.encrypt_ok(nk, nr, key, s)def Laws.Block.value(key, h, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15): %Equal.sym(Bool, A.valid_length(List.length(&2, U32, key)), True{}, h) : {Laws.block_with(A.schedule_if(_, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{S.bytes_of(S.aes(key, S.state_of([b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15])))} : Maybe<&2, List<&2, U32>>} %C.encrypt_ok(S.nk(key), S.nr(key), key, T.S{T.W{b0, b1, b2, b3}, T.W{b4, b5, b6, b7}, T.W{b8, b9, b10, b11}, T.W{b12, b13, b14, b15}}) : {Laws.block_with(A.schedule_if(True{}, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{S.bytes_of(_)} : Maybe<&2, List<&2, U32>>} %GP.bytes_of_ok(A.encrypt(S.nk(key), S.nr(key), key, T.S{T.W{b0, b1, b2, b3}, T.W{b4, b5, b6, b7}, T.W{b8, b9, b10, b11}, T.W{b12, b13, b14, b15}})) : {Laws.block_with(A.schedule_if(True{}, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{_} : Maybe<&2, List<&2, U32>>} {==}def Laws.Block.aes128(key, h): %Equal.sym(Nat, List.length(&2, U32, key), 16n, h) : {Nat.div(_, 4n) == 4n : Nat} {==}def Laws.Block.aes192(key, h): %Equal.sym(Nat, List.length(&2, U32, key), 24n, h) : {Nat.div(_, 4n) == 6n : Nat} {==}def Laws.Block.aes256(key, h): %Equal.sym(Nat, List.length(&2, U32, key), 32n, h) : {Nat.div(_, 4n) == 8n : Nat} {==}def Laws.Gcm.seal(nk, nr, key, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt): GP.seal_ok(nk, nr, key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt)def Laws.Gcm.open(nk, nr, key, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, input): GP.open_ok(nk, nr, key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, input)def Laws.Aead.roundtrip(nk, nr, key, iv, aad, pt): AD.roundtrip(nk, nr, key, iv, aad, pt)def Laws.Aead.forgery(nk, nr, key, iv, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne): AD.forgery(nk, nr, key, iv, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)def Laws.Api128.encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt): API.aes128_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)def Laws.Api128.decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct): API.aes128_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)law open128_same: for +key: List<&2, U32> for +nonce: List<&2, U32> for +aad: List<&2, U32> for +m: Maybe<&2, List<&2, U32>> {Laws.open128(key, nonce, aad, m) == API.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}def open128_same(key, nonce, aad, m): match m: case None{}: {==} case Some{c}: {==}def Laws.Api128.roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt): +m = GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) Equal.trans(Maybe<&2, List<&2, U32>>, Laws.open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), Some{pt}, open128_same(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.aes128_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt))def Laws.Api128.forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne): API.aes128_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)def Laws.Api128.bad_key(key, h, nonce, aad, pt): %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 16n), False{}, h) : {GI.seal_key(GI.schedule_if(_, key), nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>} {==}def Laws.Api128.bad_key_open(key, h, nonce, aad, ct): %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 16n), False{}, h) : {GI.open_key(GI.schedule_if(_, key), nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>} {==}def Laws.Api128.bad_nonce(key, nonce, h, aad, pt): seal_key_bad(GI.schedule_of(16n, key), nonce, h, aad, pt)def Laws.Api128.bad_nonce_open(key, nonce, h, aad, ct): open_key_bad(GI.schedule_of(16n, key), nonce, h, aad, ct)def Laws.Api256.encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt): API.aes256_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)def Laws.Api256.decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct): API.aes256_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)law open256_same: for +key: List<&2, U32> for +nonce: List<&2, U32> for +aad: List<&2, U32> for +m: Maybe<&2, List<&2, U32>> {Laws.open256(key, nonce, aad, m) == API.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}def open256_same(key, nonce, aad, m): match m: case None{}: {==} case Some{c}: {==}def Laws.Api256.roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt): +m = GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) Equal.trans(Maybe<&2, List<&2, U32>>, Laws.open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), Some{pt}, open256_same(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.aes256_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt))def Laws.Api256.forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne): API.aes256_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)def Laws.Api256.bad_key(key, h, nonce, aad, pt): %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 32n), False{}, h) : {GI.seal_key(GI.schedule_if(_, key), nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>} {==}def Laws.Api256.bad_key_open(key, h, nonce, aad, ct): %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 32n), False{}, h) : {GI.open_key(GI.schedule_if(_, key), nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>} {==}def Laws.Api256.bad_nonce(key, nonce, h, aad, pt): seal_key_bad(GI.schedule_of(32n, key), nonce, h, aad, pt)def Laws.Api256.bad_nonce_open(key, nonce, h, aad, ct): open_key_bad(GI.schedule_of(32n, key), nonce, h, aad, ct)