check.bend

bend-osdev-aes@0.1.0.0 · 54 lines · 3 definitions

1# FIPS 197 (2001) Appendix C: C.1 (AES-128) decryption, C.2 (AES-192) and
2# C.3 (AES-256) both ways, run compiled (C.1's encryption is a law,
3# aes128_fips197_c1). The checker evaluates AES slowly and keeps what it
4# evaluates, so these are not laws.
5import Base
6import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
8import bend-osdev-aes@0.1.0.0/aes.bend as X
9
10def err(e: M.CmError) -> String:
11  match e:
12    case M.CmBadKeyLength{n}:
13      "CmBadKeyLength"
14    case M.CmBadIvLength{n}:
15      "CmBadIvLength"
16    case M.CmBadTweakLength{n}:
17      "CmBadTweakLength"
18    case M.CmBadNonceLength{n}:
19      "CmBadNonceLength"
20    case M.CmBadTagLength{n}:
21      "CmBadTagLength"
22    case M.CmBadBlockSize{n}:
23      "CmBadBlockSize"
24    case M.CmNotBlockMultiple{n}:
25      "CmNotBlockMultiple"
26    case M.CmTooShort{n}:
27      "CmTooShort"
28    case M.CmTooLong{n}:
29      "CmTooLong"
30    case M.CmBadPadding{}:
31      "CmBadPadding"
32    case M.CmTagMismatch{}:
33      "CmTagMismatch"
34
35def res(r: Result<&2, &2, M.CmError, B.Octets>) -> String:
36  match r:
37    case Fail{e}:
38      "fail " ++ err(e)
39    case Done{v}:
40      B.Octets.hex(v)
41
42def main() -> IO(Unit):
43  do IO<Unit>:
44    IO.print("aes128_fips197_c1_inverse " ++ res(Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.decrypt(k, M.CmBlock{1774510296, 1786446896, 3637360512, 1890895194})), X.CmAes.key128(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15])))))
45    IO.print("aes192_fips197_c2 " ++ res(Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703})), X.CmAes.key192(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23])))))
46    IO.print("aes192_fips197_c2_inverse " ++ res(Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.decrypt(k, M.CmBlock{3718872228, 2253184992, 1856991392, 3960304017})), X.CmAes.key192(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23])))))
47    IO.print("aes256_fips197_c3 " ++ res(Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703})), X.CmAes.key256(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31])))))
48    IO.print("aes256_fips197_c3_inverse " ++ res(Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.decrypt(k, M.CmBlock{2393028554, 1365722559, 3942402448, 1263100041})), X.CmAes.key256(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31])))))
49
50#|aes128_fips197_c1_inverse 00112233445566778899aabbccddeeff
51#|aes192_fips197_c2 dda97ca4864cdfe06eaf70a0ec0d7191
52#|aes192_fips197_c2_inverse 00112233445566778899aabbccddeeff
53#|aes256_fips197_c3 8ea2b7ca516745bfeafc49904b496089
54#|aes256_fips197_c3_inverse 00112233445566778899aabbccddeeff