bend-collections-laws-crypto

Releases (1)

• 1.0.0.0 indexed

Definitions (8,881)

proofs/crypto/aes/gf.bend

• def xor_zero_l
• def xor_zero_r
• def xor_self
• def xor_assoc
• def xor_swap4
• def put_xor
• def shl_xor
• def top_xor
• def top_zero
• def put_zero
• def shl_zero
• def wscale_xor
• def tx_xor
• def tx_zero
• def tx_wscale
• def constant_xor
• def red_add
• def scale_true
• def constant_false_xor
• def red_scale_false
• def red_scale
• def constant_false_l
• def red_shift
• def smsum over the set coefficients a_i of v * x^i (mod m)
• def saAlgorithm 1 of SP 800-38D: Z ^= a_i ?
• def tx_sm
• def red_mul
• def sa_sm
• def wofThe first n coefficients of a list, zero-filled.
• def wof_nil
• def wof_false_nil
• def put_wof
• def shl_wof
• def top_short
• def red_short
• def wof_coefficients
• def coefficients_le
• def red_coefficients
• def mul_saThe product of two residues, reduced, is Algorithm 1 from Z = 0.

proofs/crypto/aes/ghash.bend

• def step_okOne bit of Algorithm 1: Z += c*V, V = V*x.
• def steps_ok
• def steps_append
• def mul_bytes_steps
• def append_nil
• def f_nil
• def absorb_ok(Y xor X) * H for one 16-byte block.
• def ghash_okGHASH over X || 0^v (then more blocks) is the implementation's GHASH over X.
• def ghash_all_okGHASH_H(A || 0^v || C || 0^u || [len(A)]_64 || [len(C)]_64).
• def pack_okThe hash subkey: the implementation packs E_K(0^128) into words.

proofs/crypto/aes/ghash_bits.bend

• def zstep_okZ xor (V and (0 - bit)) is Z + c*V.
• def mulx_w
• def mulx_okV * x: the shift toward x^127 with the reduction by R.
• def mul_byte_steps
• def block_xor_ok
• def or_false
• def u32_ext
• def word_okThe implementation packs four bytes into a big-endian word.
• def pack_int
• def bb_ok
• def int32_ctr
• def str32_ctr

proofs/crypto/aes/ghash_defs.bend

• def RThe field element of an implementation block (its 16 bytes, as SP 800-38D reads them).
• def bitThe U32 the implementation reads for a coefficient c.
• def FAlgorithm 1 continued from an implementation accumulator (Z, V) over the coefficients cs.
• def stepsThe implementation's steps over a list of coefficients.

proofs/crypto/aes/inverse.bend

• law inverse_unit_bits
• law inverse_unit
• law inverse_zero

proofs/crypto/aes/laws.bend

• def block_withOne block with an optional expanded key (the byte API in one call).
• def open128Decrypt what an encryption returned (None stays None).
• def open256
• law Sbox.valueThe constant-time S-box circuit is FIPS 197's S-box (the inverse in GF(2^8), {00} to {00}, then the affine map), on every input.
• law Inverse.unitThe specification's inverse (a^254) is the multiplicative inverse of FIPS 197 section 4.4: a * a^-1 = {01} for every nonzero byte, and {00} goes to {00} (5.1.1); so S.sbox is "inverse, then affine map".
• law Inverse.zero
• law Cipher.valueThe implementation's cipher with its expanded key is FIPS 197's Cipher with KeyExpansion, for every Nk, Nr, key and state.
• law Block.valueThe byte API: a key of 16, 24 or 32 bytes encrypts a 16-byte block with AES under the key's Nk = length/4 and Nr = Nk + 6 (FIPS 197 Figure 4).
• law Block.aes128A 16-, 24-, 32-byte key is AES-128 (Nk = 4, Nr = 10), AES-192 (6, 12), AES-256 (8, 14).
• law Block.aes192
• law Block.aes256
• law Gcm.sealThe implementation's GCM-AE / GCM-AD, for every expanded key, 96-bit nonce, AAD and input.
• law Gcm.open
• law Aead.roundtripAEAD correctness of the specification: opening the sealed message gives it back; C || T with T other than the tag of C is rejected.
• law Aead.forgery
• law Api128.encrypt
• law Api128.decrypt
• law Api128.roundtripdecrypt(encrypt(x)) == Some(x).
• law Api128.forgeryA wrong tag gives None.
• law Api128.bad_keyA key of another length is rejected.
• law Api128.bad_key_open
• law Api128.bad_nonceA nonce other than 12 bytes is rejected.
• law Api128.bad_nonce_open
• law Api256.encrypt
• law Api256.decrypt
• law Api256.roundtripdecrypt(encrypt(x)) == Some(x).
• law Api256.forgeryA wrong tag gives None.
• law Api256.bad_keyA key of another length is rejected.
• law Api256.bad_key_open
• law Api256.bad_nonceA nonce other than 12 bytes is rejected.
• law Api256.bad_nonce_open

proofs/crypto/aes/proof.bend

• def seal_nonce_badA nonce that is not 12 bytes long: None.