bend-collections-laws-crypto
Releases (1)
-
1.0.0.0 indexed
Definitions (8,881)
proofs/crypto/aead/chacha20poly1305.bend
- law poly_key_eq
- law mac_data_eq
- law tag_eq
- def iseal
- law seal_eq
- law open_tag_eq
- law open_split_eq
- law open_len_eq
- def ospl
- law open_eq
- law xkey_eq
- law xnonce_eq
- law xseal_eq
- law xopen_eq
- law length_append
- law prefix_append
- law suffix_append
- law add16_not_lta + 16 is not below 16, and (a + 16) - 16 == a.
- law add16_sub
- law open_appendOpening ct || t with a 16-byte t checks t against the tag of ct.
- def olen
- def osplit_at
- law roundtripOpening what was sealed gives the plaintext back (for every key, nonce, aad and plaintext list).
- law open_tag_false
- law forgeryOpening ciphertext || t fails for every 16-byte t that is not the tag of the ciphertext (under the key, nonce and aad given).
- law iforgeryThe implementation's tag is the specification's, so a t other than the implementation's tag is rejected by the implementation.
- law iroundtrip
proofs/crypto/aead/laws.bend
- def expected_tagThe tag the specification computes over ciphertext ct: decrypt accepts ct || t exactly for this t.
- def decrypt_sealeddecrypt applied to what encrypt returned (None stays None).
- law chacha20poly1305.seal
- law chacha20poly1305.open
- law xchacha20poly1305.seal
- law xchacha20poly1305.open
- law aes128gcm.seal
- law aes128gcm.open
- law aes256gcm.seal
- law aes256gcm.open
- law chacha20poly1305.encryptThe per-algorithm checked ChaCha20-Poly1305 API agrees with the facade.
- law chacha20poly1305.decrypt
- law xchacha20poly1305.encrypt
- law xchacha20poly1305.decrypt
- law encrypt.valid
- law encrypt.invalid
- law decrypt.valid
- law decrypt.invalid
- law roundtripdecrypt(encrypt(x)) == Some(x).
- law forgeryciphertext || t is rejected for every 16-byte t other than the tag of the ciphertext under this key, nonce and aad.
- law seal_layoutWhat encrypt returns is a ciphertext followed by its expected tag.
- law decrypt_soundDecryption is sound: whatever decrypt accepts is exactly what encrypt produces for the returned plaintext (so every accepted input is the honest ciphertext of its plaintext under this key, nonce and aad).
proofs/crypto/aead/proof.bend
- law when_same
- law when_open_same
- law valid_true
- law encrypt_valid
- law decrypt_valid
- def open_sealeddecrypt after encrypt is open after seal (on valid lengths).
- law ds_open
- law os128
- law os256
- law open_seal
- law open_forged
- def sapp
- law layout_cp
- law layout_x
- def gct
- def smaybe
- law open_sound
proofs/crypto/aead/sound.bend
- law none_some
- law some_inj
- law prefix_suffix
- law take_drop
- def csa
- law c_tag
- law c_len
- law chacha_soundWhatever opens to p is the sealing of p.
- def gsa
- law g_tag
- law g_len
- law gcm_sound
proofs/crypto/aead/subtle_eq.bend
- law step
- law fold
- law equal_sound
- law equal_refl
- law eq_value