bend-osdev-cipher-modes

Releases (1)

• 0.1.0.0 indexed

Definitions (444)

xts.bend

• def xts.shifteach byte of w shifted left, with the carries between w's own bytes
• def xts.carrythe carry out of w's last byte, into the first byte of the next word
• def Xts.mul_alpha
• def xts.benc
• def xts.bdec
• def xts.enc
• def xts.dec
• def xts.enc.go
• def xts.enc.fast
• def xts.dec.go
• def xts.dec.fast
• def Xts.encrypt_blocks
• def Xts.decrypt_blocks
• def Xts.tweakT_0: the encrypted sequence number
• def Xts.sectorthe 16-byte sequence number of data unit n (a sector number): n in little-endian order, then zeros
• def xts.alpha_nT_0 * alpha^n
• def xts.steal_c.go
• def xts.steal_t.go
• def xts.steal_cthe ciphertext of the last whole block p and the tail, under tweak t
• def xts.steal_t
• def xts.dsteal.gothe plaintext of the last whole ciphertext block c and the tail
• def xts.dsteal
• def xts.initall but the last of p then rest; and the last
• def xts.last
• def xts.eout
• def xts.dout
• def xts.e2
• def xts.d2
• def xts.e1
• def xts.d1
• def xts.tweak.go
• def xts.tweakT_0, from the 16-byte sequence number i
• def xts.init.go
• def xts.init.fast
• def xts.eout.fast
• def xts.dout.fast
• def xts.e2.fast
• def xts.d2.fast
• def xts.e1.fast
• def xts.d1.fast
• def Xts.encrypt.refXts.encrypt and Xts.decrypt through the structural forms (the laws' proofs reason about these; PROOF.bend proves them equal to the public defs)
• def Xts.decrypt.ref
• def Xts.encryptthe data unit p (at least 16 bytes) with sequence number i (16 bytes)
• def Xts.decryptdecryption needs enc too: the tweak is always encrypted