bend-osdev-cipher-modes

Releases (1)

• 0.1.0.0 indexed

Definitions (444)

aes.bend

• type CmAesState
• def aes.byte
• def aes.state_of
• def aes.block_of
• def aes.add
• def aes.inv_shift_subInvShiftRows: row r moves r columns to the right InvSubBytes: the inverse S-box on every byte (both in one pass)
• def aes.m9multiples of a byte by 9, 11, 13 and 14
• def aes.m11
• def aes.m13
• def aes.m14
• def aes.mix0
• def aes.inv_mixInvMixColumns: each column times {0e, 0b, 0d, 09}, rotated per row
• def aes.roundsThe inverse cipher over the round keys, last round key first: AddRoundKey(Nr), then Nr - 1 rounds of InvShiftRows, InvSubBytes, AddRoundKey, InvMixColumns, then InvShiftRows, InvSubBytes, AddRoundKey(0)
• def aes.decrypt
• def aes.sub_word
• def aes.rot_word
• def aes.rcon.go
• def aes.rconx^(j - 1) in GF(2^8), the round constant of word j * Nk
• def aes.temp.bigNk > 6 and i mod Nk = 4: SubWord alone
• def aes.temptemp from w[i - 1], for word i
• def aes.head
• def aes.tail
• def aes.last
• def aes.expand.gon more words from word i; win holds the last Nk words, oldest first, and acc every word so far, newest first
• def aes.wordsthe key's bytes as big-endian words
• def aes.round_keys
• def aes.expandthe 4 (Nr + 1) words of the schedule, Nr = Nk + 6
• type CmAesKeyAn expanded AES key: bend-collections' schedule for encryption, the key's bytes, and the round keys for decryption, last first, once CmAes.prepare has computed them (Nil until then: CmAes.decrypt then derives them for each block).
• def aes.key.go
• def aes.key.pick
• def aes.dkeysthe decryption round keys: the ones computed already, or from the key bytes
• def CmAes.keya 16-byte (AES-128) or 32-byte (AES-256) key
• def CmAes.key128
• def CmAes.key256
• def aes.of_maybe
• def CmAes.encryptone block, encrypted (bend-collections' encrypt_block)
• def CmAes.preparethe key with its decryption round keys computed, for decrypting many blocks
• def CmAes.decryptone block, decrypted (the inverse cipher above)

aes_modes.bend

• def CmAes.cbc_encrypt
• def CmAes.cbc_decrypt
• def CmAes.cbc_encrypt_padded
• def CmAes.cbc_decrypt_padded
• def CmAes.xts_encryptthe data unit p with 16-byte sequence number i (Xts.sector(n) for sector n)
• def CmAes.xts_decrypt
• def CmAes.ccm_encryptCCM with an m-byte tag: the ciphertext, then the tag
• def CmAes.ccm_decrypt
• def CmAes.cmacAES-CMAC (RFC 4493 with a 16-byte key): the 16-byte MAC

cbc.bend

• def cbc.enc
• def cbc.dec
• def cbc.enc.go
• def cbc.enc.fast
• def cbc.dec.go
• def cbc.dec.fast
• def Cbc.encrypt_blocks
• def Cbc.decrypt_blocks
• def cbc.iv
• def cbc.e2the whole blocks under v, or CmNotBlockMultiple(n) if bytes are left over
• def cbc.e1
• def cbc.d2
• def cbc.d1
• def cbc.e2.fast
• def cbc.e1.fast
• def cbc.d2.fast
• def cbc.d1.fast
• def Cbc.encrypt.refCbc.encrypt and Cbc.decrypt through the structural forms (the laws' proofs reason about these; PROOF.bend proves them equal to the public defs)
• def Cbc.decrypt.ref
• def Cbc.encrypt
• def Cbc.decrypt
• def Cbc.encrypt_paddedm of any length, PKCS #7 padded to whole blocks, then encrypted
• def Cbc.decrypt_paddeddecrypted, then the padding checked and removed (CmBadPadding)

ccm.bend

• def ccm.bethe low n bytes of v, most significant first (zeros above the 32 bits of v)
• def ccm.padxs zero-padded to a whole number of blocks
• def ccm.alen.pickl(a): two bytes below 65280 (2^16 - 2^8), else 0xFF 0xFE and four bytes
• def ccm.aad.pick
• def ccm.cbcmacCBC-MAC of whole blocks, from x
• def ccm.macthe CBC-MAC of B_0, the encoded a and the padded p
• def ccm.tagthe tag: the first m bytes of the MAC
• def ccm.aiA_i = A_0 with counter i (i < 2^(8L), so it stays in the counter field)
• def ccm.ctrbCTR on whole blocks: b_j xor S_(i+j)
• def ccm.xcryptCTR from counter 1: the whole blocks, then the tail xor the next S_i
• def ccm.a0A_0: (L-1) || nonce || zeros
• def ccm.tag_ok
• def ccm.len_ok.threethe message must be shorter than 2^(8L) bytes: a bound only for L = 2 or 3 (with L >= 4 every list is shorter)
• def ccm.len_ok.two
• def ccm.len_ok
• def ccm.checks.len
• def ccm.checks.nonce
• def ccm.checks.tag
• def ccm.checksthe tag length, the nonce length and the message length n, in that order
• def ccm.ebodythe ciphertext of pv, then the tag
• def ccm.e2
• def ccm.open
• def ccm.dbodythe plaintext, if the tag (compared with no early exit) matches
• def ccm.d3
• def ccm.d2
• def ccm.pad.fast
• def ccm.aad.pick.fast
• def ccm.mac.fast
• def ccm.tag.fast
• def ccm.ctrb.gothe blocks so far kept reversed in acc