Repository navigation
Expand file tree
/
Copy pathAEAD.lean
More file actions
196 lines (163 loc) · 8.66 KB
/
Copy pathAEAD.lean
File metadata and controls
196 lines (163 loc) · 8.66 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
import Commons.Definitions.Encryption
/-!
# Authenticated encryption
Banfi, §2.3.4 (printed pp. 18–21). The correlated encryption and decryption oracles
`⟦E_k, D_k⟧` of a symmetric-key encryption scheme, the transformations `ρ^cca`, `ρ^ptxt`,
`ρ^ctxt` and `ρ^ae`, and the security notions ind-cca, int-ptxt, int-ctxt and ae as
substitutions (Definitions 2.3.5–2.3.8), declared in the DSL on the interface `AE M C` with a
budget per port.
`ρ^ctxt` and `ρ^ae` act on `E_k` alone: they are converters from `AE M C` to `Encryption M C`,
whose decryption queries nothing inside, attached to the system `E_k` of `Encryption.Real`.
A notion is the pair of its systems `(X₀, X₁)` (Banfi, §2.3.1), independent of the substitution
relation; the predicate of the same name states it for the admitted distinguishers, `X₀ ≃[ε] X₁`.
Planned: nonces and associated data.
## Main definitions
* `AE M C`: the encryption and decryption interface
* `AE.Real scheme`: `⟦E_k, D_k⟧` for `k ← Gen`
* `AE.CCA`, `AE.PTXT`, `AE.CTXT`, `AE.Ideal`: the transformations `ρ^cca`, `ρ^ptxt`, `ρ^ctxt`
and `ρ^ae`, written so with `open Commons`
* `AE.INDCCA.systems`, `AE.INTPTXT.systems`, `AE.INTCTXT.systems`, `AE.Secure.systems`: the
systems of ind-cca, int-ptxt, int-ctxt and ae
* `AE.INDCCA`, `AE.INTPTXT`, `AE.INTCTXT`, `AE.Secure`: these notions for the distinguisher
advantage, within an error
-/
namespace Commons
open SystemAlgebra SystemAlgebra.DSL Probability
open scoped SystemAlgebra SystemAlgebra.DSL
interface AE(M C : Type) [Fintype M] [Fintype C]
enc(message : M) → C
dec(ciphertext : C) → Option M
/-- Banfi, printed p. 18, footnote 2: the first inserted message whose ciphertext is `c`. -/
def AE.replay {M C : Type} [DecidableEq C] (table : List (M × C)) (c : C) : Option M :=
(table.find? fun entry => entry.2 == c).map Prod.fst
/-- Banfi, printed p. 19: “if `m ∈ Q` then output `m`, otherwise output `⊥`”. -/
def AE.retain {M : Type} [DecidableEq M] (known : List M) (message : Option M) : Option M :=
message.bind fun m => if m ∈ known then some m else none
noncomputable section
variable {K M C : Type} [Fintype K] [Fintype M] [Fintype C]
-- `⟦E_k, D_k⟧` for `k ← Gen`: on `m`, output `c ← Enc_k(m)`; on `c`, output `Dec_k(c)`.
system AE.Real(scheme : SymmetricEncryption K M C) [DecidableEq K] [DecidableEq M] : AE M C
initialize
key ←$ scheme.gen
on enc(message : M) → C
encryptions ←$ scheme.encryptions
return encryptions (key, message)
on dec(ciphertext : C) → Option M
return scheme.dec key ciphertext
-- `ρ^cca`: encrypt a random message `m̃` instead of `m` and record `(m, c)`; on `c`, output its
-- first recorded message, otherwise forward `c`.
converter AE.CCA(M C : Type) [Fintype M] [Fintype C] [DecidableEq C] [Nonempty M] : AE M C
inside ae : AE M C
initialize
table ← ([] : List (M × C))
on enc(message : M) → C
replacement ←$ 𝒰[M]
ciphertext ← ae.enc(replacement)
table ← table ++ [(message, ciphertext)]
return ciphertext
on dec(ciphertext : C) → Option M
match AE.replay table ciphertext
| some message →
return some message
| none →
result ← ae.dec(ciphertext)
return result
-- `ρ^ptxt`: record each encrypted message; output a decryption only if its message was
-- recorded, otherwise `⊥`.
converter AE.PTXT(M C : Type) [Fintype M] [Fintype C] [DecidableEq M] : AE M C
inside ae : AE M C
initialize
queried ← ([] : List M)
on enc(message : M) → C
queried ← queried ++ [message]
ciphertext ← ae.enc(message)
return ciphertext
on dec(ciphertext : C) → Option M
message ← ae.dec(ciphertext)
return AE.retain queried message
-- `ρ^ctxt`: on `m`, output `c ← E_k(m)` and record `(m, c)`; on `c`, output its first recorded
-- message, otherwise `⊥`.
converter AE.CTXT(M C : Type) [Fintype M] [Fintype C] [DecidableEq C] : AE M C
inside encryption : Encryption M C
initialize
table ← ([] : List (M × C))
on enc(message : M) → C
ciphertext ← encryption.enc(message)
table ← table ++ [(message, ciphertext)]
return ciphertext
on dec(ciphertext : C) → Option M
return AE.replay table ciphertext
-- `ρ^ae`: on `m`, output `c ← E_k(m̃)` for a random message `m̃` and record `(m, c)`; on `c`,
-- output its first recorded message, otherwise `⊥`.
converter AE.Ideal(M C : Type) [Fintype M] [Fintype C] [DecidableEq C] [Nonempty M] : AE M C
inside encryption : Encryption M C
initialize
table ← ([] : List (M × C))
on enc(message : M) → C
replacement ←$ 𝒰[M]
ciphertext ← encryption.enc(replacement)
table ← table ++ [(message, ciphertext)]
return ciphertext
on dec(ciphertext : C) → Option M
return AE.replay table ciphertext
/-- `ρ^cca`, as Banfi writes it. -/
scoped notation "ρ^cca" => AE.CCA.perPort _ _
/-- `ρ^ptxt`, as Banfi writes it. -/
scoped notation "ρ^ptxt" => AE.PTXT.perPort _ _
/-- `ρ^ctxt`, as Banfi writes it. -/
scoped notation "ρ^ctxt" => AE.CTXT.perPort _ _
/-- `ρ^ae`, as Banfi writes it. -/
scoped notation "ρ^ae" => AE.Ideal.perPort _ _
/-- **The systems of ind-cca** (Banfi, Definition 2.3.5): `⟦E_k, D_k⟧` and `ρ^cca(⟦E_k, D_k⟧)`,
for `k ← Gen`, at the budget `q` per port. -/
def AE.INDCCA.systems [DecidableEq K] [DecidableEq M] [DecidableEq C] [Nonempty M]
(scheme : SymmetricEncryption K M C) (q : AE.Port → ℕ) :
TypedSystem (AE.perPort M C q) × TypedSystem (AE.perPort M C q) :=
(AE.Real.perPort scheme, AE.CCA.perPort M C • AE.Real.perPort scheme)
/-- **The systems of int-ptxt** (Banfi, Definition 2.3.6): `⟦E_k, D_k⟧` and
`ρ^ptxt(⟦E_k, D_k⟧)`, for `k ← Gen`, at the budget `q` per port. -/
def AE.INTPTXT.systems [DecidableEq K] [DecidableEq M] (scheme : SymmetricEncryption K M C)
(q : AE.Port → ℕ) :
TypedSystem (AE.perPort M C q) × TypedSystem (AE.perPort M C q) :=
(AE.Real.perPort scheme, AE.PTXT.perPort M C • AE.Real.perPort scheme)
/-- **The systems of int-ctxt** (Banfi, Definition 2.3.7): `⟦E_k, D_k⟧` and `ρ^ctxt(E_k)`, for
`k ← Gen`, at the budget `q` per port. -/
def AE.INTCTXT.systems [DecidableEq K] [DecidableEq M] [DecidableEq C]
(scheme : SymmetricEncryption K M C) (q : AE.Port → ℕ) :
TypedSystem (AE.perPort M C q) × TypedSystem (AE.perPort M C q) :=
(AE.Real.perPort scheme, AE.CTXT.perPort M C • Encryption.Real.perPort scheme)
/-- **The systems of ae** (Banfi, Definition 2.3.8): `⟦E_k, D_k⟧` and
`⟦E$_k, D^⊥⟧ = ρ^ae(E_k)`, for `k ← Gen`, at the budget `q` per port. -/
def AE.Secure.systems [DecidableEq K] [DecidableEq M] [DecidableEq C] [Nonempty M]
(scheme : SymmetricEncryption K M C) (q : AE.Port → ℕ) :
TypedSystem (AE.perPort M C q) × TypedSystem (AE.perPort M C q) :=
(AE.Real.perPort scheme, AE.Ideal.perPort M C • Encryption.Real.perPort scheme)
/-- **ind-cca** within `error`: against the admitted distinguishers, `⟦E_k, D_k⟧` substitutes
for `ρ^cca(⟦E_k, D_k⟧)`. -/
def AE.INDCCA [Interface.AdmissibleDistinguishers]
[DecidableEq K] [DecidableEq M] [DecidableEq C] [Nonempty M]
(scheme : SymmetricEncryption K M C) {q : AE.Port → ℕ}
(error : (AE.perPort M C q).inputDomain.DistinguisherBehavior → ENNReal) : Prop :=
(AE.INDCCA.systems scheme q).1 ≃[error] (AE.INDCCA.systems scheme q).2
/-- **int-ptxt** within `error`: against the admitted distinguishers, `⟦E_k, D_k⟧` substitutes
for `ρ^ptxt(⟦E_k, D_k⟧)`. -/
def AE.INTPTXT [Interface.AdmissibleDistinguishers]
[DecidableEq K] [DecidableEq M] (scheme : SymmetricEncryption K M C) {q : AE.Port → ℕ}
(error : (AE.perPort M C q).inputDomain.DistinguisherBehavior → ENNReal) : Prop :=
(AE.INTPTXT.systems scheme q).1 ≃[error] (AE.INTPTXT.systems scheme q).2
/-- **int-ctxt** within `error`: against the admitted distinguishers, `⟦E_k, D_k⟧` substitutes
for `ρ^ctxt(E_k)`. -/
def AE.INTCTXT [Interface.AdmissibleDistinguishers]
[DecidableEq K] [DecidableEq M] [DecidableEq C] (scheme : SymmetricEncryption K M C)
{q : AE.Port → ℕ} (error : (AE.perPort M C q).inputDomain.DistinguisherBehavior → ENNReal) :
Prop :=
(AE.INTCTXT.systems scheme q).1 ≃[error] (AE.INTCTXT.systems scheme q).2
/-- **ae** within `error`: against the admitted distinguishers, `⟦E_k, D_k⟧` substitutes for
`⟦E$_k, D^⊥⟧ = ρ^ae(E_k)`. -/
def AE.Secure [Interface.AdmissibleDistinguishers]
[DecidableEq K] [DecidableEq M] [DecidableEq C] [Nonempty M]
(scheme : SymmetricEncryption K M C) {q : AE.Port → ℕ}
(error : (AE.perPort M C q).inputDomain.DistinguisherBehavior → ENNReal) : Prop :=
(AE.Secure.systems scheme q).1 ≃[error] (AE.Secure.systems scheme q).2
end
end Commons