bend-osdev-legacy-ciphers

Releases (1)

• 0.1.0.0 indexed

Definitions (970)

LAWS.bend

• law des_round_trip
• law des_round_trip_dual
• law tdes_round_trip
• law tdes_round_trip_dual
• law sm4_round_trip
• law sm4_round_trip_dual
• law camellia_round_trip
• law camellia_round_trip_dual
• law serpent_round_trip
• law serpent_round_trip_dual
• law twofish_round_trip
• law twofish_round_trip_dual
• law aria_round_trip
• law aria_round_trip_dual
• law cast6_round_trip
• law cast6_round_trip_dual
• law blowfish_round_trip
• law blowfish_round_trip_dual
• law cast5_round_trip
• law cast5_round_trip_dual
• law tea_round_trip
• law tea_round_trip_dual
• law xtea_round_trip
• law xtea_round_trip_dual
• law fcrypt_round_trip
• law fcrypt_round_trip_dual
• law rc4_involutionthe cipher is its own inverse: from one state, applied twice, the data comes back
• law rc4_streaming_datadata 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_state
• law block64_octets_round_trip64-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 blocks64_octets_round_trip
• law des_ecb_round_trip
• law des_cbc_round_trip
• law tdes_ecb_round_trip
• law tdes_cbc_round_trip
• law des_cbc_octets_round_trip
• law tdes_cbc_octets_round_trip
• law des_ecb_octets_round_trip
• law tdes_ecb_octets_round_trip
• law sm4_gbt32907BEGIN GENERATED by gen/vectors.py: vectors GB/T 32907-2016, Appendix A, example 1: key = plaintext = 0123456789ABCDEFFEDCBA9876543210, ciphertext 681EDF34D206965E86B3E94F536E4246
• law camellia_rfc3713RFC 3713, Appendix A: Camellia-128, key = plaintext = 0123456789ABCDEFFEDCBA9876543210, ciphertext 67673138549669730857065648EABE43
• law serpent_nessieNESSIE Serpent-128 test vectors, set 3 vector 0: the zero key and the zero block, ciphertext 3620B17AE6A993D09618B8768266BAE9
• law des_bad_key_lengtha DES key of 7 bytes is refused
• law tdes_bad_key_lengtha TDEA key bundle of 8 bytes is refused (keying option 3 is not allowed)
• law camellia_bad_key_lengtha Camellia key of 20 bytes is refused
• law serpent_bad_key_lengtha Serpent key longer than 256 bits is refused
• law aria_rfc5794RFC 5794, Appendix A.1: ARIA-128, key 000102030405060708090A0B0C0D0E0F, plaintext 00112233445566778899AABBCCDDEEFF, ciphertext D718FBD6AB644C739DA95F3BE6451778
• law cast5_rfc2144RFC 2144, Appendix B.1: CAST-128 with the 128-bit key 0123456712345678234567893456789A, plaintext 0123456789ABCDEF, ciphertext 238B4FE5847E44B2
• law fcrypt_specthe FCrypt specification's second vector: key 114477AADD003366, plaintext 123456789ABCDEF0, ciphertext D8ED787477EC0680
• law aria_bad_key_lengthan ARIA key of 20 bytes is refused
• law cast6_bad_key_lengtha CAST-256 key of 18 bytes is refused
• law blowfish_bad_key_lengtha Blowfish key of 3 bytes is refused (32 bits at least)
• law cast5_bad_key_lengtha CAST-128 key of 4 bytes is refused (40 bits at least)
• law tea_bad_key_lengtha TEA key of 15 bytes is refused
• law xtea_bad_key_lengthan XTEA key of 17 bytes is refused
• law fcrypt_bad_key_lengthan FCrypt key of 7 bytes is refused
• law rc4_empty_keyan empty RC4 key is refused
• law modes64_not_whole_blocksthe 64-bit modes refuse a message that is not whole blocks

PROOF.bend

• def bool_xx
• def word_xx
• def u32_xx
• def block_xx
• def rot_1_31
• def rot_31_1
• def rot_19_13
• def rot_13_19
• def rot_29_3
• def rot_3_29
• def rot_25_7
• def rot_7_25
• def rot_27_5
• def rot_5_27
• def rot_10_22
• def rot_22_10
• def bswap2
• def des_ip_fpDES's IP and IP^-1 undo each other, computed on the block's 64 bits
• def des_fp_ip
• def byte_xor_bytethe low byte of a XOR depends only on the low bytes
• def blk_bytesa 64-bit block's bytes, masked and read back
• def blk8
• def des_swap2
• def des_unstep_step
• def des_step_unstep
• def des_unrounds_rounds
• def des_rounds_unrounds
• def des_rt
• def des_rt_dual
• def sm4_unstep_step
• def sm4_step_unstep
• def sm4_unrounds_rounds
• def sm4_rounds_unrounds
• def sm4_rev2
• def cam_fl_inv
• def cam_flinv_inv
• def cam_white
• def cam_f1
• def cam_f1d
• def cam_f2
• def cam_f2d
• def cam_fl_step