bend-collections-laws-crypto

Releases (1)

• 1.0.0.0 indexed

Definitions (8,881)

proofs/crypto/aes/aead.bend

• def cancel12
• def cancel13
• def cancel14
• def cancel15
• def gctr_blockOne whole block of counter mode.
• def gctr_part1
• def gctr_part2
• def gctr_part3
• def gctr_part4
• def gctr_part5
• def gctr_part6
• def gctr_part7
• def gctr_part8
• def gctr_part9
• def gctr_part10
• def gctr_part11
• def gctr_part12
• def gctr_part13
• def gctr_part14
• def gctr_part15
• def gctr_invCounter mode is an involution (the keystream is XORed twice).
• def bb16
• def hbThe GHASH block of the tag, as bytes, and byte i of the tag.
• def tb
• def tag16The tag is a 16-byte list.
• def not_shortSplitting C || T (T of 16 bytes) back into C and T.
• def sub16
• def take_app
• def drop_app
• def open_append
• def equal_refl
• def false_of
• def equal_false
• def roundtripOpening what seal produced gives the plaintext back.
• def forgeryOpening C || T with T other than the tag of C gives None.

proofs/crypto/aes/api.bend

• def valid_of
• def open128Decrypt what an encryption returned (None stays None).
• def open256
• law aes128_encrypt
• law aes128_decrypt
• law aes128_roundtrip
• law aes128_forgery
• law aes256_encrypt
• law aes256_decrypt
• law aes256_roundtrip
• law aes256_forgery
• def no_len
• law aes128_encrypt_l
• law aes128_decrypt_l
• law aes128_roundtrip_l
• law aes128_forgery_t
• law aes128_forgery_l
• law aes256_encrypt_l
• law aes256_decrypt_l
• law aes256_roundtrip_l
• law aes256_forgery_t
• law aes256_forgery_l

proofs/crypto/aes/cipher.bend

• law quad_congCongruence of the record constructors (one rewrite per field, on variables).
• law state_cong
• law sub_word_ok
• law sub_bytes_ok
• law shift_rows_ok
• law xor4_cong
• law mix_column_ok
• law mix_columns_ok
• law xor_word_ok
• law ark_ok
• law round_ok
• law last_round_ok
• law rounds_ok
• law cipher_ok
• law rot_word_ok
• law xpow_ok
• law rcon_ok
• law key_words_ok
• law get_word_ok
• law core_ok
• law next_ok
• law grow_ok
• law expand_ok
• law encrypt_okThe implementation's cipher with its expanded key is FIPS 197's Cipher with KeyExpansion, for every Nk, Nr, key and block.

proofs/crypto/aes/gcm.bend

• def cbThe counter block nonce || [c]_32.
• def nonceThe 96-bit nonce.
• def bytes_of_ok
• def xor_ok
• def keystream_ok
• def inc_ok
• def gctr_okCounter mode from counter c (a whole block per counter; a last partial block uses the leftmost bytes of its keystream block).
• def hash_key_ok
• def tag_okThe tag: GCTR from J0 over GHASH of A, C and their lengths.
• def seal_okGCM-AE: C = GCTR(inc32(J0), P), T = the tag of C.
• def accept_ok
• def open_checked_okGCM-AD with the tag compared by subtle.eq (equal to list equality).
• def open_split_ok
• def open_ok

proofs/crypto/aes/gf.bend

• def bxor_false
• def bxor_comm
• def bxor_assoc
• def bxor_self
• def bswap4