bend-osdev-cipher-modes

Releases (1)

• 0.1.0.0 indexed

Definitions (444)

aes.bend

• def aes.xt
• def aes.gmul.go
• def aes.gmul
• def aes.inv.goa := a^2 * x, n times: from a = x, six times gives x^127
• def aes.invthe multiplicative inverse, x^254 (0 for 0)
• def aes.rotl
• def aes.sboxthe S-box: the inverse, then the affine map
• def aes.isboxthe inverse S-box: the inverse affine map, then the inverse

PROOF.bend

• def tr.init_eq
• def tr.cbc_e2
• def tr.cbc_e1
• def tr.cbc_d2
• def tr.cbc_d1
• def tr.cbc_encrypt
• def tr.cbc_decrypt
• def tr.xts_eout
• def tr.xts_dout
• def tr.xts_e2
• def tr.xts_d2
• def tr.xts_e1
• def tr.xts_d1
• def tr.xts_encrypt
• def tr.xts_decrypt
• def tr.bind_conga bind whose continuations agree on every value agrees
• def tr.pad
• def tr.aad
• def tr.mac
• def tr.tag
• def tr.ctrb_go
• def tr.ctrb_eq
• def tr.xcrypt
• def tr.ebody
• def tr.e2
• def tr.ccm_encrypt
• def tr.dbody
• def tr.d3
• def tr.d2
• def tr.ccm_decrypt
• def cbcp.go
• def bx.rbool
• def bx.rword
• def bx.ru32
• def bx.rblock
• def xtsp.blkone block under one tweak: D(E(p xor t) xor t xor t) xor t == p
• def xtsp.go
• def cmacp.feed
• def sp.mask_join_onto
• def sp.split_join_shortblocks joined in front of a short tail split back into those blocks and tail
• def sp.join_append
• def li.init_app
• def li.last_app
• def li.init_last
• def li.len_enc
• def oc.le16
• def xtsp.tweak
• def xtsp.mask_steal_tthe final partial ciphertext block is masked, and splits into no blocks
• def xtsp.lt_take
• def xtsp.split_steal_t
• def xtsp.len16the bytes the stealing passes through: tl, then the stolen tail of b
• def xtsp.maskY
• def xtsp.ppY
• def xtsp.stealCiphertext stealing undoes itself: the last whole block p and a tail tl (masked, fewer than 16 bytes), encrypted by steal_c and steal_t and decrypted by dsteal, come back as p's bytes and then tl
• def xtsp.d2
• def bx.wself
• def bits.xor_self
• def bits.xor_xor
• def li.mask_xor
• def li.len_xor
• def li.xor_xor
• def li.len_bytes
• def na.add_zero
• def na.add_succ
• def na.sub_zero
• def na.sub_add(a + b) - b == a
• def na.le_zero
• def na.le_addb <= a + b
• def bo.and_r
• def bo.and_l
• def rs.disc
• def rs.empty
• def rs.absurd
• def ccmp.tag_le.gochecks that pass mean a tag of at most 16 bytes
• def ccmp.tag_le
• def ccmp.diff_self
• def ccmp.ct_refl
• def ccmp.len_ctrb
• def ccmp.ctrb2CTR twice is the identity on blocks
• def ccmp.mask_xcrypt
• def ccmp.len_join
• def ccmp.xt_shortthe CTR tail is as short as the plaintext tail
• def ccmp.xxCTR from counter 1 undoes itself (on a masked byte string)
• def ccmp.len_xcand keeps its length
• def ccmp.xxp
• def ccmp.len_xcp
• def ccmp.len_tag
• def ccmp.le_tag
• def ccmp.mask_tag
• def ccmp.mask_eb
• def ccmp.len_eb
• def ccmp.maindecryption accepts what encryption produced, whatever the parameter checks answer