LAWS.bend

bend-osdev-hashes@0.1.0.0 · 430 lines · 77 definitions

1# Generated by gen/laws.py; do not edit by hand.
2#
3# The laws of the hashes, for every input where they are proved:
4# streaming (update over a ++ b is update over a, then b, from every
5# state), the digest in any pieces equals the one-shot digest, and the
6# digest's length; then the specifications' vectors. The engine's streaming
7# law is stated once, for every chaining value and compression function;
8# each hash's is that law at its own defs.
9import Base
10import bend-osdev-bytes@0.1.0.0/bytes.bend as B
11import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
12import bend-osdev-hashes@0.1.0.0/md4.bend as M4
13import bend-osdev-hashes@0.1.0.0/md5.bend as M5
14import bend-osdev-hashes@0.1.0.0/sha1.bend as S1
15import bend-osdev-hashes@0.1.0.0/ripemd160.bend as RM
16import bend-osdev-hashes@0.1.0.0/sm3.bend as SM
17import bend-osdev-hashes@0.1.0.0/streebog.bend as ST
18import bend-osdev-hashes@0.1.0.0/michael.bend as MI
19
20# The engine (hashes.bend), for every chaining value type, compression
21# function and block size: a ++ b is a, then b, from every state
22law md_streaming:
23  for ~C: Data
24  for ~compress: C -> List<&2, U32> -> C
25  for ~last: U32
26  for s: Hs.HsMdState<C>
27  for +a: B.Octets
28  for +b: B.Octets
29  {Hs.HsMd.update(~C, ~compress, ~last, s, B.Octets.append(a, b)) == Hs.HsMd.update(~C, ~compress, ~last, Hs.HsMd.update(~C, ~compress, ~last, s, a), b) : Hs.HsMdState<C>}
30
31# MD4 (RFC 1320) (md4.bend)
32
33# MD4 (RFC 1320): update over a ++ b is update over a, then b, from every state
34law md4_streaming:
35  for s: Hs.HsMdState<Hs.HsW4>
36  for +a: B.Octets
37  for +b: B.Octets
38  {M4.HsMd4.update(s, B.Octets.append(a, b)) == M4.HsMd4.update(M4.HsMd4.update(s, a), b) : Hs.HsMdState<Hs.HsW4>}
39
40# MD4 (RFC 1320): the digest in two pieces is the one-shot digest, for every split
41law md4_split:
42  for +a: B.Octets
43  for +b: B.Octets
44  {M4.HsMd4.final(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.init(), a), b)) == M4.HsMd4.digest(B.Octets.append(a, b)) : B.Octets}
45
46# MD4 (RFC 1320): and in three pieces
47law md4_split3:
48  for +a: B.Octets
49  for +b: B.Octets
50  for +c: B.Octets
51  {M4.HsMd4.final(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.init(), a), b), c)) == M4.HsMd4.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
52
53# MD4 (RFC 1320): the digest of every state has 16 bytes
54law md4_length:
55  for +s: Hs.HsMdState<Hs.HsW4>
56  {B.Octets.len(M4.HsMd4.final(s)) == 16n : Nat}
57
58# MD4 (RFC 1320): the digest of every message has 16 bytes
59law md4_digest_length:
60  for +m: B.Octets
61  {B.Octets.len(M4.HsMd4.digest(m)) == 16n : Nat}
62
63# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
64law md4_rfc1320_1:
65  {M4.HsMd4.digest(B.Octets.of_string("")) == B.Octets.of_list([49, 214, 207, 224, 209, 106, 233, 49, 183, 60, 89, 215, 224, 192, 137, 192]) : B.Octets}
66
67# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
68law md4_rfc1320_2:
69  {M4.HsMd4.digest(B.Octets.of_string("a")) == B.Octets.of_list([189, 229, 44, 179, 29, 227, 62, 70, 36, 94, 5, 251, 219, 214, 251, 36]) : B.Octets}
70
71# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
72law md4_rfc1320_3:
73  {M4.HsMd4.digest(B.Octets.of_string("abc")) == B.Octets.of_list([164, 72, 1, 122, 175, 33, 216, 82, 95, 193, 10, 232, 122, 166, 114, 157]) : B.Octets}
74
75# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
76law md4_rfc1320_4:
77  {M4.HsMd4.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([217, 19, 10, 129, 100, 84, 159, 232, 24, 135, 72, 6, 225, 199, 1, 75]) : B.Octets}
78
79# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
80law md4_rfc1320_5:
81  {M4.HsMd4.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([215, 158, 28, 48, 138, 165, 187, 205, 238, 168, 237, 99, 223, 65, 45, 169]) : B.Octets}
82
83# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
84law md4_rfc1320_6:
85  {M4.HsMd4.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([4, 63, 133, 130, 242, 65, 219, 53, 28, 230, 39, 225, 83, 231, 240, 228]) : B.Octets}
86
87# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
88law md4_rfc1320_7:
89  {M4.HsMd4.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([227, 59, 77, 220, 156, 56, 242, 25, 156, 62, 123, 22, 79, 204, 5, 54]) : B.Octets}
90
91# MD5 (RFC 1321) (md5.bend)
92
93# MD5 (RFC 1321): update over a ++ b is update over a, then b, from every state
94law md5_streaming:
95  for s: Hs.HsMdState<Hs.HsW4>
96  for +a: B.Octets
97  for +b: B.Octets
98  {M5.HsMd5.update(s, B.Octets.append(a, b)) == M5.HsMd5.update(M5.HsMd5.update(s, a), b) : Hs.HsMdState<Hs.HsW4>}
99
100# MD5 (RFC 1321): the digest in two pieces is the one-shot digest, for every split
101law md5_split:
102  for +a: B.Octets
103  for +b: B.Octets
104  {M5.HsMd5.final(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.init(), a), b)) == M5.HsMd5.digest(B.Octets.append(a, b)) : B.Octets}
105
106# MD5 (RFC 1321): and in three pieces
107law md5_split3:
108  for +a: B.Octets
109  for +b: B.Octets
110  for +c: B.Octets
111  {M5.HsMd5.final(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.init(), a), b), c)) == M5.HsMd5.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
112
113# MD5 (RFC 1321): the digest of every state has 16 bytes
114law md5_length:
115  for +s: Hs.HsMdState<Hs.HsW4>
116  {B.Octets.len(M5.HsMd5.final(s)) == 16n : Nat}
117
118# MD5 (RFC 1321): the digest of every message has 16 bytes
119law md5_digest_length:
120  for +m: B.Octets
121  {B.Octets.len(M5.HsMd5.digest(m)) == 16n : Nat}
122
123# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
124law md5_rfc1321_1:
125  {M5.HsMd5.digest(B.Octets.of_string("")) == B.Octets.of_list([212, 29, 140, 217, 143, 0, 178, 4, 233, 128, 9, 152, 236, 248, 66, 126]) : B.Octets}
126
127# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
128law md5_rfc1321_2:
129  {M5.HsMd5.digest(B.Octets.of_string("a")) == B.Octets.of_list([12, 193, 117, 185, 192, 241, 182, 168, 49, 195, 153, 226, 105, 119, 38, 97]) : B.Octets}
130
131# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
132law md5_rfc1321_3:
133  {M5.HsMd5.digest(B.Octets.of_string("abc")) == B.Octets.of_list([144, 1, 80, 152, 60, 210, 79, 176, 214, 150, 63, 125, 40, 225, 127, 114]) : B.Octets}
134
135# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
136law md5_rfc1321_4:
137  {M5.HsMd5.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([249, 107, 105, 125, 124, 183, 147, 141, 82, 90, 47, 49, 170, 241, 97, 208]) : B.Octets}
138
139# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
140law md5_rfc1321_5:
141  {M5.HsMd5.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([195, 252, 211, 215, 97, 146, 228, 0, 125, 251, 73, 108, 202, 103, 225, 59]) : B.Octets}
142
143# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
144law md5_rfc1321_6:
145  {M5.HsMd5.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([209, 116, 171, 152, 210, 119, 217, 245, 165, 97, 28, 44, 159, 65, 157, 159]) : B.Octets}
146
147# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
148law md5_rfc1321_7:
149  {M5.HsMd5.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([87, 237, 244, 162, 43, 227, 201, 85, 172, 73, 218, 46, 33, 7, 182, 122]) : B.Octets}
150
151# SHA-1 (FIPS 180-4) (sha1.bend)
152
153# SHA-1 (FIPS 180-4): update over a ++ b is update over a, then b, from every state
154law sha1_streaming:
155  for s: Hs.HsMdState<Hs.HsW5>
156  for +a: B.Octets
157  for +b: B.Octets
158  {S1.HsSha1.update(s, B.Octets.append(a, b)) == S1.HsSha1.update(S1.HsSha1.update(s, a), b) : Hs.HsMdState<Hs.HsW5>}
159
160# SHA-1 (FIPS 180-4): the digest in two pieces is the one-shot digest, for every split
161law sha1_split:
162  for +a: B.Octets
163  for +b: B.Octets
164  {S1.HsSha1.final(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.init(), a), b)) == S1.HsSha1.digest(B.Octets.append(a, b)) : B.Octets}
165
166# SHA-1 (FIPS 180-4): and in three pieces
167law sha1_split3:
168  for +a: B.Octets
169  for +b: B.Octets
170  for +c: B.Octets
171  {S1.HsSha1.final(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.init(), a), b), c)) == S1.HsSha1.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
172
173# SHA-1 (FIPS 180-4): the digest of every state has 20 bytes
174law sha1_length:
175  for +s: Hs.HsMdState<Hs.HsW5>
176  {B.Octets.len(S1.HsSha1.final(s)) == 20n : Nat}
177
178# SHA-1 (FIPS 180-4): the digest of every message has 20 bytes
179law sha1_digest_length:
180  for +m: B.Octets
181  {B.Octets.len(S1.HsSha1.digest(m)) == 20n : Nat}
182
183# SHA-1 (FIPS 180-4): FIPS 180-4's examples (NIST's SHA-1 example values): "abc" and the 448-bit message
184law sha1_fips_1:
185  {S1.HsSha1.digest(B.Octets.of_string("abc")) == B.Octets.of_list([169, 153, 62, 54, 71, 6, 129, 106, 186, 62, 37, 113, 120, 80, 194, 108, 156, 208, 216, 157]) : B.Octets}
186
187# SHA-1 (FIPS 180-4): FIPS 180-4's examples (NIST's SHA-1 example values): "abc" and the 448-bit message
188law sha1_fips_2:
189  {S1.HsSha1.digest(B.Octets.of_string("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == B.Octets.of_list([132, 152, 62, 68, 28, 59, 210, 110, 186, 174, 74, 161, 249, 81, 41, 229, 229, 70, 112, 241]) : B.Octets}
190
191# RIPEMD-160 (ripemd160.bend)
192
193# RIPEMD-160: update over a ++ b is update over a, then b, from every state
194law ripemd160_streaming:
195  for s: Hs.HsMdState<Hs.HsW5>
196  for +a: B.Octets
197  for +b: B.Octets
198  {RM.HsRipemd160.update(s, B.Octets.append(a, b)) == RM.HsRipemd160.update(RM.HsRipemd160.update(s, a), b) : Hs.HsMdState<Hs.HsW5>}
199
200# RIPEMD-160: the digest in two pieces is the one-shot digest, for every split
201law ripemd160_split:
202  for +a: B.Octets
203  for +b: B.Octets
204  {RM.HsRipemd160.final(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.init(), a), b)) == RM.HsRipemd160.digest(B.Octets.append(a, b)) : B.Octets}
205
206# RIPEMD-160: and in three pieces
207law ripemd160_split3:
208  for +a: B.Octets
209  for +b: B.Octets
210  for +c: B.Octets
211  {RM.HsRipemd160.final(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.init(), a), b), c)) == RM.HsRipemd160.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
212
213# RIPEMD-160: the digest of every state has 20 bytes
214law ripemd160_length:
215  for +s: Hs.HsMdState<Hs.HsW5>
216  {B.Octets.len(RM.HsRipemd160.final(s)) == 20n : Nat}
217
218# RIPEMD-160: the digest of every message has 20 bytes
219law ripemd160_digest_length:
220  for +m: B.Octets
221  {B.Octets.len(RM.HsRipemd160.digest(m)) == 20n : Nat}
222
223# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
224law ripemd160_paper_1:
225  {RM.HsRipemd160.digest(B.Octets.of_string("")) == B.Octets.of_list([156, 17, 133, 165, 197, 233, 252, 84, 97, 40, 8, 151, 126, 232, 245, 72, 178, 37, 141, 49]) : B.Octets}
226
227# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
228law ripemd160_paper_2:
229  {RM.HsRipemd160.digest(B.Octets.of_string("a")) == B.Octets.of_list([11, 220, 157, 45, 37, 107, 62, 233, 218, 174, 52, 123, 230, 244, 220, 131, 90, 70, 127, 254]) : B.Octets}
230
231# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
232law ripemd160_paper_3:
233  {RM.HsRipemd160.digest(B.Octets.of_string("abc")) == B.Octets.of_list([142, 178, 8, 247, 224, 93, 152, 122, 155, 4, 74, 142, 152, 198, 176, 135, 241, 90, 11, 252]) : B.Octets}
234
235# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
236law ripemd160_paper_4:
237  {RM.HsRipemd160.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([93, 6, 137, 239, 73, 210, 250, 229, 114, 184, 129, 177, 35, 168, 95, 250, 33, 89, 95, 54]) : B.Octets}
238
239# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
240law ripemd160_paper_5:
241  {RM.HsRipemd160.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([247, 28, 39, 16, 156, 105, 44, 27, 86, 187, 220, 235, 91, 157, 40, 101, 179, 112, 141, 188]) : B.Octets}
242
243# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
244law ripemd160_paper_6:
245  {RM.HsRipemd160.digest(B.Octets.of_string("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == B.Octets.of_list([18, 160, 83, 56, 74, 156, 12, 136, 228, 5, 160, 108, 39, 220, 244, 154, 218, 98, 235, 43]) : B.Octets}
246
247# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
248law ripemd160_paper_7:
249  {RM.HsRipemd160.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([176, 226, 11, 110, 49, 22, 100, 2, 134, 237, 58, 135, 165, 113, 48, 121, 178, 31, 81, 137]) : B.Octets}
250
251# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
252law ripemd160_paper_8:
253  {RM.HsRipemd160.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([155, 117, 46, 69, 87, 61, 75, 57, 244, 219, 211, 50, 60, 171, 130, 191, 99, 50, 107, 251]) : B.Octets}
254
255# SM3 (GB/T 32905) (sm3.bend)
256
257# SM3 (GB/T 32905): update over a ++ b is update over a, then b, from every state
258law sm3_streaming:
259  for s: Hs.HsMdState<Hs.HsW8>
260  for +a: B.Octets
261  for +b: B.Octets
262  {SM.HsSm3.update(s, B.Octets.append(a, b)) == SM.HsSm3.update(SM.HsSm3.update(s, a), b) : Hs.HsMdState<Hs.HsW8>}
263
264# SM3 (GB/T 32905): the digest in two pieces is the one-shot digest, for every split
265law sm3_split:
266  for +a: B.Octets
267  for +b: B.Octets
268  {SM.HsSm3.final(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.init(), a), b)) == SM.HsSm3.digest(B.Octets.append(a, b)) : B.Octets}
269
270# SM3 (GB/T 32905): and in three pieces
271law sm3_split3:
272  for +a: B.Octets
273  for +b: B.Octets
274  for +c: B.Octets
275  {SM.HsSm3.final(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.init(), a), b), c)) == SM.HsSm3.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
276
277# SM3 (GB/T 32905): the digest of every state has 32 bytes
278law sm3_length:
279  for +s: Hs.HsMdState<Hs.HsW8>
280  {B.Octets.len(SM.HsSm3.final(s)) == 32n : Nat}
281
282# SM3 (GB/T 32905): the digest of every message has 32 bytes
283law sm3_digest_length:
284  for +m: B.Octets
285  {B.Octets.len(SM.HsSm3.digest(m)) == 32n : Nat}
286
287# SM3 (GB/T 32905): draft-shen-sm3-hash-01, examples 1 and 2
288law sm3_example_1:
289  {SM.HsSm3.digest(B.Octets.of_string("abc")) == B.Octets.of_list([102, 199, 240, 244, 98, 238, 237, 217, 209, 242, 212, 107, 220, 16, 228, 226, 65, 103, 196, 135, 92, 242, 247, 162, 41, 125, 160, 43, 143, 75, 168, 224]) : B.Octets}
290
291# SM3 (GB/T 32905): draft-shen-sm3-hash-01, examples 1 and 2
292law sm3_example_2:
293  {SM.HsSm3.digest(B.Octets.of_string("abcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcd")) == B.Octets.of_list([222, 190, 159, 249, 34, 117, 184, 161, 56, 96, 72, 137, 193, 142, 90, 77, 111, 219, 112, 229, 56, 126, 87, 101, 41, 61, 203, 163, 156, 12, 87, 50]) : B.Octets}
294
295# Streebog-512 (RFC 6986) (streebog.bend)
296
297# Streebog-512 (RFC 6986): update over a ++ b is update over a, then b, from every state
298law streebog512_streaming:
299  for s: Hs.HsMdState<ST.HsStbCv>
300  for +a: B.Octets
301  for +b: B.Octets
302  {ST.HsStreebog.update(s, B.Octets.append(a, b)) == ST.HsStreebog.update(ST.HsStreebog.update(s, a), b) : Hs.HsMdState<ST.HsStbCv>}
303
304# Streebog-512 (RFC 6986): the digest in two pieces is the one-shot digest, for every split
305law streebog512_split:
306  for +a: B.Octets
307  for +b: B.Octets
308  {ST.HsStreebog.final512(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init512(), a), b)) == ST.HsStreebog.digest512(B.Octets.append(a, b)) : B.Octets}
309
310# Streebog-512 (RFC 6986): and in three pieces
311law streebog512_split3:
312  for +a: B.Octets
313  for +b: B.Octets
314  for +c: B.Octets
315  {ST.HsStreebog.final512(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init512(), a), b), c)) == ST.HsStreebog.digest512(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
316
317# Streebog-512 (RFC 6986): the digest of every state has 64 bytes
318law streebog512_length:
319  for +s: Hs.HsMdState<ST.HsStbCv>
320  {B.Octets.len(ST.HsStreebog.final512(s)) == 64n : Nat}
321
322# Streebog-512 (RFC 6986): the digest of every message has 64 bytes
323law streebog512_digest_length:
324  for +m: B.Octets
325  {B.Octets.len(ST.HsStreebog.digest512(m)) == 64n : Nat}
326
327# Streebog-256 (RFC 6986) (streebog.bend)
328
329# Streebog-256 (RFC 6986): update over a ++ b is update over a, then b, from every state
330law streebog256_streaming:
331  for s: Hs.HsMdState<ST.HsStbCv>
332  for +a: B.Octets
333  for +b: B.Octets
334  {ST.HsStreebog.update(s, B.Octets.append(a, b)) == ST.HsStreebog.update(ST.HsStreebog.update(s, a), b) : Hs.HsMdState<ST.HsStbCv>}
335
336# Streebog-256 (RFC 6986): the digest in two pieces is the one-shot digest, for every split
337law streebog256_split:
338  for +a: B.Octets
339  for +b: B.Octets
340  {ST.HsStreebog.final256(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init256(), a), b)) == ST.HsStreebog.digest256(B.Octets.append(a, b)) : B.Octets}
341
342# Streebog-256 (RFC 6986): and in three pieces
343law streebog256_split3:
344  for +a: B.Octets
345  for +b: B.Octets
346  for +c: B.Octets
347  {ST.HsStreebog.final256(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init256(), a), b), c)) == ST.HsStreebog.digest256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
348
349# Streebog-256 (RFC 6986): the digest of every state has 32 bytes
350law streebog256_length:
351  for +s: Hs.HsMdState<ST.HsStbCv>
352  {B.Octets.len(ST.HsStreebog.final256(s)) == 32n : Nat}
353
354# Streebog-256 (RFC 6986): the digest of every message has 32 bytes
355law streebog256_digest_length:
356  for +m: B.Octets
357  {B.Octets.len(ST.HsStreebog.digest256(m)) == 32n : Nat}
358
359# Streebog's transformations (streebog.bend): RFC 6986, section 10.1, example 1
360
361# Streebog-512, K = LPS(h xor N) = LPS(0^512) (RFC 6986 prints it most significant byte first)
362law streebog_lps_zero:
363  {ST.HsStreebog.lps(B.Octets.zeros(64n)) == B.Octets.of_list([116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179]) : B.Octets}
364
365# Streebog-512, the first compression, g_N(h, m) with h = N = 0 and m the padded M1 (RFC 6986 prints it most significant byte first)
366law streebog_g_example1:
367  {ST.HsStreebog.g(B.Octets.zeros(64n), B.Octets.zeros(64n), B.Octets.of_list([48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 1])) == B.Octets.of_list([226, 218, 59, 107, 115, 228, 254, 5, 217, 245, 177, 63, 121, 53, 65, 149, 92, 129, 80, 44, 82, 15, 237, 211, 197, 186, 187, 140, 144, 246, 84, 39, 189, 142, 115, 51, 219, 138, 72, 38, 166, 169, 90, 68, 65, 102, 168, 23, 56, 79, 57, 33, 175, 52, 234, 145, 17, 203, 44, 129, 248, 44, 16, 253]) : B.Octets}
368
369# Streebog-512, g_0(h, N) after it, N = 504 (RFC 6986 prints it most significant byte first)
370law streebog_g0_example1:
371  {ST.HsStreebog.g(B.Octets.zeros(64n), B.Octets.of_list([226, 218, 59, 107, 115, 228, 254, 5, 217, 245, 177, 63, 121, 53, 65, 149, 92, 129, 80, 44, 82, 15, 237, 211, 197, 186, 187, 140, 144, 246, 84, 39, 189, 142, 115, 51, 219, 138, 72, 38, 166, 169, 90, 68, 65, 102, 168, 23, 56, 79, 57, 33, 175, 52, 234, 145, 17, 203, 44, 129, 248, 44, 16, 253]), B.Octets.of_list([248, 1])) == B.Octets.of_list([124, 29, 119, 231, 93, 26, 144, 168, 1, 69, 211, 98, 214, 225, 55, 144, 127, 110, 166, 25, 79, 161, 71, 33, 98, 148, 55, 109, 157, 182, 45, 61, 82, 151, 213, 212, 103, 112, 187, 170, 235, 22, 23, 11, 42, 111, 2, 66, 182, 20, 13, 194, 254, 228, 194, 150, 241, 92, 105, 36, 217, 31, 136, 92]) : B.Octets}
372
373# Michael (michael.bend): the same laws, under every key
374
375# Michael (IEEE 802.11i): update over a ++ b is update over a, then b, from every state
376law michael_streaming:
377  for s: Hs.HsMdState<Hs.HsW2>
378  for +a: B.Octets
379  for +b: B.Octets
380  {MI.HsMichael.update(s, B.Octets.append(a, b)) == MI.HsMichael.update(MI.HsMichael.update(s, a), b) : Hs.HsMdState<Hs.HsW2>}
381
382# Michael (IEEE 802.11i): the tag in two pieces is the one-call tag, for every key and split
383law michael_split:
384  for +k: Hs.HsW2
385  for +a: B.Octets
386  for +b: B.Octets
387  {MI.HsMichael.final(MI.HsMichael.update(MI.HsMichael.update(MI.HsMichael.init(k), a), b)) == MI.HsMichael.mic(k, B.Octets.append(a, b)) : B.Octets}
388
389# Michael (IEEE 802.11i): the tag of every state has 8 bytes
390law michael_length:
391  for +s: Hs.HsMdState<Hs.HsW2>
392  {B.Octets.len(MI.HsMichael.final(s)) == 8n : Nat}
393
394# Michael (IEEE 802.11i): the tag of every message under every key has 8 bytes
395law michael_mic_length:
396  for +k: Hs.HsW2
397  for +m: B.Octets
398  {B.Octets.len(MI.HsMichael.mic(k, m)) == 8n : Nat}
399
400# Michael (IEEE 802.11i): a key of 7 bytes is refused
401law michael_short_key:
402  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, Unit, k => Unit{}, MI.HsMichael.key(B.Octets.zeros(7n))) == Fail{Hs.HsBadKeyLength{7n}} : Result<&2, &2, Hs.HsError, Unit>}
403
404# Michael (IEEE 802.11i): test vector 1 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
405law michael_vector_1:
406  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("")), MI.HsMichael.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0]))) == Done{B.Octets.of_list([130, 146, 92, 28, 161, 209, 48, 184])} : Result<&2, &2, Hs.HsError, B.Octets>}
407
408# Michael (IEEE 802.11i): test vector 2 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
409law michael_vector_2:
410  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("M")), MI.HsMichael.key(B.Octets.of_list([130, 146, 92, 28, 161, 209, 48, 184]))) == Done{B.Octets.of_list([67, 71, 33, 202, 64, 99, 155, 63])} : Result<&2, &2, Hs.HsError, B.Octets>}
411
412# Michael (IEEE 802.11i): test vector 3 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
413law michael_vector_3:
414  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mi")), MI.HsMichael.key(B.Octets.of_list([67, 71, 33, 202, 64, 99, 155, 63]))) == Done{B.Octets.of_list([232, 249, 190, 202, 233, 126, 93, 41])} : Result<&2, &2, Hs.HsError, B.Octets>}
415
416# Michael (IEEE 802.11i): test vector 4 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
417law michael_vector_4:
418  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mic")), MI.HsMichael.key(B.Octets.of_list([232, 249, 190, 202, 233, 126, 93, 41]))) == Done{B.Octets.of_list([144, 3, 143, 198, 207, 19, 193, 219])} : Result<&2, &2, Hs.HsError, B.Octets>}
419
420# Michael (IEEE 802.11i): test vector 5 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
421law michael_vector_5:
422  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mich")), MI.HsMichael.key(B.Octets.of_list([144, 3, 143, 198, 207, 19, 193, 219]))) == Done{B.Octets.of_list([213, 94, 16, 5, 16, 18, 137, 134])} : Result<&2, &2, Hs.HsError, B.Octets>}
423
424# Michael (IEEE 802.11i): test vector 6 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
425law michael_vector_6:
426  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Michael")), MI.HsMichael.key(B.Octets.of_list([213, 94, 16, 5, 16, 18, 137, 134]))) == Done{B.Octets.of_list([10, 148, 43, 18, 78, 202, 165, 70])} : Result<&2, &2, Hs.HsError, B.Octets>}
427
428# Michael (IEEE 802.11i): IEEE Std 802.11-2012, M.6.3 (the TKIP test vector, as hostap's BSD-licensed wlantest/test_vectors.c reproduces it): the MIC of its MSDU (DA, SA, priority 0 and three zero bytes, then the data) under TK bytes 16 to 23
429law michael_tkip_m63:
430  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_list([2, 3, 4, 5, 6, 8, 2, 3, 4, 5, 6, 7, 0, 0, 0, 0, 170, 170, 3, 0, 0, 0, 8, 0, 69, 0, 0, 84, 0, 0, 64, 0, 64, 1, 165, 85, 192, 168, 10, 2, 192, 168, 10, 1, 8, 0, 58, 176, 0, 0, 0, 0, 205, 76, 5, 0, 0, 0, 0, 0, 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, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55])), MI.HsMichael.key(B.Octets.of_list([52, 86, 120, 144, 18, 52, 86, 120]))) == Done{B.Octets.of_list([104, 129, 163, 243, 214, 72, 208, 60])} : Result<&2, &2, Hs.HsError, B.Octets>}