bend-osdev-cbc Releases (1): 0.1.0.0 0x4ff94cd9a03eee1d38142effbcc617fb indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-cbc@0.1.0.0 Definitions (95): LAWS.cbc_blocks_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/LAWS.bend&name=cbc_blocks_round_trip) law cbc_blocks_round_trip: for ~K: Data for ~enc: K -> M.CmBlock -> M.CmBlock for ~dec: K -> M.CmBlock -> M.CmBlock for +k: K for inv: @xs: List<&2, M.CmBlock> -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>} for iv: M.CmBlock for bs: List<&2, M.CmBlock> {C.Cbc.decrypt_blocks(~K, ~dec, k, iv, C.Cbc.encrypt_blocks(~K, ~enc, k, iv, bs)) == bs : List<&2, M.CmBlock>} LAWS.cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/LAWS.bend&name=cbc_round_trip) # CBC on bytes: for every 16-byte IV and every message of whole blocks, # encryption succeeds and decryption gives the message back law cbc_round_trip: for ~K: Data for ~enc: K -> M.CmBlock -> M.CmBlock for ~dec: K -> M.CmBlock -> M.CmBlock for +k: K for inv: @xs: List<&2, M.CmBlock> -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>} for +iv: B.Octets for +m: B.Octets for hi: {B.Octets.len(iv) == 16n : Nat} … LAWSPadded.cbc_padded_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/LAWS_padded.bend&name=cbc_padded_round_trip) # for 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 law cbc_padded_round_trip: for ~K: Data for ~enc: K -> M.CmBlock -> M.CmBlock for ~dec: K -> M.CmBlock -> M.CmBlock for +k: K for inv: @xs: List<&2, M.CmBlock> -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>} for +iv: B.Octets for +m: B.Octets … PROOF.sp.cons_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.cons_tail) def sp.cons_tail(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}: PROOF.sp.eta (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.eta) def sp.eta(s: M.CmSplit) -> {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}: PROOF.sp.blk (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.blk) def sp.blk(b: M.CmBlock, rest: List<&2, U32>) -> {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}: PROOF.sp.mask_blk (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.mask_blk) def sp.mask_blk(b: M.CmBlock, rest: List<&2, U32>) -> {B.mask(M.cm.bytes_onto(b, rest)) == M.cm.bytes_onto(b, B.mask(rest)) : List<&2, U32>}: PROOF.sp.join_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.join_split) def sp.join_split(ys: List<&2, U32>) -> {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}: PROOF.oc.masked (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=oc.masked) def oc.masked(+o: B.Octets) -> {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}: PROOF.oc.len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=oc.len) def oc.len(+o: B.Octets, +n: Nat, h: {B.Octets.len(o) == n : Nat}) -> {B.len(B.Octets.to_list(o)) == n : Nat}: PROOF.tr.split_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.split_eq) def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}: PROOF.tr.join_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.join_eq) def tr.join_eq(+bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}: PROOF.tr.bind_cong (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.bind_cong) def tr.bind_cong(r: Result<&2, &2, M.CmError, B.Octets>, f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}) -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, f) == Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, g) : Result<&2, &2, M.CmError, B.Octets>}: PROOF.cmp.hd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=cmp.hd) def cmp.hd(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {dec(k, enc(k, x)) == x : M.CmBlock}: PROOF.cmp.tl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=cmp.tl) def cmp.tl(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}: PROOF.bx.bool (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=bx.bool) def bx.bool(a: Bool, b: Bool) -> {Bool.xor(a, Bool.xor(a, b)) == b : Bool}: PROOF.bx.word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=bx.word) def bx.word(n: Nat, a: Word(n), b: Word(n)) -> {Word.xor(n, a, Word.xor(n, a, b)) == b : Word(n)}: PROOF.bx.u32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=bx.u32) def bx.u32(a: U32, b: U32) -> {U32.xor(a, U32.xor(a, b)) == b : U32}: PROOF.bx.block (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=bx.block) # xor(a, xor(a, b)) == b on blocks def bx.block(+a: M.CmBlock, +b: M.CmBlock) -> {M.CmBlock.xor(a, M.CmBlock.xor(a, b)) == b : M.CmBlock}: PROOF.sp.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.disc) def sp.disc(n: Nat) -> Type: PROOF.sp.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.absurd) def sp.absurd(p: Nat, h: {1n+p == 0n : Nat}) -> Empty: PROOF.sp.absurd_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.absurd_tail) def sp.absurd_tail(p: Nat, xs: List<&2, U32>, h: {1n+p == 0n : Nat}) -> {M.cm.split.tail(M.cm.split(B.mask(xs))) == Nil{} : List<&2, U32>}: PROOF.sp.snd_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.snd_go) def sp.snd_go(n: Nat, m: Nat, d1: Nat, d2: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d1, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d2, r)) : Nat}: PROOF.sp.mod16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.mod16) def sp.mod16(n: Nat) -> {Nat.mod(Nat.add(16n, n), 16n) == Nat.mod(n, 16n) : Nat}: PROOF.sp.mod_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.mod_tail) # a list of whole blocks splits with no tail def sp.mod_tail(ys: List<&2, U32>) -> {Nat.mod(B.len(ys), 16n) == 0n : Nat} -> {M.cm.split.tail(M.cm.split(B.mask(ys))) == Nil{} : List<&2, U32>}: PROOF.sp.split_join (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.split_join) def sp.split_join(bs: List<&2, M.CmBlock>) -> {M.cm.split(M.cm.join_onto(bs, Nil{})) == M.CmSplit{bs, Nil{}} : M.CmSplit}: PROOF.sp.mask_join (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=sp.mask_join) def sp.mask_join(bs: List<&2, M.CmBlock>) -> {B.mask(M.cm.join_onto(bs, Nil{})) == M.cm.join_onto(bs, Nil{}) : List<&2, U32>}: PROOF.oc.mod (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=oc.mod) def oc.mod(+o: B.Octets, h: {Nat.mod(B.Octets.len(o), 16n) == 0n : Nat}) -> {Nat.mod(B.len(B.Octets.to_list(o)), 16n) == 0n : Nat}: PROOF.cbcp.iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=cbcp.iv) # a 16-byte IV is the block of its bytes def cbcp.iv(+iv: B.Octets, h: {B.Octets.len(iv) == 16n : Nat}) -> {C.cbc.iv(iv) == Done{M.cm.block_of(B.Octets.to_list(iv))} : Result<&2, &2, M.CmError, M.CmBlock>}: PROOF.tr.cbc_enc_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_enc_go) def tr.cbc_enc_go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {C.cbc.enc.go(~K, ~enc, k, bs, iv, acc) == M.cm.blocks.rev_onto(acc, C.cbc.enc(~K, ~enc, k, bs, iv)) : List<&2, M.CmBlock>}: PROOF.tr.cbc_enc_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_enc_eq) def tr.cbc_enc_eq(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {C.cbc.enc(~K, ~enc, k, bs, iv) == C.cbc.enc.fast(~K, ~enc, k, bs, iv) : List<&2, M.CmBlock>}: PROOF.tr.cbc_dec_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_dec_go) def tr.cbc_dec_go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {C.cbc.dec.go(~K, ~dec, k, bs, iv, acc) == M.cm.blocks.rev_onto(acc, C.cbc.dec(~K, ~dec, k, bs, iv)) : List<&2, M.CmBlock>}: PROOF.tr.cbc_dec_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_dec_eq) def tr.cbc_dec_eq(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {C.cbc.dec(~K, ~dec, k, bs, iv) == C.cbc.dec.fast(~K, ~dec, k, bs, iv) : List<&2, M.CmBlock>}: PROOF.tr.cbc_e2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_e2) def tr.cbc_e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +v: M.CmBlock, s: M.CmSplit, +n: Nat) -> {C.cbc.e2(~K, ~enc, k, v, s, n) == C.cbc.e2.fast(~K, ~enc, k, v, s, n) : Result<&2, &2, M.CmError, B.Octets>}: PROOF.tr.cbc_e1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_e1) def tr.cbc_e1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> {C.cbc.e1(~K, ~enc, k, r, xs) == C.cbc.e1.fast(~K, ~enc, k, r, xs) : Result<&2, &2, M.CmError, B.Octets>}: PROOF.tr.cbc_d2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_d2) def tr.cbc_d2(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +v: M.CmBlock, s: M.CmSplit, +n: Nat) -> {C.cbc.d2(~K, ~dec, k, v, s, n) == C.cbc.d2.fast(~K, ~dec, k, v, s, n) : Result<&2, &2, M.CmError, B.Octets>}: PROOF.tr.cbc_d1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_d1) def tr.cbc_d1(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> {C.cbc.d1(~K, ~dec, k, r, xs) == C.cbc.d1.fast(~K, ~dec, k, r, xs) : Result<&2, &2, M.CmError, B.Octets>}: PROOF.tr.cbc_encrypt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_encrypt) def tr.cbc_encrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +m: B.Octets) -> {C.Cbc.encrypt.ref(~K, ~enc, k, iv, m) == C.Cbc.encrypt(~K, ~enc, k, iv, m) : Result<&2, &2, M.CmError, B.Octets>}: PROOF.tr.cbc_decrypt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=tr.cbc_decrypt) def tr.cbc_decrypt(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +c: B.Octets) -> {C.Cbc.decrypt.ref(~K, ~dec, k, iv, c) == C.Cbc.decrypt(~K, ~dec, k, iv, c) : Result<&2, &2, M.CmError, B.Octets>}: PROOF.cbcp.ins (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=cbcp.ins) # the blocks CBC encryption gives the cipher: each plaintext block XOR the # block before it (the IV first) def cbcp.ins(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> List<&2, M.CmBlock>: PROOF.cbcp.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=cbcp.go) def cbcp.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, cbcp.ins(~K, ~enc, k, bs, iv)) == cbcp.ins(~K, ~enc, k, bs, iv) : List<&2, M.CmBlock>} -> {C.cbc.dec(~K, ~dec, k, C.cbc.enc(~K, ~enc, k, bs, iv), iv) == bs : List<&2, M.CmBlock>}: PROOFPadded.pk.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pk.disc) def pk.disc(b: Bool) -> Type: PROOFPadded.pk.empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pk.empty) def pk.empty(h: {False{} == True{} : Bool}) -> Empty: PROOFPadded.pk.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pk.absurd) def pk.absurd(-A: Type, h: {False{} == True{} : Bool}) -> A: PROOFPadded.pk.ug (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pk.ug) def pk.ug(+bs: Nat, +m: B.Octets, +n: Nat, +md: Nat) -> Result<&2, &2, M.CmError, B.Octets>: PROOFPadded.pd.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.disc) def pd.disc(-A: Data, r: Result<&2, &2, M.CmError, A>) -> Type: PROOFPadded.pd.fd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.fd) def pd.fd(-A: Data, +e: M.CmError, +x: A, h: {Fail{e} == Done{x} : Result<&2, &2, M.CmError, A>}) -> Empty: PROOFPadded.pd.val (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.val) def pd.val(-A: Data, r: Result<&2, &2, M.CmError, A>, d: A) -> A: PROOFPadded.pd.inj (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.inj) def pd.inj(-A: Data, +a: A, +b: A, h: {Done{a} == Done{b} : Result<&2, &2, M.CmError, A>}) -> {a == b : A}: PROOFPadded.pd.ndisc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.ndisc) def pd.ndisc(n: Nat) -> Type: PROOFPadded.pd.nd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.nd) def pd.nd(+p: Nat, h: {1n+p == 0n : Nat}) -> Empty: PROOFPadded.pd.len0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.len0) def pd.len0(+x: Nat) -> {Nat.is_lt(0n, x) == False{} : Bool} -> {x == 0n : Nat}: PROOFPadded.pd.nil (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.nil) def pd.nil(xs: List<&2, U32>) -> {B.len(xs) == 0n : Nat} -> {xs == Nil{} : List<&2, U32>}: PROOFPadded.pd.e0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.e0) # CBC decryption of no bytes, under any IV, is no bytes def pd.e0(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +mp: B.Octets) -> {C.cbc.d1.fast(~K, ~dec, k, r, Nil{}) == Done{mp} : Result<&2, &2, M.CmError, B.Octets>} -> {B.Octets.len(mp) == 0n : Nat}: PROOFPadded.pd.dpx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.dpx) # decrypt_padded with its first check as an argument def pd.dpx(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, +c: B.Octets, ok: Bool) -> Result<&2, &2, M.CmError, B.Octets>: PROOFPadded.pd.dc0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.dc0) # an empty ciphertext cannot decrypt to M': its decryption is empty, and # unpadding the empty string is refused def pd.dc0(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +mp: B.Octets, +m: B.Octets, e2: {P.Pkcs7.unpad(16n, mp) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, +c: B.Octets, eo: {Nat.is_lt(0n, B.Octets.len(c)) == False{} : Bool}, e1: {C.Cbc.decrypt(~K, ~dec, k, iv, c) == Done{mp} : Result<&2, &2, M.CmError, B.Octets>}) -> {C.Cbc.decrypt_padded(~K, ~dec, k, iv, c) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}: PROOFPadded.pd.dc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.dc) # from the ciphertext c, decrypting gives M' and unpadding M' gives m def pd.dc(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +mp: B.Octets, +m: B.Octets, e2: {P.Pkcs7.unpad(16n, mp) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, +c: B.Octets, ok: Bool) -> {Nat.is_lt(0n, B.Octets.len(c)) == ok : Bool} -> {C.Cbc.decrypt(~K, ~dec, k, iv, c) == Done{mp} : Result<&2, &2, M.CmError, B.Octets>} -> {C.Cbc.decrypt_padded(~K, ~dec, k, iv, c) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}: PROOFPadded.pd.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.go) def pd.go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +mp: B.Octets, +m: B.Octets, e2: {P.Pkcs7.unpad(16n, mp) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, r: Result<&2, &2, M.CmError, B.Octets>) -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, c => C.Cbc.decrypt(~K, ~dec, k, iv, c)) == Done{mp} : Result<&2, &2, M.CmError, B.Octets>} -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, c => C.Cbc.decrypt_padded(~K, ~dec, k, iv, c)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}: Cbc.cbc.enc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.enc) def cbc.enc(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>: Cbc.cbc.dec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.dec) def cbc.dec(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>: Cbc.cbc.enc.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.enc.go) def cbc.enc.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>: Cbc.cbc.enc.fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.enc.fast) def cbc.enc.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>: Cbc.cbc.dec.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.dec.go) def cbc.dec.go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>: Cbc.cbc.dec.fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.dec.fast) def cbc.dec.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>: Cbc.Cbc.encrypt_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.encrypt_blocks) def Cbc.encrypt_blocks(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>: Cbc.Cbc.decrypt_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.decrypt_blocks) def Cbc.decrypt_blocks(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>: Cbc.cbc.iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.iv) def cbc.iv(o: B.Octets) -> Result<&2, &2, M.CmError, M.CmBlock>: Cbc.cbc.e2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.e2) # the whole blocks under v, or CmNotBlockMultiple(n) if bytes are left over def cbc.e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.cbc.e1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.e1) def cbc.e1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.cbc.d2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.d2) def cbc.d2(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.cbc.d1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.d1) def cbc.d1(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.cbc.e2.fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.e2.fast) def cbc.e2.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.cbc.e1.fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.e1.fast) def cbc.e1.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.cbc.d2.fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.d2.fast) def cbc.d2.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.cbc.d1.fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.d1.fast) def cbc.d1.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.Cbc.encrypt.ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.encrypt.ref) # Cbc.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.encrypt.ref(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.Cbc.decrypt.ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.decrypt.ref) def Cbc.decrypt.ref(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.Cbc.encrypt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.encrypt) def Cbc.encrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.Cbc.decrypt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.decrypt) def Cbc.decrypt(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.Cbc.encrypt_padded (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.encrypt_padded) # m of any length, PKCS #7 padded to whole blocks, then encrypted def Cbc.encrypt_padded(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Cbc.Cbc.decrypt_padded (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=Cbc.decrypt_padded) # decrypted, then the padding checked and removed (CmBadPadding) def Cbc.decrypt_padded(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, +c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Check.err (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=err) def err(e: M.CmError) -> String: Check.res (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=res) def res(r: Result<&2, &2, M.CmError, B.Octets>) -> String: Check.back (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=back) # whether r is m def back(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String: Check.bytes.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=bytes.go) # n pseudo-random bytes (a linear congruential generator) def bytes.go(n: Nat, +s: U32, acc: List<&2, U32>) -> List<&2, U32>: Check.msg (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=msg) def msg(n: Nat) -> B.Octets: Check.iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=iv) def iv() -> B.Octets: Check.toy.rot (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=toy.rot) # A toy permutation of blocks, NOT a cipher: the words rotated, then XOR # with the key block. Enough to run the mode's code paths (encryption and # decryption differ, so mixing them up shows); the mode is tested against # its specification over AES in bend-osdev-aes-modes (the specifications' # vectors) and in ref/ (against Python's cryptography). def toy.rot(b: M.CmBlock) -> M.CmBlock: Check.toy.unrot (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=toy.unrot) def toy.unrot(b: M.CmBlock) -> M.CmBlock: Check.toy.enc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=toy.enc) def toy.enc(k: M.CmBlock, b: M.CmBlock) -> M.CmBlock: Check.toy.dec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=toy.dec) def toy.dec(k: M.CmBlock, c: M.CmBlock) -> M.CmBlock: Check.key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=key) def key() -> M.CmBlock: Check.key2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=key2) def key2() -> M.CmBlock: Check.hexs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=hexs) def hexs(bs: List<&2, M.CmBlock>) -> String: Check.main (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/check.bend&name=main) def main() -> IO(Unit):