bend-osdev-cipher-modes

Releases (1)

• 0.1.0.0 indexed

Definitions (444)

ccm.bend

• def ccm.ctrb.fast
• def ccm.xcrypt.fast
• def ccm.ebody.fast
• def ccm.e2.fast
• def ccm.dbody.fast
• def ccm.d3.fast
• def ccm.d2.fast
• def Ccm.encrypt.refCcm.encrypt and Ccm.decrypt through the structural forms (the laws' proofs reason about these; PROOF.bend proves them equal to the public defs)
• def Ccm.decrypt.ref
• def Ccm.encryptp with associated data aad under the nonce: the ciphertext, then the m-byte tag
• def Ccm.decryptthe plaintext of c (the ciphertext, then the m-byte tag), or CmTagMismatch when the tag does not match; no plaintext is released from a message that fails

check.bend

• def err
• def res
• def bulk.goLonger messages, as a regression test for long inputs: 32 KB of pseudo-random bytes (a linear congruential generator) through CBC, and 32 KB and 5 bytes through XTS (ciphertext stealing), each encrypted and decrypted back; the last 16 bytes of each ciphertext were checked against Python's cryptography
• def bulk.key
• def bulk.key2
• def bulk.iv
• def bulk.same
• def bulk.cbc
• def bulk.xts
• def bulk.nonce
• def bulk.aad
• def bulk.ccm
• def main

cipher_modes.bend

• type CmBlock
• type CmErrorEvery failure a mode can report
• def CmBlock.zero
• def CmBlock.xor
• def cm.bytea byte (the low 8 bits of x), as bend-osdev-bytes masks it
• def cm.bits8
• def cm.of8
• def cm.wordthe word with bytes a, b, c, d, most significant first
• def cm.b0the bytes of w, most significant first
• def cm.b1
• def cm.b2
• def cm.b3
• def cm.unwordthe four bytes of w, most significant first, in front of rest
• def cm.w0
• def cm.w1
• def cm.w2
• def cm.w3
• def cm.bytes_ontothe 16 bytes of a block in front of rest (always 16 cells, whatever b is)
• def cm.bytes_of
• def cm.block16
• def cm.block_of.full
• def cm.block_ofthe block of the first 16 bytes of xs, zero-filled if xs is shorter
• type CmSplitA byte string as its whole blocks and the 0 to 15 bytes after them
• def cm.split.cons
• def cm.split
• def cm.split.blocks
• def cm.split.tail
• def cm.join_ontothe bytes of the blocks bs, in front of rest
• def cm.join
• def cm.xor_bytesbyte-wise XOR, as long as the shorter list
• def cm.blocks.rev_ontothe blocks of bs in reverse order, in front of acc
• def cm.blocks.len.go
• def cm.blocks.lenthe number of blocks (List.length)
• def cm.blocks.appendxs, then ys (List.append)
• def cm.split.gothe blocks split so far are kept reversed in acc (cm.split)
• def cm.split.fast
• def cm.join.gothe bytes of the blocks rs (last first) in front of acc
• def cm.join_onto.fastcm.join_onto
• def cm.xor_bytes.go
• def cm.xor_bytes.fastcm.xor_bytes
• def cm.diff
• def cm.ct_eqequality of two byte lists with no early exit of the same length (a tag check)
• def cm.mask0 for a 0 bit, all ones for a 1 bit (the low bit of b)
• def cm.check
• def cm.need_block.picka 16-byte value as a block, or the error e
• def cm.need_block
• def CmBlock.to_octets
• def CmBlock.of_octets.pick
• def CmBlock.of_octetsa 16-byte string as a block; None for any other length
• def CmBlock.hex

cmac.bend

• def Cmac.dbl
• def cmac.k1
• def cmac.k2
• def Cmac.subkey1the subkeys K1 and K2
• def Cmac.subkey2
• type CmacStateThe state: the chaining value x, and the bytes not yet processed (at most 16, newest first) and their count.
• def Cmac.start
• def cmac.push
• def cmac.step
• def cmac.feed
• def Cmac.updatethe state after the bytes of m
• def cmac.lastthe last block: whole, xor K1; partial (or empty), padded, xor K2
• def Cmac.finishthe 16-byte MAC
• def Cmac.macThe MAC of m in one call
• def Cmac.verifywhether tag is m's 16-byte MAC, compared with no early exit

pkcs7.bend

• def pkcs7.filln bytes of value v
• def pkcs7.size_ok
• def pkcs7.pad.octm and its padding (on Octets, so that a long message is not walked as a list: Bend 2.0.37's runtime overflows its stack on deep structural recursion)
• def Pkcs7.pad.go
• def Pkcs7.padm padded to a whole number of bs-byte blocks
• def pkcs7.diff0 when every byte of xs is v
• def pkcs7.lastthe last byte, or d if there is none
• def pkcs7.strip
• def pkcs7.unpad.octthe value p of the last byte must be 1 to bs, and the last p bytes all p (on Octets of n bytes, so that only those p bytes become a list)
• def Pkcs7.unpad.go
• def Pkcs7.unpadm without its padding; m must be a non-empty whole number of blocks