pcbc.bend

bend-osdev-crypto@0.1.0.0 · 86 lines · 10 definitions

1# PCBC, propagating cipher block chaining, over any block cipher of any block
2# size (the block-cipher interface, block.bend), as the FCrypt specification
3# (T. Anderson, 2000, "Modes of operation") and Kerberos version 4 use it:
4#   C_i = E(P_i xor V_i),  V_1 = IV,  V_(i+1) = P_i xor C_i
5#   P_i = D(C_i) xor V_i
6# on lists of blocks and on bytes (a whole number of blocks, no padding; the
7# chaining value after the last block is P_n xor C_n, so a message may
8# arrive a block at a time through the block layer, CrPcbc.next_iv).
9#
10# Every loop over blocks is a tail call; the structural forms the proofs use
11# are proved equal to them in PROOF.bend. Decryption undoes encryption for
12# every key, IV and list of blocks wherever the cipher's decryption undoes
13# its encryption: a law per instance (gen/instances.py, <c>_pcbc_round_trip).
14import Base
15import bend-osdev-bytes@0.1.0.0/bytes.bend as B
16import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
17import bend-osdev-crypto@0.1.0.0/modes.bend as Md
18
19# Structural forms (the proofs' reference)
20
21def cr.pcbc.enc(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, v: Blk) -> List<&2, Blk>:
22  match bs:
23    case Nil{}:
24      Nil{}
25    case Con{+p, t}:
26      +c = enc(k, bxor(p, v))
27      Con{c, cr.pcbc.enc(~K, ~Blk, ~enc, ~bxor, k, t, bxor(p, c))}
28
29def cr.pcbc.dec(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, v: Blk) -> List<&2, Blk>:
30  match bs:
31    case Nil{}:
32      Nil{}
33    case Con{+c, t}:
34      +p = bxor(dec(k, c), v)
35      Con{p, cr.pcbc.dec(~K, ~Blk, ~dec, ~bxor, k, t, bxor(p, c))}
36
37# The loops that run
38
39def cr.pcbc.enc.go(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, v: Blk, acc: List<&2, Blk>) -> List<&2, Blk>:
40  match bs:
41    case Nil{}:
42      Md.cr.blks.rev_onto(~Blk, acc, Nil{})
43    case Con{+p, t}:
44      +c = enc(k, bxor(p, v))
45      cr.pcbc.enc.go(~K, ~Blk, ~enc, ~bxor, k, t, bxor(p, c), Con{c, acc})
46
47def cr.pcbc.dec.go(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, v: Blk, acc: List<&2, Blk>) -> List<&2, Blk>:
48  match bs:
49    case Nil{}:
50      Md.cr.blks.rev_onto(~Blk, acc, Nil{})
51    case Con{+c, t}:
52      +p = bxor(dec(k, c), v)
53      cr.pcbc.dec.go(~K, ~Blk, ~dec, ~bxor, k, t, bxor(p, c), Con{p, acc})
54
55# PCBC on blocks, from the chaining value v (the IV for the first call)
56def CrPcbc.encrypt_blocks(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, v: Blk, bs: List<&2, Blk>) -> List<&2, Blk>:
57  cr.pcbc.enc.go(~K, ~Blk, ~enc, ~bxor, k, bs, v, Nil{})
58
59def CrPcbc.decrypt_blocks(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, v: Blk, bs: List<&2, Blk>) -> List<&2, Blk>:
60  cr.pcbc.dec.go(~K, ~Blk, ~dec, ~bxor, k, bs, v, Nil{})
61
62def cr.pcbc.last(~Blk: Data, ~bxor: Blk -> Blk -> Blk, ps: List<&2, Blk>, cs: List<&2, Blk>, v: Blk) -> Blk:
63  match ps cs:
64    case Con{p, pt} Con{c, ct}:
65      cr.pcbc.last(~Blk, ~bxor, pt, ct, bxor(p, c))
66    case _ _:
67      v
68
69# The chaining value after the plaintext blocks ps encrypted to cs from v:
70# the next call's v, so a message may arrive in pieces of whole blocks
71def CrPcbc.next_iv(~Blk: Data, ~bxor: Blk -> Blk -> Blk, v: Blk, ps: List<&2, Blk>, cs: List<&2, Blk>) -> Blk:
72  cr.pcbc.last(~Blk, ~bxor, ps, cs, v)
73
74# PCBC on bytes: a message of whole blocks under a one-block IV
75# (CrBadIvLength, CrNotBlockMultiple otherwise)
76def CrPcbc.encrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
77  do Result<&2, &2, Cr.CrError, B.Octets>:
78    v : Blk <- Md.cr.iv(~Blk, ~blk_of, iv)
79    bs : List<&2, Blk> <- Md.CrModes.blocks_of(~Blk, ~bsize, ~blk_of, m)
80    return Md.CrModes.octets_of(~Blk, ~blk_to, CrPcbc.encrypt_blocks(~K, ~Blk, ~enc, ~bxor, k, v, bs))
81
82def CrPcbc.decrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
83  do Result<&2, &2, Cr.CrError, B.Octets>:
84    v : Blk <- Md.cr.iv(~Blk, ~blk_of, iv)
85    bs : List<&2, Blk> <- Md.CrModes.blocks_of(~Blk, ~bsize, ~blk_of, c)
86    return Md.CrModes.octets_of(~Blk, ~blk_to, CrPcbc.decrypt_blocks(~K, ~Blk, ~dec, ~bxor, k, v, bs))