check.bend
bend-osdev-aead@0.1.0.0 · 247 lines · 37 definitions
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15import Base
16import bend-osdev-bytes@0.1.0.0/bytes.bend as B
17import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
18import bend-osdev-cipher-modes@0.1.0.0/aes.bend as X
19import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
20import bend-osdev-crypto@0.1.0.0/inst_cm.bend as CM
21import bend-osdev-crypto@0.1.0.0/inst_aes.bend as A
22import bend-osdev-crypto@0.1.0.0/inst_ccm.bend as CC
23import bend-osdev-crypto@0.1.0.0/inst_sha2.bend as SH
24import bend-osdev-crypto@0.1.0.0/hmac.bend as Hm
25import bend-osdev-aead@0.1.0.0/aesround.bend as R
26import bend-osdev-aead@0.1.0.0/aegis128.bend as Ae
27import bend-osdev-aead@0.1.0.0/authenc.bend as Au
28import bend-osdev-aead@0.1.0.0/ivcipher.bend as Iv
29import bend-osdev-aead@0.1.0.0/essiv.bend as Es
30import bend-osdev-aead@0.1.0.0/seqiv.bend as Sq
31import bend-osdev-aead@0.1.0.0/echainiv.bend as Ec
32
33def cat(a: String, b: String) -> String:
34 a ++ b
35
36def err(e: Cr.CrError) -> String:
37 match e:
38 case Cr.CrBadKeyLength{n}:
39 cat("bad key length ", Nat.show(n))
40 case Cr.CrBadIvLength{n}:
41 cat("bad iv length ", Nat.show(n))
42 case Cr.CrBadNonceLength{n}:
43 cat("bad nonce length ", Nat.show(n))
44 case Cr.CrNotBlockMultiple{n}:
45 cat("not whole blocks ", Nat.show(n))
46 case Cr.CrTagMismatch{}:
47 "tag mismatch"
48 case Cr.CrTooShort{n}:
49 cat("too short ", Nat.show(n))
50 case _:
51 "other error"
52
53def show(r: Result<&2, &2, Cr.CrError, B.Octets>) -> String:
54 match r:
55 case Done{o}:
56 B.Octets.hex(o)
57 case Fail{e}:
58 err(e)
59
60def ad.check.base(digit: Bool) -> U32:
61 match digit:
62 case True{}:
63 48
64 case False{}:
65 87
66
67def ad.check.nib(+c: U32) -> U32:
68 U32.sub(c, ad.check.base(U32.is_lt(c, 58)))
69
70def ad.check.hex(cs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
71 match cs:
72 case Con{a, Con{b, t}}:
73 ad.check.hex(t, Con{U32.add(U32.mul(ad.check.nib(a), 16), ad.check.nib(b)), acc})
74 case _:
75 B.rev(acc)
76
77def hx(s: String) -> B.Octets:
78 B.Octets.of_list(ad.check.hex(B.Octets.to_list(B.Octets.of_string(s)), Nil{}))
79
80
81def both(e: Result<&2, &2, Cr.CrError, B.Octets>, d: Result<&2, &2, Cr.CrError, B.Octets>) -> String:
82 cat(show(e), cat(" ", show(d)))
83
84
85
86def aegis(+k: B.Octets, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> String:
87 +r = Ae.AdAegis128.key(k)
88 +c = Result.bind(&2, &2, Cr.CrError, Ae.AdAegisKey, B.Octets, r, kk => Ae.AdAegis128.seal(kk, n, a, p))
89 both(c, Result.bind(&2, &2, Cr.CrError, Ae.AdAegisKey, B.Octets, r, kk => Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, c, x => Ae.AdAegis128.open(kk, n, a, x))))
90
91def aegis_seal(+k: B.Octets, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> String:
92 show(Result.bind(&2, &2, Cr.CrError, Ae.AdAegisKey, B.Octets, Ae.AdAegis128.key(k), kk => Ae.AdAegis128.seal(kk, n, a, p)))
93
94def aegis_open(+k: B.Octets, +n: B.Octets, +a: B.Octets, +c: B.Octets) -> String:
95 show(Result.bind(&2, &2, Cr.CrError, Ae.AdAegisKey, B.Octets, Ae.AdAegis128.key(k), kk => Ae.AdAegis128.open(kk, n, a, c)))
96
97
98
99def au.enc(k: X.CmAesKey, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
100 Iv.AdCbc.encrypt(~X.CmAesKey, ~M.CmBlock, ~16n, ~X.CmAes.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, k, iv, m)
101
102def au.dec(k: X.CmAesKey, iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
103 Iv.AdCbc.decrypt(~X.CmAesKey, ~M.CmBlock, ~16n, ~X.CmAes.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, k, iv, c)
104
105def au.encp(k: X.CmAesKey, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
106 Iv.AdCbc.encrypt_padded(~X.CmAesKey, ~M.CmBlock, ~16n, ~X.CmAes.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, k, iv, m)
107
108def au.decp(k: X.CmAesKey, iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
109 Iv.AdCbc.decrypt_padded(~X.CmAesKey, ~M.CmBlock, ~16n, ~X.CmAes.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, k, iv, c)
110
111def au.mac(k: Hm.CrHmacKey, m: B.Octets) -> B.Octets:
112 Hm.CrHmac.mac(~SH.CrSha2.sha256, k, m)
113
114def au.mkey(o: B.Octets) -> Result<&2, &2, Cr.CrError, Hm.CrHmacKey>:
115 Hm.CrHmac.key_of(~64n, ~SH.CrSha2.sha256, o)
116
117def au.key(o: B.Octets) -> Result<&2, &2, Cr.CrError, Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>>:
118 Au.AdAuthenc.key(~X.CmAesKey, ~Hm.CrHmacKey, ~A.CrAes.key, ~au.mkey, ~16n, o)
119
120
121def au.seal_k(k: Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, iv: B.Octets, a: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
122 Au.AdAuthenc.seal(~X.CmAesKey, ~Hm.CrHmacKey, ~au.enc, ~au.mac, ~Au.AdAuthenc.input_kernel, ~32n, k, iv, a, p)
123
124def au.open_k(k: Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, iv: B.Octets, a: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
125 Au.AdAuthenc.open(~X.CmAesKey, ~Hm.CrHmacKey, ~au.dec, ~au.mac, ~Au.AdAuthenc.input_kernel, ~32n, k, iv, a, c)
126
127
128def au.seal_m(k: Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, iv: B.Octets, a: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
129 Au.AdAuthenc.seal(~X.CmAesKey, ~Hm.CrHmacKey, ~au.encp, ~au.mac, ~Au.AdAuthenc.input_mcgrew, ~16n, k, iv, a, p)
130
131def au.open_m(k: Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, iv: B.Octets, a: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
132 Au.AdAuthenc.open(~X.CmAesKey, ~Hm.CrHmacKey, ~au.decp, ~au.mac, ~Au.AdAuthenc.input_mcgrew, ~16n, k, iv, a, c)
133
134def authenc(~seal: Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey> -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~open: Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey> -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: B.Octets, +iv: B.Octets, +a: B.Octets, +p: B.Octets) -> String:
135 +r = au.key(k)
136 +c = Result.bind(&2, &2, Cr.CrError, Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, B.Octets, r, kk => seal(kk, iv, a, p))
137 both(c, Result.bind(&2, &2, Cr.CrError, Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, B.Octets, r, kk => Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, c, x => open(kk, iv, a, x))))
138
139def authenc_open(~open: Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey> -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: B.Octets, +iv: B.Octets, +a: B.Octets, +c: B.Octets) -> String:
140 show(Result.bind(&2, &2, Cr.CrError, Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, B.Octets, au.key(k), kk => open(kk, iv, a, c)))
141
142
143
144def es.key(o: B.Octets) -> Result<&2, &2, Cr.CrError, Es.AdEssivKey<X.CmAesKey, X.CmAesKey>>:
145 Es.AdEssiv.key(~X.CmAesKey, ~X.CmAesKey, ~A.CrAes.key, ~A.CrAes.key, ~SH.CrSha2.sha256, o)
146
147def es.enc(k: Es.AdEssivKey<X.CmAesKey, X.CmAesKey>, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
148 Es.AdEssiv.encrypt(~X.CmAesKey, ~X.CmAesKey, ~M.CmBlock, ~X.CmAes.encrypt, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, ~au.enc, k, iv, m)
149
150def es.dec(k: Es.AdEssivKey<X.CmAesKey, X.CmAesKey>, iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
151 Es.AdEssiv.decrypt(~X.CmAesKey, ~X.CmAesKey, ~M.CmBlock, ~X.CmAes.encrypt, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, ~au.dec, k, iv, c)
152
153def essiv(+k: B.Octets, +iv: B.Octets, +p: B.Octets) -> String:
154 +r = es.key(k)
155 +c = Result.bind(&2, &2, Cr.CrError, Es.AdEssivKey<X.CmAesKey, X.CmAesKey>, B.Octets, r, kk => es.enc(kk, iv, p))
156 both(c, Result.bind(&2, &2, Cr.CrError, Es.AdEssivKey<X.CmAesKey, X.CmAesKey>, B.Octets, r, kk => Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, c, x => es.dec(kk, iv, x))))
157
158
159
160def ccm.seal(k: X.CmAesKey, n: B.Octets, a: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
161 CC.CrCcm.seal(~X.CmAesKey, ~X.CmAes.encrypt, ~16n, k, n, a, p)
162
163def ccm.open(k: X.CmAesKey, n: B.Octets, a: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
164 CC.CrCcm.open(~X.CmAesKey, ~X.CmAes.encrypt, ~16n, k, n, a, c)
165
166def sq.key(o: B.Octets) -> Result<&2, &2, Cr.CrError, Sq.AdSeqivKey<X.CmAesKey>>:
167 Sq.AdSeqiv.key(~X.CmAesKey, ~A.CrAes.key, ~12n, o)
168
169def seqiv(+k: B.Octets, +seq: B.Octets, +a: B.Octets, +p: B.Octets) -> String:
170 +r = sq.key(k)
171 +c = Result.bind(&2, &2, Cr.CrError, Sq.AdSeqivKey<X.CmAesKey>, B.Octets, r, kk => Sq.AdSeqiv.seal(~X.CmAesKey, ~ccm.seal, kk, seq, a, p))
172 both(c, Result.bind(&2, &2, Cr.CrError, Sq.AdSeqivKey<X.CmAesKey>, B.Octets, r, kk => Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, c, x => Sq.AdSeqiv.open(~X.CmAesKey, ~ccm.open, ~12n, kk, seq, a, x))))
173
174def seqiv_open(+k: B.Octets, +seq: B.Octets, +a: B.Octets, +c: B.Octets) -> String:
175 show(Result.bind(&2, &2, Cr.CrError, Sq.AdSeqivKey<X.CmAesKey>, B.Octets, sq.key(k), kk => Sq.AdSeqiv.open(~X.CmAesKey, ~ccm.open, ~12n, kk, seq, a, c)))
176
177
178
179def ec.key(ak: B.Octets, ck: B.Octets, salt: B.Octets) -> Result<&2, &2, Cr.CrError, Ec.AdEchainivKey<Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, X.CmAesKey>>:
180 Ec.AdEchainiv.key(~Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, ~X.CmAesKey, ~au.key, ~A.CrAes.key, ak, ck, salt)
181
182def echainiv(+ak: B.Octets, +ck: B.Octets, +salt: B.Octets, +seq: B.Octets, +a: B.Octets, +p: B.Octets) -> String:
183 +r = ec.key(ak, ck, salt)
184 +c = Result.bind(&2, &2, Cr.CrError, Ec.AdEchainivKey<Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, X.CmAesKey>, B.Octets, r, kk => Ec.AdEchainiv.seal(~Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, ~X.CmAesKey, ~M.CmBlock, ~X.CmAes.encrypt, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, ~au.seal_k, kk, seq, a, p))
185 both(c, Result.bind(&2, &2, Cr.CrError, Ec.AdEchainivKey<Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, X.CmAesKey>, B.Octets, r, kk => Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, c, x => Ec.AdEchainiv.open(~Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, ~X.CmAesKey, ~au.open_k, ~16n, kk, seq, a, x))))
186
187def echainiv_open(+ak: B.Octets, +ck: B.Octets, +salt: B.Octets, +seq: B.Octets, +a: B.Octets, +c: B.Octets) -> String:
188 show(Result.bind(&2, &2, Cr.CrError, Ec.AdEchainivKey<Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, X.CmAesKey>, B.Octets, ec.key(ak, ck, salt), kk => Ec.AdEchainiv.open(~Au.AdAuthencKey<X.CmAesKey, Hm.CrHmacKey>, ~X.CmAesKey, ~au.open_k, ~16n, kk, seq, a, c)))
189
190def main() -> IO(Unit):
191 +z16 = B.Octets.zeros(16n)
192 +k = hx("000102030405060708090a0b0c0d0e0f")
193 +n = hx("101112131415161718191a1b1c1d1e1f")
194 +kr = hx("000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f")
195 +pr = B.Octets.of_string("A cipher system must not be required to be secret, and it must be able to fall into the hands of the enemy without inconvenience")
196 +ivr = hx("1af38c2dc2b96ffdd86694092341bc04")
197 +ar = B.Octets.of_string("The second principle of Auguste Kerckhoffs")
198 +ak = hx("202122232425262728292a2b2c2d2e2f303132333435363738393a3b3c3d3e3f000102030405060708090a0b0c0d0e0f")
199 +m32 = hx("000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f")
200 +sk = hx("000102030405060708090a0b0c0d0e0fa0a1a2a3a4a5a6a7a8a9aaab")
201 do IO<Unit>:
202 IO.print(R.AdBlk.hex(R.AdAes.round(R.AdAes.sbox(), R.AdBlk.of_octets(hx("000102030405060708090a0b0c0d0e0f")), R.AdBlk.of_octets(hx("101112131415161718191a1b1c1d1e1f")))))
203 IO.print(aegis(z16, z16, B.Octets.empty(), B.Octets.empty()))
204 IO.print(aegis(z16, z16, B.Octets.empty(), z16))
205 IO.print(aegis(k, n, hx("0001020304050607"), m32))
206 IO.print(aegis(k, n, hx("00010203"), hx("000102030405060708090a0b0c")))
207 IO.print(aegis(k, n, B.Octets.of_string("associated data, two blocks long"), B.Octets.of_string("a message of sixty-one bytes, which ends in a partial block...")))
208 IO.print(aegis_open(k, n, hx("00010203"), hx("000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c")))
209 IO.print(aegis_seal(hx("000102030405060708090a0b0c0d0e"), n, B.Octets.empty(), B.Octets.empty()))
210 IO.print(aegis_seal(k, hx("101112131415161718191a1b1c1d1e"), B.Octets.empty(), B.Octets.empty()))
211 IO.print(aegis_open(k, n, B.Octets.empty(), hx("000102030405060708090a0b0c0d0e")))
212 IO.print(authenc(~au.seal_m, ~au.open_m, kr, ivr, ar, pr))
213 IO.print(authenc(~au.seal_k, ~au.open_k, kr, ivr, ar, m32))
214 IO.print(authenc_open(~au.open_m, kr, ivr, ar, hx("c80edfa32ddf39d5ef00c0b468834279a2e46a1b8049f792f76bfe54b903a9c9a94ac9b47ad2655c5f10f9aef71427e2fc6f9b3f399a221489f16362c703233609d45ac69864e3321cf82935ac4096c86e133314c54019e8ca7980dfa4b9cf1b384c486f3a54c51078158ee5d79de59fbd34d848b3d69550a67646344427ade54b8851ffb598f7f80074b9473c82e2db652c3fa36b0a7c5b3219fab3a30bc1c5")))
215 IO.print(authenc_open(~au.open_k, kr, ivr, ar, hx("00")))
216 IO.print(essiv(kr, hx("00000000000000000000000000000000"), m32))
217 IO.print(essiv(k, hx("07000000000000000000000000000000"), B.Octets.zeros(64n)))
218 IO.print(seqiv(sk, hx("0000000000000001"), hx("0001020304050607"), B.Octets.of_string("seqiv over AES-CCM")))
219 IO.print(seqiv(sk, hx("00000000000000ff00000002"), B.Octets.empty(), B.Octets.empty()))
220 IO.print(seqiv_open(sk, hx("0000000000000001"), hx("0001020304050607"), hx("a1a1a2a3a4a5a6a7a8a9aaaa0d0593fbd64079e780eac7a612cbc2c361abf939db30bd025719f04d7e5611335a36")))
221 IO.print(seqiv_open(sk, hx("0000000000000001"), hx("0001020304050607"), hx("a0a1a2a3a4a5")))
222 IO.print(echainiv(ak, k, n, hx("0000000000000001"), hx("0001020304050607"), m32))
223 IO.print(echainiv(ak, k, n, hx("0000000000000002"), B.Octets.empty(), B.Octets.zeros(48n)))
224 IO.print(echainiv_open(ak, k, n, hx("0000000000000001"), hx("0001020304050607"), hx("5f7ed55606bdb961c1821f3964f0677519fae8ab350e663f77fc5e7c714699385a8f006affb14b20ca29241a76851a0baf0e8efc707dcaf9a1b324015191ccebd83f61f0f2787a85a647e10061197f69")))
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247