~/jendhub

LAWS.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 363 lines · 58 definitions

1# Laws about the public interface of every cipher in the package.
2#
3# Properties, for every input: each block cipher's decryption undoes its
4# encryption, and its encryption undoes its decryption, for every key and
5# every block (so each is a permutation of the blocks), for the 128-bit
6# ciphers (SM4, Camellia, Serpent, Twofish, ARIA, CAST-256) and the 64-bit
7# ones (DES, 3DES, Blowfish, CAST-128, TEA, XTEA, FCrypt); the 64-bit modes undo
8# themselves for DES and 3DES; RC4 applied twice from one state gives the
9# data back, and RC4 in pieces is RC4 of the whole; 64-bit blocks survive
10# their byte form.
11#
12# Vectors: the specifications' own test values, proved by computation (see
13# the end of the file).
14import Base
15import bend-osdev-bytes@0.1.0.0/bytes.bend as B
16import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
17import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
18import bend-osdev-legacy-ciphers@0.1.0.0/des.bend as D
19import bend-osdev-legacy-ciphers@0.1.0.0/tdes.bend as T
20import bend-osdev-legacy-ciphers@0.1.0.0/sm4.bend as S
21import bend-osdev-legacy-ciphers@0.1.0.0/camellia.bend as C
22import bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend as P
23import bend-osdev-legacy-ciphers@0.1.0.0/twofish.bend as F
24import bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend as R
25import bend-osdev-legacy-ciphers@0.1.0.0/modes64.bend as X
26import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A
27import bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend as C6
28import bend-osdev-legacy-ciphers@0.1.0.0/blowfish.bend as BF
29import bend-osdev-legacy-ciphers@0.1.0.0/cast5.bend as C5
30import bend-osdev-legacy-ciphers@0.1.0.0/tea.bend as TE
31import bend-osdev-legacy-ciphers@0.1.0.0/xtea.bend as XT
32import bend-osdev-legacy-ciphers@0.1.0.0/fcrypt.bend as FC
33
34# DES (FIPS 46-3)
35
36law des_round_trip:
37  for k: D.LcDesKey
38  for +b: L.LcBlock64
39  {D.LcDes.decrypt(k, D.LcDes.encrypt(k, b)) == b : L.LcBlock64}
40
41law des_round_trip_dual:
42  for k: D.LcDesKey
43  for +b: L.LcBlock64
44  {D.LcDes.encrypt(k, D.LcDes.decrypt(k, b)) == b : L.LcBlock64}
45
46# Triple DES (SP 800-67), for every key bundle (any three DES keys)
47
48law tdes_round_trip:
49  for k: T.LcTdesKey
50  for +b: L.LcBlock64
51  {T.LcTdes.decrypt(k, T.LcTdes.encrypt(k, b)) == b : L.LcBlock64}
52
53law tdes_round_trip_dual:
54  for k: T.LcTdesKey
55  for +b: L.LcBlock64
56  {T.LcTdes.encrypt(k, T.LcTdes.decrypt(k, b)) == b : L.LcBlock64}
57
58# SM4 (GB/T 32907-2016)
59
60law sm4_round_trip:
61  for k: S.LcSm4Key
62  for +b: M.CmBlock
63  {S.LcSm4.decrypt(k, S.LcSm4.encrypt(k, b)) == b : M.CmBlock}
64
65law sm4_round_trip_dual:
66  for k: S.LcSm4Key
67  for +b: M.CmBlock
68  {S.LcSm4.encrypt(k, S.LcSm4.decrypt(k, b)) == b : M.CmBlock}
69
70# Camellia (RFC 3713), every key size
71
72law camellia_round_trip:
73  for k: C.LcCamelliaKey
74  for +b: M.CmBlock
75  {C.LcCamellia.decrypt(k, C.LcCamellia.encrypt(k, b)) == b : M.CmBlock}
76
77law camellia_round_trip_dual:
78  for k: C.LcCamelliaKey
79  for +b: M.CmBlock
80  {C.LcCamellia.encrypt(k, C.LcCamellia.decrypt(k, b)) == b : M.CmBlock}
81
82# Serpent (the AES submission), every key size
83
84law serpent_round_trip:
85  for k: P.LcSerpentKey
86  for +b: M.CmBlock
87  {P.LcSerpent.decrypt(k, P.LcSerpent.encrypt(k, b)) == b : M.CmBlock}
88
89law serpent_round_trip_dual:
90  for k: P.LcSerpentKey
91  for +b: M.CmBlock
92  {P.LcSerpent.encrypt(k, P.LcSerpent.decrypt(k, b)) == b : M.CmBlock}
93
94# Twofish (Schneier et al.), every key size
95
96law twofish_round_trip:
97  for k: F.LcTwofishKey
98  for +b: M.CmBlock
99  {F.LcTwofish.decrypt(k, F.LcTwofish.encrypt(k, b)) == b : M.CmBlock}
100
101law twofish_round_trip_dual:
102  for k: F.LcTwofishKey
103  for +b: M.CmBlock
104  {F.LcTwofish.encrypt(k, F.LcTwofish.decrypt(k, b)) == b : M.CmBlock}
105
106# ARIA (RFC 5794), every key size
107
108law aria_round_trip:
109  for k: A.LcAriaKey
110  for +b: M.CmBlock
111  {A.LcAria.decrypt(k, A.LcAria.encrypt(k, b)) == b : M.CmBlock}
112
113law aria_round_trip_dual:
114  for k: A.LcAriaKey
115  for +b: M.CmBlock
116  {A.LcAria.encrypt(k, A.LcAria.decrypt(k, b)) == b : M.CmBlock}
117
118# CAST-256 (RFC 2612), every key size
119
120law cast6_round_trip:
121  for k: C6.LcCast6Key
122  for +b: M.CmBlock
123  {C6.LcCast6.decrypt(k, C6.LcCast6.encrypt(k, b)) == b : M.CmBlock}
124
125law cast6_round_trip_dual:
126  for k: C6.LcCast6Key
127  for +b: M.CmBlock
128  {C6.LcCast6.encrypt(k, C6.LcCast6.decrypt(k, b)) == b : M.CmBlock}
129
130# Blowfish (Schneier), every key
131
132law blowfish_round_trip:
133  for k: BF.LcBlowfishKey
134  for +b: L.LcBlock64
135  {BF.LcBlowfish.decrypt(k, BF.LcBlowfish.encrypt(k, b)) == b : L.LcBlock64}
136
137law blowfish_round_trip_dual:
138  for k: BF.LcBlowfishKey
139  for +b: L.LcBlock64
140  {BF.LcBlowfish.encrypt(k, BF.LcBlowfish.decrypt(k, b)) == b : L.LcBlock64}
141
142# CAST-128 (RFC 2144), every key size
143
144law cast5_round_trip:
145  for k: C5.LcCast5Key
146  for +b: L.LcBlock64
147  {C5.LcCast5.decrypt(k, C5.LcCast5.encrypt(k, b)) == b : L.LcBlock64}
148
149law cast5_round_trip_dual:
150  for k: C5.LcCast5Key
151  for +b: L.LcBlock64
152  {C5.LcCast5.encrypt(k, C5.LcCast5.decrypt(k, b)) == b : L.LcBlock64}
153
154# TEA (Wheeler and Needham), every key, byte order and number of cycles
155
156law tea_round_trip:
157  for k: TE.LcTeaKey
158  for +b: L.LcBlock64
159  {TE.LcTea.decrypt(k, TE.LcTea.encrypt(k, b)) == b : L.LcBlock64}
160
161law tea_round_trip_dual:
162  for k: TE.LcTeaKey
163  for +b: L.LcBlock64
164  {TE.LcTea.encrypt(k, TE.LcTea.decrypt(k, b)) == b : L.LcBlock64}
165
166# XTEA (Needham and Wheeler), every key, byte order and number of cycles
167
168law xtea_round_trip:
169  for k: XT.LcXteaKey
170  for +b: L.LcBlock64
171  {XT.LcXtea.decrypt(k, XT.LcXtea.encrypt(k, b)) == b : L.LcBlock64}
172
173law xtea_round_trip_dual:
174  for k: XT.LcXteaKey
175  for +b: L.LcBlock64
176  {XT.LcXtea.encrypt(k, XT.LcXtea.decrypt(k, b)) == b : L.LcBlock64}
177
178# FCrypt (the AFS specification), every key
179
180law fcrypt_round_trip:
181  for k: FC.LcFcryptKey
182  for +b: L.LcBlock64
183  {FC.LcFcrypt.decrypt(k, FC.LcFcrypt.encrypt(k, b)) == b : L.LcBlock64}
184
185law fcrypt_round_trip_dual:
186  for k: FC.LcFcryptKey
187  for +b: L.LcBlock64
188  {FC.LcFcrypt.encrypt(k, FC.LcFcrypt.decrypt(k, b)) == b : L.LcBlock64}
189
190# RC4 (RFC 6229), for every state (so for every key) and all data
191
192# the cipher is its own inverse: from one state, applied twice, the data
193# comes back
194law rc4_involution:
195  for +st: R.LcRc4State
196  for +m: B.Octets
197  {R.LcRc4.out_data(R.LcRc4.update(st, R.LcRc4.out_data(R.LcRc4.update(st, m)))) == m : B.Octets}
198
199# data in pieces: the output of a ++ b is the output of a, then the output
200# of b from the state after a; and the state after a ++ b is the state
201# after a, then b
202law rc4_streaming_data:
203  for +st: R.LcRc4State
204  for +a: B.Octets
205  for +b: B.Octets
206  {R.LcRc4.out_data(R.LcRc4.update(st, B.Octets.append(a, b))) == B.Octets.append(R.LcRc4.out_data(R.LcRc4.update(st, a)), R.LcRc4.out_data(R.LcRc4.update(R.LcRc4.out_state(R.LcRc4.update(st, a)), b))) : B.Octets}
207
208law rc4_streaming_state:
209  for +st: R.LcRc4State
210  for +a: B.Octets
211  for +b: B.Octets
212  {R.LcRc4.out_state(R.LcRc4.update(st, B.Octets.append(a, b))) == R.LcRc4.out_state(R.LcRc4.update(R.LcRc4.out_state(R.LcRc4.update(st, a)), b)) : R.LcRc4State}
213
214# 64-bit blocks as bytes: a block read back from its 8 bytes is itself, and
215# a list of blocks read back from its bytes is itself
216law block64_octets_round_trip:
217  for +b: L.LcBlock64
218  {L.LcBlock64.of_octets(L.LcBlock64.to_octets(b)) == Some{b} : Maybe<&2, L.LcBlock64>}
219
220law blocks64_octets_round_trip:
221  for +bs: List<&2, L.LcBlock64>
222  {X.Lc64.blocks_of(X.Lc64.octets_of(bs)) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>}
223
224# The 64-bit modes undo themselves for DES and 3DES, for every key, IV and
225# message: on blocks, and on bytes (every message of whole blocks is the
226# bytes of its blocks, Lc64.octets_of)
227
228law des_ecb_round_trip:
229  for +k: D.LcDesKey
230  for +bs: List<&2, L.LcBlock64>
231  {X.Lc64.ecb_decrypt_blocks(~D.LcDesKey, ~D.LcDes.decrypt, k, X.Lc64.ecb_encrypt_blocks(~D.LcDesKey, ~D.LcDes.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
232
233law des_cbc_round_trip:
234  for +k: D.LcDesKey
235  for +iv: L.LcBlock64
236  for +bs: List<&2, L.LcBlock64>
237  {X.Lc64.cbc_decrypt_blocks(~D.LcDesKey, ~D.LcDes.decrypt, k, iv, X.Lc64.cbc_encrypt_blocks(~D.LcDesKey, ~D.LcDes.encrypt, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
238
239law tdes_ecb_round_trip:
240  for +k: T.LcTdesKey
241  for +bs: List<&2, L.LcBlock64>
242  {X.Lc64.ecb_decrypt_blocks(~T.LcTdesKey, ~T.LcTdes.decrypt, k, X.Lc64.ecb_encrypt_blocks(~T.LcTdesKey, ~T.LcTdes.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
243
244law tdes_cbc_round_trip:
245  for +k: T.LcTdesKey
246  for +iv: L.LcBlock64
247  for +bs: List<&2, L.LcBlock64>
248  {X.Lc64.cbc_decrypt_blocks(~T.LcTdesKey, ~T.LcTdes.decrypt, k, iv, X.Lc64.cbc_encrypt_blocks(~T.LcTdesKey, ~T.LcTdes.encrypt, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
249
250law des_cbc_octets_round_trip:
251  for +k: D.LcDesKey
252  for +iv: L.LcBlock64
253  for +bs: List<&2, L.LcBlock64>
254  {Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.cbc_encrypt(~D.LcDesKey, ~D.LcDes.encrypt, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)), c => X.Lc64.cbc_decrypt(~D.LcDesKey, ~D.LcDes.decrypt, k, L.LcBlock64.to_octets(iv), c)) == Done{X.Lc64.octets_of(bs)} : Result<&2, &2, L.LcError, B.Octets>}
255
256law tdes_cbc_octets_round_trip:
257  for +k: T.LcTdesKey
258  for +iv: L.LcBlock64
259  for +bs: List<&2, L.LcBlock64>
260  {Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.cbc_encrypt(~T.LcTdesKey, ~T.LcTdes.encrypt, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)), c => X.Lc64.cbc_decrypt(~T.LcTdesKey, ~T.LcTdes.decrypt, k, L.LcBlock64.to_octets(iv), c)) == Done{X.Lc64.octets_of(bs)} : Result<&2, &2, L.LcError, B.Octets>}
261
262law des_ecb_octets_round_trip:
263  for +k: D.LcDesKey
264  for +bs: List<&2, L.LcBlock64>
265  {Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.ecb_encrypt(~D.LcDesKey, ~D.LcDes.encrypt, k, X.Lc64.octets_of(bs)), c => X.Lc64.ecb_decrypt(~D.LcDesKey, ~D.LcDes.decrypt, k, c)) == Done{X.Lc64.octets_of(bs)} : Result<&2, &2, L.LcError, B.Octets>}
266
267law tdes_ecb_octets_round_trip:
268  for +k: T.LcTdesKey
269  for +bs: List<&2, L.LcBlock64>
270  {Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.ecb_encrypt(~T.LcTdesKey, ~T.LcTdes.encrypt, k, X.Lc64.octets_of(bs)), c => X.Lc64.ecb_decrypt(~T.LcTdesKey, ~T.LcTdes.decrypt, k, c)) == Done{X.Lc64.octets_of(bs)} : Result<&2, &2, L.LcError, B.Octets>}
271
272# Vectors: the specifications' own test values, proved by computation. Some
273# run compiled in check.bend instead: the Twofish paper's (one Twofish key
274# schedule takes about 2.5 GB in the checker), and DES's, 3DES's and RC4's
275# (the checker proves them, but they run past the --verdict kernel's
276# evaluation budget: RC4's 256-step key schedule does, 128 steps do not).
277
278# BEGIN GENERATED by gen/vectors.py: vectors
279# GB/T 32907-2016, Appendix A, example 1: key = plaintext =
280# 0123456789ABCDEFFEDCBA9876543210, ciphertext 681EDF34D206965E86B3E94F536E4246
281law sm4_gbt32907:
282  {Result.map(&2, &2, L.LcError, S.LcSm4Key, M.CmBlock, k => S.LcSm4.encrypt(k, M.CmBlock{19088743, 2309737967, 4275878552, 1985229328}), S.LcSm4.key(B.Octets.of_list([1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50, 16]))) == Done{M.CmBlock{1746853684, 3523647070, 2259937615, 1399734854}} : Result<&2, &2, L.LcError, M.CmBlock>}
283
284# RFC 3713, Appendix A: Camellia-128, key = plaintext =
285# 0123456789ABCDEFFEDCBA9876543210, ciphertext 67673138549669730857065648EABE43
286law camellia_rfc3713:
287  {Result.map(&2, &2, L.LcError, C.LcCamelliaKey, M.CmBlock, k => C.LcCamellia.encrypt(k, M.CmBlock{19088743, 2309737967, 4275878552, 1985229328}), C.LcCamellia.key(B.Octets.of_list([1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50, 16]))) == Done{M.CmBlock{1734816056, 1419143539, 139920982, 1223343683}} : Result<&2, &2, L.LcError, M.CmBlock>}
288
289# NESSIE Serpent-128 test vectors, set 3 vector 0: the zero key and the
290# zero block, ciphertext 3620B17AE6A993D09618B8768266BAE9
291law serpent_nessie:
292  {Result.map(&2, &2, L.LcError, P.LcSerpentKey, M.CmBlock, k => P.LcSerpent.encrypt(k, M.CmBlock{0, 0, 0, 0}), P.LcSerpent.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) == Done{M.CmBlock{908112250, 3869873104, 2518202486, 2187770601}} : Result<&2, &2, L.LcError, M.CmBlock>}
293
294# a DES key of 7 bytes is refused
295law des_bad_key_length:
296  {Result.map(&2, &2, L.LcError, D.LcDesKey, Unit, k => Unit{}, D.LcDes.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{7n}} : Result<&2, &2, L.LcError, Unit>}
297
298# a TDEA key bundle of 8 bytes is refused (keying option 3 is not allowed)
299law tdes_bad_key_length:
300  {Result.map(&2, &2, L.LcError, T.LcTdesKey, Unit, k => Unit{}, T.LcTdes.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{8n}} : Result<&2, &2, L.LcError, Unit>}
301
302# a Camellia key of 20 bytes is refused
303law camellia_bad_key_length:
304  {Result.map(&2, &2, L.LcError, C.LcCamelliaKey, Unit, k => Unit{}, C.LcCamellia.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{20n}} : Result<&2, &2, L.LcError, Unit>}
305
306# a Serpent key longer than 256 bits is refused
307law serpent_bad_key_length:
308  {Result.map(&2, &2, L.LcError, P.LcSerpentKey, Unit, k => Unit{}, P.LcSerpent.key(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, 0]))) == Fail{L.LcBadKeyLength{33n}} : Result<&2, &2, L.LcError, Unit>}
309
310# RFC 5794, Appendix A.1: ARIA-128, key 000102030405060708090A0B0C0D0E0F,
311# plaintext 00112233445566778899AABBCCDDEEFF, ciphertext
312# D718FBD6AB644C739DA95F3BE6451778
313law aria_rfc5794:
314  {Result.map(&2, &2, L.LcError, A.LcAriaKey, M.CmBlock, k => A.LcAria.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703}), A.LcAria.key(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]))) == Done{M.CmBlock{3608738774, 2875477107, 2645122875, 3863287672}} : Result<&2, &2, L.LcError, M.CmBlock>}
315
316# RFC 2144, Appendix B.1: CAST-128 with the 128-bit key
317# 0123456712345678234567893456789A, plaintext 0123456789ABCDEF, ciphertext
318# 238B4FE5847E44B2
319law cast5_rfc2144:
320  {Result.map(&2, &2, L.LcError, C5.LcCast5Key, L.LcBlock64, k => C5.LcCast5.encrypt(k, L.LcBlock64{19088743, 2309737967}), C5.LcCast5.key(B.Octets.of_list([1, 35, 69, 103, 18, 52, 86, 120, 35, 69, 103, 137, 52, 86, 120, 154]))) == Done{L.LcBlock64{596332517, 2222867634}} : Result<&2, &2, L.LcError, L.LcBlock64>}
321
322# the FCrypt specification's second vector: key 114477AADD003366,
323# plaintext 123456789ABCDEF0, ciphertext D8ED787477EC0680
324law fcrypt_spec:
325  {Result.map(&2, &2, L.LcError, FC.LcFcryptKey, L.LcBlock64, k => FC.LcFcrypt.encrypt(k, L.LcBlock64{305419896, 2596069104}), FC.LcFcrypt.key(B.Octets.of_list([17, 68, 119, 170, 221, 0, 51, 102]))) == Done{L.LcBlock64{3639441524, 2011956864}} : Result<&2, &2, L.LcError, L.LcBlock64>}
326
327# an ARIA key of 20 bytes is refused
328law aria_bad_key_length:
329  {Result.map(&2, &2, L.LcError, A.LcAriaKey, Unit, k => Unit{}, A.LcAria.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{20n}} : Result<&2, &2, L.LcError, Unit>}
330
331# a CAST-256 key of 18 bytes is refused
332law cast6_bad_key_length:
333  {Result.map(&2, &2, L.LcError, C6.LcCast6Key, Unit, k => Unit{}, C6.LcCast6.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{18n}} : Result<&2, &2, L.LcError, Unit>}
334
335# a Blowfish key of 3 bytes is refused (32 bits at least)
336law blowfish_bad_key_length:
337  {Result.map(&2, &2, L.LcError, BF.LcBlowfishKey, Unit, k => Unit{}, BF.LcBlowfish.key(B.Octets.of_list([0, 0, 0]))) == Fail{L.LcBadKeyLength{3n}} : Result<&2, &2, L.LcError, Unit>}
338
339# a CAST-128 key of 4 bytes is refused (40 bits at least)
340law cast5_bad_key_length:
341  {Result.map(&2, &2, L.LcError, C5.LcCast5Key, Unit, k => Unit{}, C5.LcCast5.key(B.Octets.of_list([0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{4n}} : Result<&2, &2, L.LcError, Unit>}
342
343# a TEA key of 15 bytes is refused
344law tea_bad_key_length:
345  {Result.map(&2, &2, L.LcError, TE.LcTeaKey, Unit, k => Unit{}, TE.LcTea.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{15n}} : Result<&2, &2, L.LcError, Unit>}
346
347# an XTEA key of 17 bytes is refused
348law xtea_bad_key_length:
349  {Result.map(&2, &2, L.LcError, XT.LcXteaKey, Unit, k => Unit{}, XT.LcXtea.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{17n}} : Result<&2, &2, L.LcError, Unit>}
350
351# an FCrypt key of 7 bytes is refused
352law fcrypt_bad_key_length:
353  {Result.map(&2, &2, L.LcError, FC.LcFcryptKey, Unit, k => Unit{}, FC.LcFcrypt.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{7n}} : Result<&2, &2, L.LcError, Unit>}
354
355# an empty RC4 key is refused
356law rc4_empty_key:
357  {R.LcRc4.crypt(B.Octets.empty(), B.Octets.zeros(4n)) == Fail{L.LcBadKeyLength{0n}} : Result<&2, &2, L.LcError, B.Octets>}
358
359# the 64-bit modes refuse a message that is not whole blocks
360law modes64_not_whole_blocks:
361  {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, Unit, bs => Unit{}, X.Lc64.blocks_of(B.Octets.zeros(12n))) == Fail{L.LcNotBlockMultiple{12n}} : Result<&2, &2, L.LcError, Unit>}
362
363# END GENERATED: vectors