1	# Laws about CBC (cbc.bend), for every cipher given as the template
2	# arguments ~K, ~enc, ~dec. Laws that need decryption to undo encryption
3	# take that as a hypothesis, inv, at the law's key: for every list of blocks
4	# xs, CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs (each block encrypted and
5	# decrypted back is itself), so they hold for every cipher and key that
6	# satisfy it. The hypothesis is an ordinary one, used once (on the list of
7	# blocks the mode gives the cipher), which --verdict models; a cipher that
8	# proves dec(k, enc(k, b)) == b for every key and block as a law gives it
9	# for every list by induction (bend-osdev-cm-instances writes that out).
10	# Padded CBC's round trip is in LAWS_padded.bend.
11	import Base
12	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
13	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
14	import ./cbc.bend as C
15	
16	law cbc_blocks_round_trip:
17	  for ~K: Data
18	  for ~enc: K -> M.CmBlock -> M.CmBlock
19	  for ~dec: K -> M.CmBlock -> M.CmBlock
20	  for +k: K
21	  for inv: @xs: List<&2, M.CmBlock> -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}
22	  for iv: M.CmBlock
23	  for bs: List<&2, M.CmBlock>
24	  {C.Cbc.decrypt_blocks(~K, ~dec, k, iv, C.Cbc.encrypt_blocks(~K, ~enc, k, iv, bs)) == bs : List<&2, M.CmBlock>}
25	
26	# CBC on bytes: for every 16-byte IV and every message of whole blocks,
27	# encryption succeeds and decryption gives the message back
28	law cbc_round_trip:
29	  for ~K: Data
30	  for ~enc: K -> M.CmBlock -> M.CmBlock
31	  for ~dec: K -> M.CmBlock -> M.CmBlock
32	  for +k: K
33	  for inv: @xs: List<&2, M.CmBlock> -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}
34	  for +iv: B.Octets
35	  for +m: B.Octets
36	  for hi: {B.Octets.len(iv) == 16n : Nat}
37	  for hm: {Nat.mod(B.Octets.len(m), 16n) == 0n : Nat}
38	  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt(~K, ~enc, k, iv, m), c => C.Cbc.decrypt(~K, ~dec, k, iv, c)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}