bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

def key_words
def get_word
def schedule_core
def next_wordhistory is the words so far, the newest first.
def grow
def round_keysFour consecutive words make a round key.
def expand
def encrypt
type ScheduleAn expanded key: the number of rounds and the round keys.
def valid_lengthFIPS 197 Figure 4: a key of 16, 24 or 32 bytes; Nk = its length in words, Nr = Nk + 6.
def schedule_if
def expand_keyA 16-, 24- or 32-byte key (AES-128, AES-192, AES-256); None otherwise.
def encrypt_state
def state_of
def bytes_of
def encrypt_bytes
def encrypt_blockEncrypts one 16-byte block; None for another length.
def hex_digit_if
def hex_digit
def hexLowercase hexadecimal of a byte list.

type Block
type Acc
def zero
def mulxV * x: the block shifted one bit toward x^127, x^128 = R.
def add_maskedZ xor (V and (0 - bit)), bit being 0 or 1.
def step
def mul_byteThe eight bits of a byte, the most significant first.
def mul_bytes
def acc_z
def unpackThe 16 bytes of a block, and the block of 16 bytes (big-endian words).
def word
def packAn AES state as a block: its columns are the words.
def xor_bytes
def absorb(Y xor X) * H for a 16-byte X.
def zeros
def ghashGHASH_H over the bytes, a last partial block padded with zero bytes.
def octets[n]_(8*width), most significant byte first.
def lengths[len(A)]_64 || [len(C)]_64, in bits.
def counterThe counter block: the 96-bit nonce (three words) and a 32-bit counter.
def keystream
def gctr
def hash_key
def tagThe tag of ciphertext c: GHASH over A || 0^v || C || 0^u || lengths, encrypted with the counter block J0 = nonce || 1.
def seal_coreC || T; the counter of the first data block is 2 (inc32(J0)).
def accept
def open_checkedThe plaintext when t is the tag of c; None otherwise (compared in constant time).
def open_split
def open_core
def seal_nonce
def open_nonce
def seal_key
def open_key
def schedule_if
def schedule_ofThe expanded key when the key has the given length.

def sbox_wordThe AES S-box and the GF(2^8) doublings MixColumns needs, computed with U32 bit operations only: no table and no branch reads a secret byte.
def sboxThe S-box.
def xtime_word{02} * x in GF(2^8) (FIPS 197 section 4.2.1, xtime): shift left and, when bit 7 was set, add x^8 = {1b}; the reduction mask is 0 - bit7, not a branch.
def xtime
def mul3_word{03} * x = {02} * x + x.
def mul3

type QuadShared representation only; this module contains no algorithm or operations.
type State

def cat
def len
def le32LE32(n) for n < 2^32.
def hp_goH' for T > 64 (RFC 9106 section 3.3): W1 || ..
def hp_pick
def hprimeH'^T(a): the variable-length hash, over LE32(T) || a.
def h0H0 (RFC 9106 section 3.2, step 1), version 0x13 and type 2 (Argon2id).
def block_ofA block from its 1024 little-endian bytes.
def state_bytes
def block_bytesThe 1024 little-endian bytes of a block.
def row_at
def at
def laneLane n (0 <= n < 128) of a block.
def hi
def small
def input_ofZ = (r, l, s, m', t, y, i), zero-padded to a block.
def input_block(r is inspected first, so the proofs keep an input block with a symbolic pass folded instead of compressing it symbolically.)
def addressesThe address block of counter ctr: G(0, G(0, Z)).
def regenThe address block for position idx: a new one at the segment's first position and at every multiple of 128 (data-independent segments only).
def area_base|W|, the number of blocks the reference may be drawn from.
def area_other
def area
def rel|W| - 1 - (|W| * (J1^2 / 2^32)) / 2^32
def start_last
def startThe first block of the reference area: 0 in the first pass, else the start of the next segment (wrapping).
def ref_lane
def prev_index
def pick
def store_xor
def storeB[l][j] = G(B[l][j-1], B[l'][z']), XORed into the old block after the first pass.
def with_ref
def stepOne block: pair holds the memory and the previous block.
def seg_goPositions idx ..
def start_index