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). 14 import Base 15 import bend-osdev-bytes@0.1.0.0/bytes.bend as B 16 import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M 17 import ./legacy_ciphers.bend as L 18 import ./des.bend as D 19 import ./tdes.bend as T 20 import ./sm4.bend as S 21 import ./camellia.bend as C 22 import ./serpent.bend as P 23 import ./twofish.bend as F 24 import ./rc4.bend as R 25 import ./modes64.bend as X 26 import ./aria.bend as A 27 import ./cast6.bend as C6 28 import ./blowfish.bend as BF 29 import ./cast5.bend as C5 30 import ./tea.bend as TE 31 import ./xtea.bend as XT 32 import ./fcrypt.bend as FC 33 34 # DES (FIPS 46-3) 35 36 law 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 41 law 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 48 law 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 53 law 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 60 law 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 65 law 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 72 law 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 77 law 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 84 law 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 89 law 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 96 law 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 101 law 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 108 law 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 113 law 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 120 law 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 125 law 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 132 law 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 137 law 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 144 law 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 149 law 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 156 law 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 161 law 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 168 law 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 173 law 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 180 law 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 185 law 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 194 law 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 202 law 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 208 law 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 216 law 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 220 law 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 228 law 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 233 law 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 239 law 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 244 law 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 250 law 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 256 law 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 262 law 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 267 law 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 281 law 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 286 law 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 291 law 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 295 law 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) 299 law 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 303 law 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 307 law 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 313 law 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 319 law 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 324 law 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 328 law 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 332 law 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) 336 law 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) 340 law 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 344 law 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 348 law 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 352 law 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 356 law 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 360 law 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