PROOF_padded.bend

bend-osdev-cbc@0.1.0.0 · 141 lines · 17 definitions

1import Base
2import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
4import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
5import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P
6import bend-osdev-cbc@0.1.0.0/cbc.bend as C
7import bend-osdev-cbc@0.1.0.0/LAWS.bend as CML
8import bend-osdev-cbc@0.1.0.0/PROOF.bend as CMP
9import bend-osdev-pkcs7@0.1.0.0/LAWS.bend as PL
10import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PP
11import bend-osdev-cbc@0.1.0.0/LAWS_padded.bend as Laws
12
13# How the proof goes. Encryption pads m to M' (whole blocks:
14# pkcs7_pad_blocks) and encrypts M'; cbc_round_trip gives M' back from the
15# ciphertext c, and pkcs7_round_trip gives m back from M'. What is left is
16# decrypt_padded's first check, that c is not empty: if it were, decryption
17# would give the empty string, and unpadding the empty string is refused,
18# where unpadding M' gives m.
19
20# From bend-osdev-pkcs7's proofs (private there): False is not True, and
21# unpad with its two checks as arguments
22
23def pk.disc(b: Bool) -> Type:
24  match b:
25    case False{}:
26      Unit
27    case True{}:
28      Empty
29
30def pk.empty(h: {False{} == True{} : Bool}) -> Empty:
31  %h : pk.disc(_)
32  Unit{}
33
34def pk.absurd(-A: Type, h: {False{} == True{} : Bool}) -> A:
35  Empty.absurd(A, pk.empty(h))
36
37def pk.ug(+bs: Nat, +m: B.Octets, +n: Nat, +md: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
38  do Result<&2, &2, M.CmError, B.Octets>:
39    M.cm.check(Nat.is_lt(0n, n), M.CmTooShort{n})
40    M.cm.check(Nat.is_eq(md, 0n), M.CmNotBlockMultiple{n})
41    P.pkcs7.unpad.oct(bs, m, n)
42
43# Results
44
45def pd.disc(-A: Data, r: Result<&2, &2, M.CmError, A>) -> Type:
46  match r:
47    case Fail{e}:
48      Unit
49    case Done{x}:
50      Empty
51
52def pd.fd(-A: Data, +e: M.CmError, +x: A, h: {Fail{e} == Done{x} : Result<&2, &2, M.CmError, A>}) -> Empty:
53  %h : pd.disc(A, _)
54  Unit{}
55
56def pd.val(-A: Data, r: Result<&2, &2, M.CmError, A>, d: A) -> A:
57  match r:
58    case Fail{e}:
59      d
60    case Done{x}:
61      x
62
63def pd.inj(-A: Data, +a: A, +b: A, h: {Done{a} == Done{b} : Result<&2, &2, M.CmError, A>}) -> {a == b : A}:
64  Equal.cong(Result<&2, &2, M.CmError, A>, A, r => pd.val(A, r, a), Done{a}, Done{b}, h)
65
66# Naturals and lists
67
68def pd.ndisc(n: Nat) -> Type:
69  match n:
70    case 0n:
71      Empty
72    case 1n+p:
73      Unit
74
75def pd.nd(+p: Nat, h: {1n+p == 0n : Nat}) -> Empty:
76  %h : pd.ndisc(_)
77  Unit{}
78
79def pd.len0(+x: Nat) -> {Nat.is_lt(0n, x) == False{} : Bool} -> {x == 0n : Nat}:
80  match x:
81    case 0n:
82      h => {==}
83    case 1n+p:
84      h => pk.absurd({1n+p == 0n : Nat}, Equal.sym(Bool, True{}, False{}, h))
85
86def pd.nil(xs: List<&2, U32>) -> {B.len(xs) == 0n : Nat} -> {xs == Nil{} : List<&2, U32>}:
87  match xs:
88    case Nil{}:
89      h => {==}
90    case Con{x, t}:
91      h => Empty.absurd({Con{x, t} == Nil{} : List<&2, U32>}, pd.nd(B.len(t), h))
92
93# CBC decryption of no bytes, under any IV, is no bytes
94def 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}:
95  match r:
96    case Fail{e}:
97      h => Empty.absurd({B.Octets.len(mp) == 0n : Nat}, pd.fd(B.Octets, e, mp, h))
98    case Done{v}:
99      h => Equal.sym(Nat, B.Octets.len(B.Octets.of_list(Nil{})), B.Octets.len(mp), Equal.cong(B.Octets, Nat, o => B.Octets.len(o), B.Octets.of_list(Nil{}), mp, pd.inj(B.Octets, B.Octets.of_list(Nil{}), mp, h)))
100
101# decrypt_padded with its first check as an argument
102def 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>:
103  do Result<&2, &2, M.CmError, B.Octets>:
104    M.cm.check(ok, M.CmTooShort{B.Octets.len(c)})
105    padded : B.Octets <- C.Cbc.decrypt(~K, ~dec, k, iv, c)
106    P.Pkcs7.unpad(16n, padded)
107
108# an empty ciphertext cannot decrypt to M': its decryption is empty, and
109# unpadding the empty string is refused
110def 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>}:
111  # c is empty
112  +z = pd.len0(B.Octets.len(c))(eo)
113  +nl = pd.nil(B.Octets.to_list(c))(Equal.trans(Nat, B.len(B.Octets.to_list(c)), B.Octets.len(c), 0n, Equal.sym(Nat, B.Octets.len(c), B.len(B.Octets.to_list(c)), BL.octets_len_list(c)), z))
114  # so M' is empty
115  +e3 = Equal.trans(Result<&2, &2, M.CmError, B.Octets>, C.cbc.d1.fast(~K, ~dec, k, C.cbc.iv(iv), Nil{}), C.Cbc.decrypt(~K, ~dec, k, iv, c), Done{mp}, Equal.cong(List<&2, U32>, Result<&2, &2, M.CmError, B.Octets>, l => C.cbc.d1.fast(~K, ~dec, k, C.cbc.iv(iv), l), Nil{}, B.Octets.to_list(c), Equal.sym(List<&2, U32>, B.Octets.to_list(c), Nil{}, nl)), e1)
116  +z2 = pd.e0(~K, ~dec, k, C.cbc.iv(iv), mp)(e3)
117  # and unpadding it is refused
118  +e4 = Equal.trans(Result<&2, &2, M.CmError, B.Octets>, Fail{M.CmTooShort{0n}}, P.Pkcs7.unpad(16n, mp), Done{m}, Equal.cong(Nat, Result<&2, &2, M.CmError, B.Octets>, n => pk.ug(16n, mp, n, Nat.mod(n, 16n)), 0n, B.Octets.len(mp), Equal.sym(Nat, B.Octets.len(mp), 0n, z2)), e2)
119  Empty.absurd({C.Cbc.decrypt_padded(~K, ~dec, k, iv, c) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, pd.fd(B.Octets, M.CmTooShort{0n}, m, e4))
120
121# from the ciphertext c, decrypting gives M' and unpadding M' gives m
122def 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>}:
123  match ok:
124    case True{}:
125      eo => e1 => %Equal.sym(Bool, Nat.is_lt(0n, B.Octets.len(c)), True{}, eo) : {pd.dpx(~K, ~dec, k, iv, c, _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
126        %Equal.sym(Result<&2, &2, M.CmError, B.Octets>, C.Cbc.decrypt(~K, ~dec, k, iv, c), Done{mp}, e1) : {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, _, padded => P.Pkcs7.unpad(16n, padded)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
127        e2
128    case False{}:
129      eo => e1 => pd.dc0(~K, ~dec, k, iv, mp, m, e2, c, eo, e1)
130
131def 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>}:
132  match r:
133    case Fail{e}:
134      e1 => Empty.absurd({Fail{e} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, pd.fd(B.Octets, e, mp, e1))
135    case Done{+c}:
136      e1 => pd.dc(~K, ~dec, k, iv, mp, m, e2, c, Nat.is_lt(0n, B.Octets.len(c)))({==})(e1)
137
138def Laws.cbc_padded_round_trip(K, enc, dec, k, inv, iv, m, hi):
139  # the padded message is whole blocks
140  +hm = pd.inj(Nat, Nat.mod(B.Octets.len(P.pkcs7.pad.oct(16n, m)), 16n), 0n, PL.pkcs7_pad_blocks(16n, m))
141  pd.go(~K, ~dec, k, iv, P.pkcs7.pad.oct(16n, m), m, PL.pkcs7_round_trip(16n, m), C.Cbc.encrypt(~K, ~enc, k, iv, P.pkcs7.pad.oct(16n, m)))(CML.cbc_round_trip(~K, ~enc, ~dec, k, inv, iv, P.pkcs7.pad.oct(16n, m), hi, hm))