bend-osdev-legacy-ciphers Releases (1): 0.1.0.0 0x7d16ec09f99b830428c8e2852af315f6 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-legacy-ciphers@0.1.0.0 Definitions (970, 1 to 100 shown): LAWS.des_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=des_round_trip) law des_round_trip: for k: D.LcDesKey for +b: L.LcBlock64 {D.LcDes.decrypt(k, D.LcDes.encrypt(k, b)) == b : L.LcBlock64} LAWS.des_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=des_round_trip_dual) law des_round_trip_dual: for k: D.LcDesKey for +b: L.LcBlock64 {D.LcDes.encrypt(k, D.LcDes.decrypt(k, b)) == b : L.LcBlock64} LAWS.tdes_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_round_trip) law tdes_round_trip: for k: T.LcTdesKey for +b: L.LcBlock64 {T.LcTdes.decrypt(k, T.LcTdes.encrypt(k, b)) == b : L.LcBlock64} LAWS.tdes_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_round_trip_dual) law tdes_round_trip_dual: for k: T.LcTdesKey for +b: L.LcBlock64 {T.LcTdes.encrypt(k, T.LcTdes.decrypt(k, b)) == b : L.LcBlock64} LAWS.sm4_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=sm4_round_trip) law sm4_round_trip: for k: S.LcSm4Key for +b: M.CmBlock {S.LcSm4.decrypt(k, S.LcSm4.encrypt(k, b)) == b : M.CmBlock} LAWS.sm4_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=sm4_round_trip_dual) law sm4_round_trip_dual: for k: S.LcSm4Key for +b: M.CmBlock {S.LcSm4.encrypt(k, S.LcSm4.decrypt(k, b)) == b : M.CmBlock} LAWS.camellia_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=camellia_round_trip) law camellia_round_trip: for k: C.LcCamelliaKey for +b: M.CmBlock {C.LcCamellia.decrypt(k, C.LcCamellia.encrypt(k, b)) == b : M.CmBlock} LAWS.camellia_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=camellia_round_trip_dual) law camellia_round_trip_dual: for k: C.LcCamelliaKey for +b: M.CmBlock {C.LcCamellia.encrypt(k, C.LcCamellia.decrypt(k, b)) == b : M.CmBlock} LAWS.serpent_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=serpent_round_trip) law serpent_round_trip: for k: P.LcSerpentKey for +b: M.CmBlock {P.LcSerpent.decrypt(k, P.LcSerpent.encrypt(k, b)) == b : M.CmBlock} LAWS.serpent_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=serpent_round_trip_dual) law serpent_round_trip_dual: for k: P.LcSerpentKey for +b: M.CmBlock {P.LcSerpent.encrypt(k, P.LcSerpent.decrypt(k, b)) == b : M.CmBlock} LAWS.twofish_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=twofish_round_trip) law twofish_round_trip: for k: F.LcTwofishKey for +b: M.CmBlock {F.LcTwofish.decrypt(k, F.LcTwofish.encrypt(k, b)) == b : M.CmBlock} LAWS.twofish_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=twofish_round_trip_dual) law twofish_round_trip_dual: for k: F.LcTwofishKey for +b: M.CmBlock {F.LcTwofish.encrypt(k, F.LcTwofish.decrypt(k, b)) == b : M.CmBlock} LAWS.aria_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=aria_round_trip) law aria_round_trip: for k: A.LcAriaKey for +b: M.CmBlock {A.LcAria.decrypt(k, A.LcAria.encrypt(k, b)) == b : M.CmBlock} LAWS.aria_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=aria_round_trip_dual) law aria_round_trip_dual: for k: A.LcAriaKey for +b: M.CmBlock {A.LcAria.encrypt(k, A.LcAria.decrypt(k, b)) == b : M.CmBlock} LAWS.cast6_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=cast6_round_trip) law cast6_round_trip: for k: C6.LcCast6Key for +b: M.CmBlock {C6.LcCast6.decrypt(k, C6.LcCast6.encrypt(k, b)) == b : M.CmBlock} LAWS.cast6_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=cast6_round_trip_dual) law cast6_round_trip_dual: for k: C6.LcCast6Key for +b: M.CmBlock {C6.LcCast6.encrypt(k, C6.LcCast6.decrypt(k, b)) == b : M.CmBlock} LAWS.blowfish_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=blowfish_round_trip) law blowfish_round_trip: for k: BF.LcBlowfishKey for +b: L.LcBlock64 {BF.LcBlowfish.decrypt(k, BF.LcBlowfish.encrypt(k, b)) == b : L.LcBlock64} LAWS.blowfish_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=blowfish_round_trip_dual) law blowfish_round_trip_dual: for k: BF.LcBlowfishKey for +b: L.LcBlock64 {BF.LcBlowfish.encrypt(k, BF.LcBlowfish.decrypt(k, b)) == b : L.LcBlock64} LAWS.cast5_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=cast5_round_trip) law cast5_round_trip: for k: C5.LcCast5Key for +b: L.LcBlock64 {C5.LcCast5.decrypt(k, C5.LcCast5.encrypt(k, b)) == b : L.LcBlock64} LAWS.cast5_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=cast5_round_trip_dual) law cast5_round_trip_dual: for k: C5.LcCast5Key for +b: L.LcBlock64 {C5.LcCast5.encrypt(k, C5.LcCast5.decrypt(k, b)) == b : L.LcBlock64} LAWS.tea_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tea_round_trip) law tea_round_trip: for k: TE.LcTeaKey for +b: L.LcBlock64 {TE.LcTea.decrypt(k, TE.LcTea.encrypt(k, b)) == b : L.LcBlock64} LAWS.tea_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tea_round_trip_dual) law tea_round_trip_dual: for k: TE.LcTeaKey for +b: L.LcBlock64 {TE.LcTea.encrypt(k, TE.LcTea.decrypt(k, b)) == b : L.LcBlock64} LAWS.xtea_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=xtea_round_trip) law xtea_round_trip: for k: XT.LcXteaKey for +b: L.LcBlock64 {XT.LcXtea.decrypt(k, XT.LcXtea.encrypt(k, b)) == b : L.LcBlock64} LAWS.xtea_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=xtea_round_trip_dual) law xtea_round_trip_dual: for k: XT.LcXteaKey for +b: L.LcBlock64 {XT.LcXtea.encrypt(k, XT.LcXtea.decrypt(k, b)) == b : L.LcBlock64} LAWS.fcrypt_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=fcrypt_round_trip) law fcrypt_round_trip: for k: FC.LcFcryptKey for +b: L.LcBlock64 {FC.LcFcrypt.decrypt(k, FC.LcFcrypt.encrypt(k, b)) == b : L.LcBlock64} LAWS.fcrypt_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=fcrypt_round_trip_dual) law fcrypt_round_trip_dual: for k: FC.LcFcryptKey for +b: L.LcBlock64 {FC.LcFcrypt.encrypt(k, FC.LcFcrypt.decrypt(k, b)) == b : L.LcBlock64} LAWS.rc4_involution (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=rc4_involution) # the cipher is its own inverse: from one state, applied twice, the data # comes back law rc4_involution: for +st: R.LcRc4State for +m: B.Octets {R.LcRc4.out_data(R.LcRc4.update(st, R.LcRc4.out_data(R.LcRc4.update(st, m)))) == m : B.Octets} LAWS.rc4_streaming_data (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=rc4_streaming_data) # data in pieces: the output of a ++ b is the output of a, then the output # of b from the state after a; and the state after a ++ b is the state # after a, then b law rc4_streaming_data: for +st: R.LcRc4State for +a: B.Octets for +b: B.Octets {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} LAWS.rc4_streaming_state (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=rc4_streaming_state) law rc4_streaming_state: for +st: R.LcRc4State for +a: B.Octets for +b: B.Octets {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} LAWS.block64_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=block64_octets_round_trip) # 64-bit blocks as bytes: a block read back from its 8 bytes is itself, and # a list of blocks read back from its bytes is itself law block64_octets_round_trip: for +b: L.LcBlock64 {L.LcBlock64.of_octets(L.LcBlock64.to_octets(b)) == Some{b} : Maybe<&2, L.LcBlock64>} LAWS.blocks64_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=blocks64_octets_round_trip) law blocks64_octets_round_trip: for +bs: List<&2, L.LcBlock64> {X.Lc64.blocks_of(X.Lc64.octets_of(bs)) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>} LAWS.des_ecb_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=des_ecb_round_trip) law des_ecb_round_trip: for +k: D.LcDesKey for +bs: List<&2, L.LcBlock64> {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>} LAWS.des_cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=des_cbc_round_trip) law des_cbc_round_trip: for +k: D.LcDesKey for +iv: L.LcBlock64 for +bs: List<&2, L.LcBlock64> {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>} LAWS.tdes_ecb_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_ecb_round_trip) law tdes_ecb_round_trip: for +k: T.LcTdesKey for +bs: List<&2, L.LcBlock64> {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>} LAWS.tdes_cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_cbc_round_trip) law tdes_cbc_round_trip: for +k: T.LcTdesKey for +iv: L.LcBlock64 for +bs: List<&2, L.LcBlock64> {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>} LAWS.des_cbc_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=des_cbc_octets_round_trip) law des_cbc_octets_round_trip: for +k: D.LcDesKey for +iv: L.LcBlock64 for +bs: List<&2, L.LcBlock64> {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>} LAWS.tdes_cbc_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_cbc_octets_round_trip) law tdes_cbc_octets_round_trip: for +k: T.LcTdesKey for +iv: L.LcBlock64 for +bs: List<&2, L.LcBlock64> {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>} LAWS.des_ecb_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=des_ecb_octets_round_trip) law des_ecb_octets_round_trip: for +k: D.LcDesKey for +bs: List<&2, L.LcBlock64> {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>} LAWS.tdes_ecb_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_ecb_octets_round_trip) law tdes_ecb_octets_round_trip: for +k: T.LcTdesKey for +bs: List<&2, L.LcBlock64> {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>} LAWS.sm4_gbt32907 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=sm4_gbt32907) # BEGIN GENERATED by gen/vectors.py: vectors # GB/T 32907-2016, Appendix A, example 1: key = plaintext = # 0123456789ABCDEFFEDCBA9876543210, ciphertext 681EDF34D206965E86B3E94F536E4246 law sm4_gbt32907: {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>} LAWS.camellia_rfc3713 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=camellia_rfc3713) # RFC 3713, Appendix A: Camellia-128, key = plaintext = # 0123456789ABCDEFFEDCBA9876543210, ciphertext 67673138549669730857065648EABE43 law camellia_rfc3713: {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>} LAWS.serpent_nessie (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=serpent_nessie) # NESSIE Serpent-128 test vectors, set 3 vector 0: the zero key and the # zero block, ciphertext 3620B17AE6A993D09618B8768266BAE9 law serpent_nessie: {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>} LAWS.des_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=des_bad_key_length) # a DES key of 7 bytes is refused law des_bad_key_length: {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>} LAWS.tdes_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_bad_key_length) # a TDEA key bundle of 8 bytes is refused (keying option 3 is not allowed) law tdes_bad_key_length: {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>} LAWS.camellia_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=camellia_bad_key_length) # a Camellia key of 20 bytes is refused law camellia_bad_key_length: {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>} LAWS.serpent_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=serpent_bad_key_length) # a Serpent key longer than 256 bits is refused law serpent_bad_key_length: {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>} LAWS.aria_rfc5794 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=aria_rfc5794) # RFC 5794, Appendix A.1: ARIA-128, key 000102030405060708090A0B0C0D0E0F, # plaintext 00112233445566778899AABBCCDDEEFF, ciphertext # D718FBD6AB644C739DA95F3BE6451778 law aria_rfc5794: {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>} LAWS.cast5_rfc2144 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=cast5_rfc2144) # RFC 2144, Appendix B.1: CAST-128 with the 128-bit key # 0123456712345678234567893456789A, plaintext 0123456789ABCDEF, ciphertext # 238B4FE5847E44B2 law cast5_rfc2144: {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>} LAWS.fcrypt_spec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=fcrypt_spec) # the FCrypt specification's second vector: key 114477AADD003366, # plaintext 123456789ABCDEF0, ciphertext D8ED787477EC0680 law fcrypt_spec: {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>} LAWS.aria_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=aria_bad_key_length) # an ARIA key of 20 bytes is refused law aria_bad_key_length: {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>} LAWS.cast6_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=cast6_bad_key_length) # a CAST-256 key of 18 bytes is refused law cast6_bad_key_length: {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>} LAWS.blowfish_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=blowfish_bad_key_length) # a Blowfish key of 3 bytes is refused (32 bits at least) law blowfish_bad_key_length: {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>} LAWS.cast5_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=cast5_bad_key_length) # a CAST-128 key of 4 bytes is refused (40 bits at least) law cast5_bad_key_length: {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>} LAWS.tea_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tea_bad_key_length) # a TEA key of 15 bytes is refused law tea_bad_key_length: {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>} LAWS.xtea_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=xtea_bad_key_length) # an XTEA key of 17 bytes is refused law xtea_bad_key_length: {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>} LAWS.fcrypt_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=fcrypt_bad_key_length) # an FCrypt key of 7 bytes is refused law fcrypt_bad_key_length: {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>} LAWS.rc4_empty_key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=rc4_empty_key) # an empty RC4 key is refused law rc4_empty_key: {R.LcRc4.crypt(B.Octets.empty(), B.Octets.zeros(4n)) == Fail{L.LcBadKeyLength{0n}} : Result<&2, &2, L.LcError, B.Octets>} LAWS.modes64_not_whole_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=modes64_not_whole_blocks) # the 64-bit modes refuse a message that is not whole blocks law modes64_not_whole_blocks: {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>} PROOF.bool_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=bool_xx) def bool_xx(a: Bool, b: Bool) -> {a == Bool.xor(Bool.xor(a, b), b) : Bool}: PROOF.word_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=word_xx) def word_xx(n: Nat, a: Word(n), b: Word(n)) -> {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}: PROOF.u32_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=u32_xx) def u32_xx(a: U32, b: U32) -> {a == U32.xor(U32.xor(a, b), b) : U32}: PROOF.block_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=block_xx) def block_xx(s: M.CmBlock, k: M.CmBlock) -> {s == M.CmBlock.xor(M.CmBlock.xor(s, k), k) : M.CmBlock}: PROOF.rot_1_31 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_1_31) def rot_1_31(x: U32) -> {x == L.lc.rotl1.bits(L.lc.rotl31.bits(x)) : U32}: PROOF.rot_31_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_31_1) def rot_31_1(x: U32) -> {x == L.lc.rotl31.bits(L.lc.rotl1.bits(x)) : U32}: PROOF.rot_19_13 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_19_13) def rot_19_13(x: U32) -> {x == L.lc.rotl19.bits(L.lc.rotl13.bits(x)) : U32}: PROOF.rot_13_19 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_13_19) def rot_13_19(x: U32) -> {x == L.lc.rotl13.bits(L.lc.rotl19.bits(x)) : U32}: PROOF.rot_29_3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_29_3) def rot_29_3(x: U32) -> {x == L.lc.rotl29.bits(L.lc.rotl3.bits(x)) : U32}: PROOF.rot_3_29 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_3_29) def rot_3_29(x: U32) -> {x == L.lc.rotl3.bits(L.lc.rotl29.bits(x)) : U32}: PROOF.rot_25_7 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_25_7) def rot_25_7(x: U32) -> {x == L.lc.rotl25.bits(L.lc.rotl7.bits(x)) : U32}: PROOF.rot_7_25 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_7_25) def rot_7_25(x: U32) -> {x == L.lc.rotl7.bits(L.lc.rotl25.bits(x)) : U32}: PROOF.rot_27_5 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_27_5) def rot_27_5(x: U32) -> {x == L.lc.rotl27.bits(L.lc.rotl5.bits(x)) : U32}: PROOF.rot_5_27 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_5_27) def rot_5_27(x: U32) -> {x == L.lc.rotl5.bits(L.lc.rotl27.bits(x)) : U32}: PROOF.rot_10_22 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_10_22) def rot_10_22(x: U32) -> {x == L.lc.rotl10.bits(L.lc.rotl22.bits(x)) : U32}: PROOF.rot_22_10 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rot_22_10) def rot_22_10(x: U32) -> {x == L.lc.rotl22.bits(L.lc.rotl10.bits(x)) : U32}: PROOF.bswap2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=bswap2) def bswap2(x: U32) -> {x == L.lc.bswap.bits(L.lc.bswap.bits(x)) : U32}: PROOF.des_ip_fp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_ip_fp) # DES's IP and IP^-1 undo each other, computed on the block's 64 bits def des_ip_fp(h: D.LcDesHalves) -> {h == D.des.ip(D.des.fp(h)) : D.LcDesHalves}: PROOF.des_fp_ip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_fp_ip) def des_fp_ip(b: L.LcBlock64) -> {b == D.des.fp(D.des.ip(b)) : L.LcBlock64}: PROOF.byte_xor_byte (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=byte_xor_byte) # the low byte of a XOR depends only on the low bytes def byte_xor_byte(z: U32, k: U32) -> {B.byte(U32.xor(z, k)) == B.byte(U32.xor(B.byte(z), k)) : U32}: PROOF.blk_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=blk_bytes) # a 64-bit block's bytes, masked and read back def blk_bytes(b: L.LcBlock64) -> {L.lc.block_of(B.mask(L.lc.block_bytes(b, Nil{}))) == Some{b} : Maybe<&2, L.LcBlock64>}: PROOF.blk8 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=blk8) def blk8(hi: U32, lo: U32) -> {L.LcBlock64{hi, lo} == L.lc.block8(B.byte(L.lc.b0.bits(hi)), B.byte(L.lc.b1.bits(hi)), B.byte(L.lc.b2.bits(hi)), B.byte(L.lc.b3.bits(hi)), B.byte(L.lc.b0.bits(lo)), B.byte(L.lc.b1.bits(lo)), B.byte(L.lc.b2.bits(lo)), B.byte(L.lc.b3.bits(lo))) : L.LcBlock64}: PROOF.des_swap2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_swap2) def des_swap2(h: D.LcDesHalves) -> {h == D.des.swap(D.des.swap(h)) : D.LcDesHalves}: PROOF.des_unstep_step (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_unstep_step) def des_unstep_step(+k: D.LcDesRk, h: D.LcDesHalves) -> {h == D.des.unstep(k, D.des.step(k, h)) : D.LcDesHalves}: PROOF.des_step_unstep (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_step_unstep) def des_step_unstep(+k: D.LcDesRk, h: D.LcDesHalves) -> {h == D.des.step(k, D.des.unstep(k, h)) : D.LcDesHalves}: PROOF.des_unrounds_rounds (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_unrounds_rounds) def des_unrounds_rounds(ks: List<&2, D.LcDesRk>, +h: D.LcDesHalves) -> {h == D.des.unrounds(ks, D.des.rounds(ks, h)) : D.LcDesHalves}: PROOF.des_rounds_unrounds (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_rounds_unrounds) def des_rounds_unrounds(ks: List<&2, D.LcDesRk>, +h: D.LcDesHalves) -> {h == D.des.rounds(ks, D.des.unrounds(ks, h)) : D.LcDesHalves}: PROOF.des_rt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_rt) def des_rt(k: D.LcDesKey, +b: L.LcBlock64) -> {b == D.LcDes.decrypt(k, D.LcDes.encrypt(k, b)) : L.LcBlock64}: PROOF.des_rt_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=des_rt_dual) def des_rt_dual(k: D.LcDesKey, +b: L.LcBlock64) -> {b == D.LcDes.encrypt(k, D.LcDes.decrypt(k, b)) : L.LcBlock64}: PROOF.sm4_unstep_step (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sm4_unstep_step) def sm4_unstep_step(+tab: L.LcTab, +rk: U32, s: M.CmBlock) -> {s == S.sm4.unstep(tab, rk, S.sm4.step(tab, rk, s)) : M.CmBlock}: PROOF.sm4_step_unstep (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sm4_step_unstep) def sm4_step_unstep(+tab: L.LcTab, +rk: U32, s: M.CmBlock) -> {s == S.sm4.step(tab, rk, S.sm4.unstep(tab, rk, s)) : M.CmBlock}: PROOF.sm4_unrounds_rounds (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sm4_unrounds_rounds) def sm4_unrounds_rounds(+tab: L.LcTab, ks: List<&2, U32>, +s: M.CmBlock) -> {s == S.sm4.unrounds(tab, ks, S.sm4.rounds(tab, ks, s)) : M.CmBlock}: PROOF.sm4_rounds_unrounds (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sm4_rounds_unrounds) def sm4_rounds_unrounds(+tab: L.LcTab, ks: List<&2, U32>, +s: M.CmBlock) -> {s == S.sm4.rounds(tab, ks, S.sm4.unrounds(tab, ks, s)) : M.CmBlock}: PROOF.sm4_rev2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sm4_rev2) def sm4_rev2(s: M.CmBlock) -> {s == S.sm4.rev(S.sm4.rev(s)) : M.CmBlock}: PROOF.cam_fl_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_fl_inv) def cam_fl_inv(x: L.LcBlock64, k: L.LcBlock64) -> {x == C.cam.flinv(C.cam.fl(x, k), k) : L.LcBlock64}: PROOF.cam_flinv_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_flinv_inv) def cam_flinv_inv(y: L.LcBlock64, k: L.LcBlock64) -> {y == C.cam.fl(C.cam.flinv(y, k), k) : L.LcBlock64}: PROOF.cam_white (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_white) def cam_white(a: L.LcBlock64, b: L.LcBlock64, +s: M.CmBlock) -> {s == C.cam.white(a, b, C.cam.white(a, b, s)) : M.CmBlock}: PROOF.cam_f1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_f1) def cam_f1(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF1{t, k}, C.cam.op(C.LcCamF1{t, k}, s)) : M.CmBlock}: PROOF.cam_f1d (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_f1d) def cam_f1d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF1{t, k}, C.cam.unop(C.LcCamF1{t, k}, s)) : M.CmBlock}: PROOF.cam_f2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_f2) def cam_f2(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF2{t, k}, C.cam.op(C.LcCamF2{t, k}, s)) : M.CmBlock}: PROOF.cam_f2d (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_f2d) def cam_f2d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF2{t, k}, C.cam.unop(C.LcCamF2{t, k}, s)) : M.CmBlock}: PROOF.cam_fl_step (https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=cam_fl_step) def cam_fl_step(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamFl{a, b}, C.cam.op(C.LcCamFl{a, b}, s)) : M.CmBlock}: More: https://jend.leeeet.dev/packages/bend-osdev-legacy-ciphers.txt?definitions_offset=100