proofs/crypto/aes/cipher.bend checks

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

6 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 I
import ../../../spec/crypto/aes/aes.bend as S
import ./sbox.bend as L

Laws

law quad_cong provedsource · line 14 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+a2:U32 -> @+b2:U32 -> @+c2:U32 -> @+d2:U32 -> @+ea:{a == a2 : U32} -> @+eb:{b == b2 : U32} -> @+ec:{c == c2 : U32} -> @+ed:{d == d2 : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{a, b, c, d} == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{a2, b2, c2, d2} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

Congruence of the record constructors (one rewrite per field, on variables).

law state_cong provedsource · line 36 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+a2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+b2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+c2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+d2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+ea:{a == a2 : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad} -> @+eb:{b == b2 : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad} -> @+ec:{c == c2 : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad} -> @+ed:{d == d2 : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.S{a, b, c, d} == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.S{a2, b2, c2, d2} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law sub_word_ok provedsource · line 58 · raw

@+w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.sub_word(w) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sub_word(w) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law sub_bytes_ok provedsource · line 67 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.sub_bytes(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sub_bytes(s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law shift_rows_ok provedsource · line 76 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.shift_rows(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.shift_rows(s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law xor4_cong provedsource · line 85 · raw

@+p:U32 -> @+q:U32 -> @+r:U32 -> @+s:U32 -> @+p2:U32 -> @+q2:U32 -> @+r2:U32 -> @+s2:U32 -> @+ep:{p == p2 : U32} -> @+eq:{q == q2 : U32} -> @+er:{r == r2 : U32} -> @+es:{s == s2 : U32} -> {U32.xor(U32.xor(U32.xor(p, q), r), s) == U32.xor(U32.xor(U32.xor(p2, q2), r2), s2) : U32}

law mix_column_ok provedsource · line 107 · raw

@+w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.mix_column(w) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mix_column(w) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law mix_columns_ok provedsource · line 117 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.mix_columns(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mix_columns(s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law xor_word_ok provedsource · line 126 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.xor_word(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.xor_word(a, b) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law ark_ok provedsource · line 136 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @+w0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.add_round_key(s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.S{w0, w1, w2, w3}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.add_round_key(s, w0, w1, w2, w3) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law round_ok provedsource · line 153 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @+w0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.round(s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.S{w0, w1, w2, w3}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.add_round_key(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mix_columns(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.shift_rows(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sub_bytes(s))), w0, w1, w2, w3) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law last_round_ok provedsource · line 167 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @+w0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @+w3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.last_round(s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.S{w0, w1, w2, w3}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.add_round_key(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.shift_rows(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sub_bytes(s)), w0, w1, w2, w3) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law rounds_ok provedsource · line 180 · raw

@+n:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @+w:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.rounds(n, s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.round_keys(w)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.rounds(n, s, w) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law cipher_ok provedsource · line 210 · raw

@+nr:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @+w:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.cipher(nr, s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.round_keys(w)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.cipher(nr, s, w) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State}

law rot_word_ok provedsource · line 232 · raw

@+w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.rot_word(w) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.rot_word(w) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law xpow_ok provedsource · line 241 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.xpow(n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.xpow(n) : U32}

law rcon_ok provedsource · line 253 · raw

@+j:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.rcon(j) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.rcon(j) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law key_words_ok provedsource · line 261 · raw

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

law get_word_ok provedsource · line 279 · raw

@+ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> @+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.get_word(ws, n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_word(ws, n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law core_ok provedsource · line 293 · raw

@+k:Nat -> @+big:Bool -> @+q:Nat -> @+temp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.schedule_core(k, big, q, temp) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.transform(k, big, q, temp) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law next_ok provedsource · line 322 · raw

@+nk:Nat -> @+i:Nat -> @+h:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.next_word(nk, i, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.next_word(nk, i, h) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad}

law grow_ok provedsource · line 334 · raw

@+n:Nat -> @+nk:Nat -> @+i:Nat -> @+h:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.grow(n, nk, i, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.expand(n, nk, i, h) : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad>}

law expand_ok provedsource · line 349 · raw

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

law encrypt_ok provedsource · line 362 · 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 block.