bend-osdev-cbc

Releases (1)

• 0.1.0.0 indexed

Definitions (95)

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)

check.bend

• def err
• def res
• def backwhether r is m
• def bytes.gon pseudo-random bytes (a linear congruential generator)
• def msg
• def iv
• def toy.rotA toy permutation of blocks, NOT a cipher: the words rotated, then XOR with the key block.
• def toy.unrot
• def toy.enc
• def toy.dec
• def key
• def key2
• def hexs
• def main

LAWS.bend

• law cbc_blocks_round_trip
• law cbc_round_tripCBC on bytes: for every 16-byte IV and every message of whole blocks, encryption succeeds and decryption gives the message back

LAWS_padded.bend

• law cbc_padded_round_tripfor every cipher and key with inv (as LAWS.bend's laws take it), every 16-byte IV and every message: encryption succeeds and decryption gives the message back

PROOF.bend

• def sp.cons_tail
• def sp.eta
• def sp.blk
• def sp.mask_blk
• def sp.join_split
• def oc.masked
• def oc.len
• def tr.split_eq
• def tr.join_eq
• def tr.bind_cong
• def cmp.hd
• def cmp.tl
• def bx.bool
• def bx.word
• def bx.u32
• def bx.blockxor(a, xor(a, b)) == b on blocks
• def sp.disc
• def sp.absurd
• def sp.absurd_tail
• def sp.snd_go
• def sp.mod16
• def sp.mod_taila list of whole blocks splits with no tail
• def sp.split_join
• def sp.mask_join
• def oc.mod
• def cbcp.iva 16-byte IV is the block of its bytes
• def tr.cbc_enc_go
• def tr.cbc_enc_eq
• def tr.cbc_dec_go
• def tr.cbc_dec_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 cbcp.insthe blocks CBC encryption gives the cipher: each plaintext block XOR the block before it (the IV first)
• def cbcp.go

PROOF_padded.bend

• def pk.disc
• def pk.empty
• def pk.absurd
• def pk.ug
• def pd.disc
• def pd.fd
• def pd.val
• def pd.inj
• def pd.ndisc
• def pd.nd
• def pd.len0
• def pd.nil
• def pd.e0CBC decryption of no bytes, under any IV, is no bytes
• def pd.dpxdecrypt_padded with its first check as an argument
• def pd.dc0an empty ciphertext cannot decrypt to M': its decryption is empty, and unpadding the empty string is refused
• def pd.dcfrom the ciphertext c, decrypting gives M' and unpadding M' gives m
• def pd.go