bend-osdev-crypto

Releases (1)

• 0.1.0.0 indexed

Definitions (678)

LAWS.bend

• law hmac_streebog256_streamingHMAC over Streebog-256 (hashes): the state after a ++ b is the state after a, then b
• law hmac_streebog256_splitHMAC over Streebog-256 (hashes): the tag in pieces is the tag in one call, for every split
• law streebog512_hash_streamingStreebog-512 (hashes): update over a ++ b is update over a, then b, for every state
• law streebog512_hash_splitStreebog-512 (hashes): streaming equals one-shot, for every split
• law streebog512_hash_split3Streebog-512 (hashes): and for every split into three
• law streebog512_hash_lengthStreebog-512 (hashes): final(s) has 64 bytes, for every state
• law hmac_streebog512_streamingHMAC over Streebog-512 (hashes): the state after a ++ b is the state after a, then b
• law hmac_streebog512_splitHMAC over Streebog-512 (hashes): the tag in pieces is the tag in one call, for every split

PROOF.bend

• def byte_xor_byteBEGIN GENERATED by gen/proof.py: bits the low byte of a XOR depends only on the low byte of its first operand
• def be32_lena word's big-endian bytes are four
• def f128_bytesa 128-bit block's 16 bytes, masked and read back
• def bool_xx
• def word_xx
• def u32_xx
• def byte_xx
• def rev2
• def mask_append
• def octets_of_appendOctets.of_list of an append is the append of the Octets (from bytes' laws)
• def ks_go_refthe loop, for every list and state, is the structural output reversed onto what it had
• def xor_update_ref
• def ks_mask_xs
• def ks_xs_xs
• def ks_after_append
• def ks_xs_append
• def cmblock_xx
• def lcblock64_xx
• def ecb_tr
• def ecb_pub
• def cbc_enc_tr
• def cbc_dec_tr
• def cbc_enc_pub
• def cbc_dec_pub
• def pcbc_enc_tr
• def pcbc_dec_tr
• def pcbc_enc_pub
• def pcbc_dec_pub
• def lrw_enc_tr
• def lrw_dec_tr
• def lrw_enc_pub
• def lrw_dec_pub
• def append_nil
• def mask_len
• def octets_len_ofthe length of a list made Octets
• def pbkdf2_out_lenPBKDF2: the output generator gives n bytes, whatever the MAC (induction on n), and its first n bytes are the same whatever comes after
• def pbkdf2_out_prefix
• def pbkdf2_checked_len
• def kb_ctr_len
• def kb_ctr_prefix
• def kb_fb_len
• def kb_fb_prefix
• def kb_key_len
• def kb_checked_len
• def kb_fkey_len
• def kb_fchecked_len
• def ecb_rt.des
• def cbc_rt.des
• def pcbc_rt.des
• def ecb_rt.tdes
• def cbc_rt.tdes
• def pcbc_rt.tdes
• def ecb_rt.sm4
• def cbc_rt.sm4
• def pcbc_rt.sm4
• def lrw_b.sm4
• def lrw_rt.sm4
• def ecb_rt.camellia
• def cbc_rt.camellia
• def pcbc_rt.camellia
• def lrw_b.camellia
• def lrw_rt.camellia
• def ecb_rt.serpent
• def cbc_rt.serpent
• def pcbc_rt.serpent
• def lrw_b.serpent
• def lrw_rt.serpent
• def ecb_rt.twofish
• def cbc_rt.twofish
• def pcbc_rt.twofish
• def lrw_b.twofish
• def lrw_rt.twofish
• def ecb_rt.aria
• def cbc_rt.aria
• def pcbc_rt.aria
• def lrw_b.aria
• def lrw_rt.aria
• def ecb_rt.cast6
• def cbc_rt.cast6
• def pcbc_rt.cast6
• def lrw_b.cast6
• def lrw_rt.cast6
• def ecb_rt.blowfish
• def cbc_rt.blowfish
• def pcbc_rt.blowfish
• def ecb_rt.cast5
• def cbc_rt.cast5
• def pcbc_rt.cast5
• def ecb_rt.tea
• def cbc_rt.tea
• def pcbc_rt.tea
• def ecb_rt.xtea