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).
14	import Base
15	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
16	import ./crypto.bend as Cr
17	import ./modes.bend as Md
18	
19	# Structural forms (the proofs' reference)
20	
21	def 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	
29	def 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	
39	def 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	
47	def 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)
56	def 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	
59	def 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	
62	def 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
71	def 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)
76	def 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	
82	def 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))