check.bend
bend-osdev-cipher-modes@0.1.0.0 · 167 lines · 13 definitions
1
2
3
4
5
6
7
8import Base
9import bend-osdev-bytes@0.1.0.0/bytes.bend as B
10import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
11import bend-osdev-cipher-modes@0.1.0.0/aes.bend as X
12import bend-osdev-cipher-modes@0.1.0.0/cmac.bend as CM
13import bend-osdev-cipher-modes@0.1.0.0/aes_modes.bend as D
14
15def err(e: M.CmError) -> String:
16 match e:
17 case M.CmBadKeyLength{n}:
18 "CmBadKeyLength"
19 case M.CmBadIvLength{n}:
20 "CmBadIvLength"
21 case M.CmBadTweakLength{n}:
22 "CmBadTweakLength"
23 case M.CmBadNonceLength{n}:
24 "CmBadNonceLength"
25 case M.CmBadTagLength{n}:
26 "CmBadTagLength"
27 case M.CmBadBlockSize{n}:
28 "CmBadBlockSize"
29 case M.CmNotBlockMultiple{n}:
30 "CmNotBlockMultiple"
31 case M.CmTooShort{n}:
32 "CmTooShort"
33 case M.CmTooLong{n}:
34 "CmTooLong"
35 case M.CmBadPadding{}:
36 "CmBadPadding"
37 case M.CmTagMismatch{}:
38 "CmTagMismatch"
39
40def res(r: Result<&2, &2, M.CmError, B.Octets>) -> String:
41 match r:
42 case Fail{e}:
43 "fail " ++ err(e)
44 case Done{v}:
45 B.Octets.hex(v)
46
47
48
49
50
51
52def bulk.go(n: Nat, +s: U32, acc: List<&2, U32>) -> List<&2, U32>:
53 match n:
54 case 0n:
55 acc
56 case 1n+p:
57 +s2 = U32.add(U32.mul(s, 1103515245), 12345)
58 bulk.go(p, s2, Con{U32.and(U32.shrn(s2, 16n), 255), acc})
59
60def bulk.key() -> B.Octets:
61 B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60])
62
63def bulk.key2() -> B.Octets:
64 B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16])
65
66def bulk.iv() -> B.Octets:
67 B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15])
68
69def bulk.same(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String:
70 match r:
71 case Done{o}:
72 Bool.show(B.Octets.is_eq(o, m))
73 case Fail{e}:
74 "fail " ++ err(e)
75
76def bulk.cbc(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String:
77 match r:
78 case Done{+c}:
79 B.Octets.hex(B.Octets.drop(Nat.sub(B.Octets.len(c), 16n), c)) ++ " back " ++ bulk.same(D.CmAes.cbc_decrypt(bulk.key(), bulk.iv(), c), m)
80 case Fail{e}:
81 "fail " ++ err(e)
82
83def bulk.xts(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String:
84 match r:
85 case Done{+c}:
86 B.Octets.hex(B.Octets.drop(Nat.sub(B.Octets.len(c), 16n), c)) ++ " back " ++ bulk.same(D.CmAes.xts_decrypt(bulk.key2(), bulk.iv(), c), m)
87 case Fail{e}:
88 "fail " ++ err(e)
89
90def bulk.nonce() -> B.Octets:
91 B.Octets.of_list([0, 0, 0, 3, 2, 1, 0, 160, 161, 162, 163, 164])
92
93def bulk.aad() -> B.Octets:
94 B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7])
95
96def bulk.ccm(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String:
97 match r:
98 case Done{+c}:
99 B.Octets.hex(B.Octets.drop(Nat.sub(B.Octets.len(c), 16n), c)) ++ " back " ++ bulk.same(D.CmAes.ccm_decrypt(bulk.key(), 8n, bulk.nonce(), bulk.aad(), c), m)
100 case Fail{e}:
101 "fail " ++ err(e)
102
103def main() -> IO(Unit):
104 +m1 = B.Octets.of_list(bulk.go(32768n, 7, Nil{}))
105 +m2 = B.Octets.of_list(bulk.go(32773n, 7, Nil{}))
106 do IO<Unit>:
107 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])))))
108 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])))))
109 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])))))
110 IO.print("cbc_sp800_38a_f21 " ++ res(D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174, 45, 138, 87, 30, 3, 172, 156, 158, 183, 111, 172, 69, 175, 142, 81, 48, 200, 28, 70, 163, 92, 228, 17, 229, 251, 193, 25, 26, 10, 82, 239, 246, 159, 36, 69, 223, 79, 155, 23, 173, 43, 65, 123, 230, 108, 55, 16]))))
111 IO.print("cbc_sp800_38a_f22 " ++ res(D.CmAes.cbc_decrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([118, 73, 171, 172, 129, 25, 178, 70, 206, 233, 142, 155, 18, 233, 25, 125, 80, 134, 203, 155, 80, 114, 25, 238, 149, 219, 17, 58, 145, 118, 120, 178, 115, 190, 214, 184, 227, 193, 116, 59, 113, 22, 230, 158, 34, 34, 149, 22, 63, 241, 202, 161, 104, 31, 172, 9, 18, 14, 202, 48, 117, 134, 225, 167]))))
112 IO.print("cbc_sp800_38a_f25 " ++ res(D.CmAes.cbc_encrypt(B.Octets.of_list([96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119, 129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174, 45, 138, 87, 30, 3, 172, 156, 158, 183, 111, 172, 69, 175, 142, 81, 48, 200, 28, 70, 163, 92, 228, 17, 229, 251, 193, 25, 26, 10, 82, 239, 246, 159, 36, 69, 223, 79, 155, 23, 173, 43, 65, 123, 230, 108, 55, 16]))))
113 IO.print("cbc_sp800_38a_f26 " ++ res(D.CmAes.cbc_decrypt(B.Octets.of_list([96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119, 129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([245, 140, 76, 4, 214, 229, 241, 186, 119, 158, 171, 251, 95, 123, 251, 214, 156, 252, 78, 150, 126, 219, 128, 141, 103, 159, 119, 123, 198, 112, 44, 125, 57, 242, 51, 105, 169, 217, 186, 207, 165, 48, 226, 99, 4, 35, 20, 97, 178, 235, 5, 226, 195, 155, 233, 252, 218, 108, 25, 7, 140, 106, 157, 27]))))
114 IO.print("cbc_padded_f21 " ++ res(Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => B.Octets.take(64n, c), D.CmAes.cbc_encrypt_padded(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174, 45, 138, 87, 30, 3, 172, 156, 158, 183, 111, 172, 69, 175, 142, 81, 48, 200, 28, 70, 163, 92, 228, 17, 229, 251, 193, 25, 26, 10, 82, 239, 246, 159, 36, 69, 223, 79, 155, 23, 173, 43, 65, 123, 230, 108, 55, 16])))))
115 IO.print("xts_ieee1619_v1 " ++ res(D.CmAes.xts_encrypt(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))))
116 IO.print("xts_ieee1619_v2 " ++ res(D.CmAes.xts_encrypt(B.Octets.of_list([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34]), B.Octets.of_list([51, 51, 51, 51, 51, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68, 68]))))
117 IO.print("xts_ieee1619_v2_inverse " ++ res(D.CmAes.xts_decrypt(B.Octets.of_list([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34]), B.Octets.of_list([51, 51, 51, 51, 51, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([196, 84, 24, 94, 106, 22, 147, 110, 57, 51, 64, 56, 172, 239, 131, 139, 251, 24, 111, 255, 116, 128, 173, 196, 40, 147, 130, 236, 214, 211, 148, 240]))))
118 IO.print("xts_ieee1619_v15 " ++ res(D.CmAes.xts_encrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]))))
119 IO.print("xts_ieee1619_v15_inverse " ++ res(D.CmAes.xts_decrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([108, 22, 37, 219, 70, 113, 82, 45, 61, 117, 153, 96, 29, 231, 202, 9, 237]))))
120 IO.print("xts_ieee1619_v16 " ++ res(D.CmAes.xts_encrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17]))))
121 IO.print("xts_ieee1619_v17 " ++ res(D.CmAes.xts_encrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18]))))
122 IO.print("xts_ieee1619_v18 " ++ res(D.CmAes.xts_encrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19]))))
123 IO.print("xts_ieee1619_v18_inverse " ++ res(D.CmAes.xts_decrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([157, 132, 200, 19, 247, 25, 170, 44, 123, 227, 246, 97, 113, 199, 197, 194, 237, 191, 157, 172]))))
124 IO.print("ccm_rfc3610_p1 " ++ res(D.CmAes.ccm_encrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 8n, B.Octets.of_list([0, 0, 0, 3, 2, 1, 0, 160, 161, 162, 163, 164, 165]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30]))))
125 IO.print("ccm_rfc3610_p1_inverse " ++ res(D.CmAes.ccm_decrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 8n, B.Octets.of_list([0, 0, 0, 3, 2, 1, 0, 160, 161, 162, 163, 164, 165]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([88, 140, 151, 154, 97, 198, 99, 210, 240, 102, 208, 194, 192, 249, 137, 128, 109, 95, 107, 97, 218, 195, 132, 23, 232, 209, 44, 253, 249, 38, 224]))))
126 IO.print("ccm_rfc3610_p1_tampered " ++ res(D.CmAes.ccm_decrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 8n, B.Octets.of_list([0, 0, 0, 3, 2, 1, 0, 160, 161, 162, 163, 164, 165]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([88, 140, 151, 154, 97, 198, 99, 210, 240, 102, 208, 194, 192, 249, 137, 128, 109, 95, 107, 97, 218, 195, 132, 23, 232, 209, 44, 253, 249, 38, 225]))))
127 IO.print("ccm_rfc3610_p2 " ++ res(D.CmAes.ccm_encrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 8n, B.Octets.of_list([0, 0, 0, 4, 3, 2, 1, 160, 161, 162, 163, 164, 165]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31]))))
128 IO.print("ccm_rfc3610_p3 " ++ res(D.CmAes.ccm_encrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 8n, B.Octets.of_list([0, 0, 0, 5, 4, 3, 2, 160, 161, 162, 163, 164, 165]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]))))
129 IO.print("cmac_rfc4493_ex1 " ++ res(D.CmAes.cmac(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([]))))
130 IO.print("cmac_rfc4493_ex2 " ++ res(D.CmAes.cmac(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42]))))
131 IO.print("cmac_rfc4493_ex3 " ++ res(D.CmAes.cmac(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174, 45, 138, 87, 30, 3, 172, 156, 158, 183, 111, 172, 69, 175, 142, 81, 48, 200, 28, 70, 163, 92, 228, 17]))))
132 IO.print("cmac_rfc4493_ex4 " ++ res(D.CmAes.cmac(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174, 45, 138, 87, 30, 3, 172, 156, 158, 183, 111, 172, 69, 175, 142, 81, 48, 200, 28, 70, 163, 92, 228, 17, 229, 251, 193, 25, 26, 10, 82, 239, 246, 159, 36, 69, 223, 79, 155, 23, 173, 43, 65, 123, 230, 108, 55, 16]))))
133 IO.print("cmac_rfc4493_k2 " ++ res(Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(CM.Cmac.subkey2(~X.CmAesKey, ~X.CmAes.encrypt, k)), X.CmAes.key128(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60])))))
134 IO.print("cbc_32k " ++ bulk.cbc(D.CmAes.cbc_encrypt(bulk.key(), bulk.iv(), m1), m1))
135 IO.print("xts_32k " ++ bulk.xts(D.CmAes.xts_encrypt(bulk.key2(), bulk.iv(), m2), m2))
136 IO.print("ccm_32k " ++ bulk.ccm(D.CmAes.ccm_encrypt(bulk.key(), 8n, bulk.nonce(), bulk.aad(), m1), m1))
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167