~/bend-docscommunity

spec/crypto/aes/aes.bend checks

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

3 imports
import Base
import ../../../src/crypto/aes/types.bend as T
import ./poly.bend as P

Definitions

def bits source · line 11 · raw

@x:U32 -> List<&2, Bool>

Section 3.2/4: the byte b7 b6 ... b0 is the polynomial b7 x^7 + ... + b0.

def byte source · line 16 · raw

@w:Word(8n) -> U32

def low source · line 22 · raw

Word(8n)

Section 4.2: m(x) = x^8 + x^4 + x^3 + x + 1, so x^8 = x^4 + x^3 + x + 1.

def mul source · line 26 · raw

@+a:U32 -> @+b:U32 -> U32

Section 4.2: the product of two bytes is their polynomial product modulo m(x).

def inverse source · line 35 · raw

@+a:U32 -> U32

Section 4.4 / 5.1.1: the multiplicative inverse of a nonzero a in GF(2^8), {00} mapped to itself. The multiplicative group of GF(2^8) has 255 elements, so a^255 = {01} and a^-1 = a^254 for a != {00} (and {00}^254 = {00}): computed by squaring, a^254 = a^2 a^4 a^8 ... a^128. (tools/check_aes.py checks this against the defining property a * b = {01} for all 256 bytes.)

def nth_bit source · line 45 · raw

@xs:List<&2, Bool> -> @n:Nat -> Bool

def affine_bit source · line 56 · raw

@+b:List<&2, Bool> -> @+c:List<&2, Bool> -> @+i:Nat -> Bool

Section 5.1.1, equation (5.1): b'_i = b_i + b_(i+4 mod 8) + b_(i+5 mod 8) + b_(i+6 mod 8) + b_(i+7 mod 8) + c_i, with c = {63}.

def affine source · line 62 · raw

@+x:U32 -> U32

def sbox_byte source · line 70 · raw

@+x:U32 -> U32

Section 5.1.1: the S-box is the inverse followed by the affine transformation.

def byte8 source · line 74 · raw

@c0:Bool -> @c1:Bool -> @c2:Bool -> @c3:Bool -> @c4:Bool -> @c5:Bool -> @c6:Bool -> @c7:Bool -> U32

The byte c7..c0 (the S-box reads only the low eight bits of a U32).

def sbox_at source · line 80 · raw

@+c0:Bool -> @+c1:Bool -> @+c2:Bool -> @+c3:Bool -> @+c4:Bool -> @+c5:Bool -> @+c6:Bool -> @c7:Bool -> U32

Both arms are the S-box of the byte: the match on bit 7 only keeps a proof about a byte whose bits are unknown from expanding the field arithmetic (the specification is not run in constant time).

def sbox source · line 85 · raw

@x:U32 -> U32

def byte_at source · line 91 · raw

@w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @r:Nat -> U32

s[r,c]: byte r of column c.

def column source · line 102 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @c:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

def at source · line 113 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @+r:Nat -> @+c:Nat -> U32

def sub_word source · line 117 · raw

@w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

Section 5.1.1: SubBytes applies the S-box to every byte of the state.

def sub_bytes source · line 122 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def shifted source · line 128 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @+c:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

Section 5.1.2: s'[r,c] = s[r, (c + shift(r, 4)) mod 4], shift(r, 4) = r.

def shift_rows source · line 132 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def mix_column source · line 136 · raw

@w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

Section 5.1.3, equation (5.6).

def mix_columns source · line 144 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def xor_word source · line 149 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

def add_round_key source · line 155 · 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/types.State

Section 5.1.4: column c is added to the key word w[round*4 + c].

def rounds source · line 163 · raw

@n:Nat -> @s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @w:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

Section 5.1, Figure 5. After the initial AddRoundKey, n more full rounds (SubBytes, ShiftRows, MixColumns, AddRoundKey) and the final round (no MixColumns), each taking the next four words of the key schedule.

def cipher source · line 172 · raw

@+nr:Nat -> @s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> @w:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def rot_word source · line 180 · raw

@w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

Section 5.2: RotWord, SubWord (sub_word above), and Rcon[j] = [x^(j-1), 0, 0, 0].

def xpow source · line 185 · raw

@n:Nat -> U32

def rcon source · line 192 · raw

@j:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

def key_words source · line 196 · raw

@key:List<&2, U32> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad>

w[i] = [key[4i], key[4i+1], key[4i+2], key[4i+3]] for i < Nk.

def nth_word source · line 203 · raw

@ws:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> @n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

def transform source · line 214 · raw

@k:Nat -> @big:Bool -> @+q:Nat -> @temp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

The transformation of temp = w[i-1] in Figure 11, by k = i mod Nk, big = (Nk > 6) and q = i / Nk.

def next_word source · line 234 · raw

@+nk:Nat -> @+i:Nat -> @+history:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad

w[i] = w[i-Nk] xor transform(w[i-1]); history holds w[i-1], w[i-2], ...

def expand source · line 238 · raw

@n:Nat -> @+nk:Nat -> @+i:Nat -> @+history:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad>

def key_expansion source · line 246 · raw

@+nk:Nat -> @+nr:Nat -> @key:List<&2, U32> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.Quad>

Figure 11: Nb*(Nr+1) = 4*(Nr+1) words, the first Nk from the key.

def encrypt source · line 250 · raw

@+nk:Nat -> @+nr:Nat -> @key:List<&2, U32> -> @block:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def nk source · line 255 · raw

@+key:List<&2, U32> -> Nat

Figure 4: Nk is the key length in 32-bit words and Nr = Nk + 6 (AES-128: 4, 10; AES-192: 6, 12; AES-256: 8, 14).

def nr source · line 258 · raw

@+key:List<&2, U32> -> Nat

def aes source · line 262 · raw

@+key:List<&2, U32> -> @block:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

AES with the key's own Nk and Nr.

def aes128 source · line 265 · raw

@key:List<&2, U32> -> @block:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def aes256 source · line 268 · raw

@key:List<&2, U32> -> @block:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def nth_byte source · line 273 · raw

@xs:List<&2, U32> -> @n:Nat -> U32

Section 3.4: s[r,c] = in[r + 4c], out[r + 4c] = s[r,c]. Missing input bytes read as {00}.

def state_of source · line 282 · raw

@+input:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State

def bytes_of source · line 288 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> List<&2, U32>