|- ∀x. Sbox x = n2w (EL (w2n x) [99; 124; 119; 123; 242; 107; 111; 197; 48; 1; 103; 43; 254; 215; 171; 118; 202; 130; 201; 125; 250; 89; 71; 240; 173; 212; 162; 175; 156; 164; 114; 192; 183; 253; 147; 38; 54; 63; 247; 204; 52; 165; 229; 241; 113; 216; 49; 21; 4; 199; 35; 195; 24; 150; 5; 154; 7; 18; 128; 226; 235; 39; 178; 117; 9; 131; 44; 26; 27; 110; 90; 160; 82; 59; 214; 179; 41; 227; 47; 132; 83; 209; 0; 237; 32; 252; 177; 91; 106; 203; 190; 57; 74; 76; 88; 207; 208; 239; 170; 251; 67; 77; 51; 133; 69; 249; 2; 127; 80; 60; 159; 168; 81; 163; 64; 143; 146; 157; 56; 245; 188; 182; 218; 33; 16; 255; 243; 210; 205; 12; 19; 236; 95; 151; 68; 23; 196; 167; 126; 61; 100; 93; 25; 115; 96; 129; 79; 220; 34; 42; 144; 136; 70; 238; 184; 20; 222; 94; 11; 219; 224; 50; 58; 10; 73; 6; 36; 92; 194; 211; 172; 98; 145; 149; 228; 121; 231; 200; 55; 109; 141; 213; 78; 169; 108; 86; 244; 234; 101; 122; 174; 8; 186; 120; 37; 46; 28; 166; 180; 198; 232; 221; 116; 31; 75; 189; 139; 138; 112; 62; 181; 102; 72; 3; 246; 14; 97; 53; 87; 185; 134; 193; 29; 158; 225; 248; 152; 17; 105; 217; 142; 148; 155; 30; 135; 233; 206; 85; 40; 223; 140; 161; 137; 13; 191; 230; 66; 104; 65; 153; 45; 15; 176; 84; 187; 22]) |- ∀x. InvSbox x = n2w (EL (w2n x) [82; 9; 106; 213; 48; 54; 165; 56; 191; 64; 163; 158; 129; 243; 215; 251; 124; 227; 57; 130; 155; 47; 255; 135; 52; 142; 67; 68; 196; 222; 233; 203; 84; 123; 148; 50; 166; 194; 35; 61; 238; 76; 149; 11; 66; 250; 195; 78; 8; 46; 161; 102; 40; 217; 36; 178; 118; 91; 162; 73; 109; 139; 209; 37; 114; 248; 246; 100; 134; 104; 152; 22; 212; 164; 92; 204; 93; 101; 182; 146; 108; 112; 72; 80; 253; 237; 185; 218; 94; 21; 70; 87; 167; 141; 157; 132; 144; 216; 171; 0; 140; 188; 211; 10; 247; 228; 88; 5; 184; 179; 69; 6; 208; 44; 30; 143; 202; 63; 15; 2; 193; 175; 189; 3; 1; 19; 138; 107; 58; 145; 17; 65; 79; 103; 220; 234; 151; 242; 207; 206; 240; 180; 230; 115; 150; 172; 116; 34; 231; 173; 53; 133; 226; 249; 55; 232; 28; 117; 223; 110; 71; 241; 26; 113; 29; 41; 197; 137; 111; 183; 98; 14; 170; 24; 190; 27; 252; 86; 62; 75; 198; 210; 121; 32; 154; 219; 192; 254; 120; 205; 90; 244; 31; 221; 168; 51; 136; 7; 199; 49; 177; 18; 16; 89; 39; 128; 236; 95; 96; 81; 127; 169; 25; 181; 74; 13; 45; 229; 122; 159; 147; 201; 156; 239; 160; 224; 59; 77; 174; 42; 245; 176; 200; 235; 187; 60; 131; 83; 153; 97; 23; 43; 4; 126; 186; 119; 214; 38; 225; 105; 20; 99; 85; 33; 12; 125]) |- ∀S b00 b01 b02 b03 b10 b11 b12 b13 b20 b21 b22 b23 b30 b31 b32 b33. genSubBytes S (b00,b01,b02,b03,b10,b11,b12,b13,b20,b21,b22,b23,b30,b31,b32, b33) = (S b00,S b01,S b02,S b03,S b10,S b11,S b12,S b13,S b20,S b21,S b22, S b23,S b30,S b31,S b32,S b33) |- SubBytes = genSubBytes Sbox |- ∀b00 b01 b02 b03 b10 b11 b12 b13 b20 b21 b22 b23 b30 b31 b32 b33. ShiftRows (b00,b01,b02,b03,b10,b11,b12,b13,b20,b21,b22,b23,b30,b31,b32, b33) = (b00,b01,b02,b03,b11,b12,b13,b10,b22,b23,b20,b21,b33,b30,b31,b32) |- ∀a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15. XOR_BLOCK (a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15) (b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15) = (a0 ⊕ b0,a1 ⊕ b1,a2 ⊕ b2,a3 ⊕ b3,a4 ⊕ b4,a5 ⊕ b5,a6 ⊕ b6,a7 ⊕ b7, a8 ⊕ b8,a9 ⊕ b9,a10 ⊕ b10,a11 ⊕ b11,a12 ⊕ b12,a13 ⊕ b13,a14 ⊕ b14, a15 ⊕ b15) |- AddRoundKey = XOR_BLOCK |- ∀MC b00 b01 b02 b03 b10 b11 b12 b13 b20 b21 b22 b23 b30 b31 b32 b33. genMixColumns MC (b00,b01,b02,b03,b10,b11,b12,b13,b20,b21,b22,b23,b30,b31,b32, b33) = (let (b00',b10',b20',b30') = MC (b00,b10,b20,b30) in let (b01',b11',b21',b31') = MC (b01,b11,b21,b31) in let (b02',b12',b22',b32') = MC (b02,b12,b22,b32) in let (b03',b13',b23',b33') = MC (b03,b13,b23,b33) in (b00',b01',b02',b03',b10',b11',b12',b13',b20',b21',b22',b23', b30',b31',b32',b33')) |- ∀w. xtime w = w ≪ 1 ⊕ if word_msb w then 27w else 0w |- ∀b2 b1. b1 ** b2 = if b1 = 0w then 0w else if word_lsb b1 then b2 ⊕ b1 ⋙ 1 ** xtime b2 else b1 ⋙ 1 ** xtime b2 |- ∀a b c d. MultCol (a,b,c,d) = (2w ** a ⊕ 3w ** b ⊕ c ⊕ d,a ⊕ 2w ** b ⊕ 3w ** c ⊕ d, a ⊕ b ⊕ 2w ** c ⊕ 3w ** d,3w ** a ⊕ b ⊕ c ⊕ 2w ** d) |- MixColumns = genMixColumns MultCol |- ∀k0 k1 k2 k3 k4 k5 k6 k7 k8 k9 k10. ROTKEYS (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10) = (k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k0) |- RoundTuple (n,keys,state) = if n = 0 then (0,ROTKEYS keys, AddRoundKey (FST keys) (ShiftRows (SubBytes state))) else RoundTuple (n − 1,ROTKEYS keys, AddRoundKey (FST keys) (MixColumns (ShiftRows (SubBytes state)))) |- ∀n k s. Round n k s = SND (SND (RoundTuple (n,k,s))) |- ∀b0 b4 b8 b12 b1 b5 b9 b13 b2 b6 b10 b14 b3 b7 b11 b15. from_state (b0,b4,b8,b12,b1,b5,b9,b13,b2,b6,b10,b14,b3,b7,b11,b15) = (b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15) |- ∀b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15. to_state (b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15) = (b0,b4,b8,b12,b1,b5,b9,b13,b2,b6,b10,b14,b3,b7,b11,b15) |- ∀a b c d. InvMultCol (a,b,c,d) = (14w ** a ⊕ 11w ** b ⊕ 13w ** c ⊕ 9w ** d, 9w ** a ⊕ 14w ** b ⊕ 11w ** c ⊕ 13w ** d, 13w ** a ⊕ 9w ** b ⊕ 14w ** c ⊕ 11w ** d, 11w ** a ⊕ 13w ** b ⊕ 9w ** c ⊕ 14w ** d) |- InvMixColumns = genMixColumns InvMultCol |- ∀b00 b01 b02 b03 b11 b12 b13 b10 b22 b23 b20 b21 b33 b30 b31 b32. InvShiftRows (b00,b01,b02,b03,b11,b12,b13,b10,b22,b23,b20,b21,b33,b30,b31, b32) = (b00,b01,b02,b03,b10,b11,b12,b13,b20,b21,b22,b23,b30,b31,b32,b33) |- InvSubBytes = genSubBytes InvSbox |- InvRoundTuple (n,keys,state) = if n = 0 then (0,ROTKEYS keys, AddRoundKey (FST keys) (InvSubBytes (InvShiftRows state))) else InvRoundTuple (n − 1,ROTKEYS keys, InvMixColumns (AddRoundKey (FST keys) (InvSubBytes (InvShiftRows state)))) |- ∀n k s. InvRound n k s = SND (SND (InvRoundTuple (n,k,s))) |- ∀keys. AES_FWD keys = from_state o Round 9 (ROTKEYS keys) o AddRoundKey (FST keys) o to_state |- ∀keys. AES_BWD keys = from_state o InvRound 9 (ROTKEYS keys) o AddRoundKey (FST keys) o to_state