-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathprivate-authentication.html
More file actions
323 lines (273 loc) · 83.3 KB
/
private-authentication.html
File metadata and controls
323 lines (273 loc) · 83.3 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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
<!DOCTYPE html>
<html lang="en-US">
<head>
<meta charset="UTF-8">
<title>Squirrel Prover - Squirrel Prover</title>
<link rel="stylesheet" href="style.css">
</head>
<body onkeydown="key(event)">
<span style="display: none;"><span class="squirrel-step" id="step0">
<span class="input-line" id="in0">set postQuantumSound=true.</span>
<span class="output-line" id="out0"></span>
<span class="com-line" id="com0"><h1 id="private-authentication">PRIVATE AUTHENTICATION</h1>
<p>The Private Authentication protocol as described in [F] involves an initiator A and a responder B.</p>
<p>The initiator A sends a message <code>enc(<pkA,n0>,r0,pkB)</code> to the responder B, where <code>pkA</code> (respectively <code>pkB</code>) is the public key of A (respectively B). The responder B checks that the first projection of the decryption of the received message is equal to <code>pkA</code> and that the second projection of the decryption of the received message has a correct length. In that case, B sends back <code>enc(<n0,n>,r,pkA)</code>.</p>
<p>The protocol is as follows:</p>
<ul>
<li>A -> B : enc(<pkA,n0>,r0,pkB)</li>
<li>B -> A : enc(<n0,n>,r,pkA)</li>
</ul>
<p>This is a “light” model without the last check of A.</p>
<p>In this file, we prove anonymity, <em>i.e.</em> that an attacker cannot tell whether a session is initiated by an identity A or by an identity Abis.</p>
<p>[F] G. Bana and H. Comon-Lundh. A computationally complete symbolic attacker for equivalence properties. In 2014 ACM Conference on Computer and Communications Security, CCS ’14, pages 609–620. ACM, 2014</p>
<hr />
<p>When this option is set to <code>true</code>, Squirrel checks whether each tactic invoked for the proof is also sound for quantum attackers.</p>
</span>
</span>
<span class="squirrel-step" id="step1">
<span class="input-line" id="in1">channel cA<br>channel cAbis<br>channel cB<br>channel cO<br><br>aenc enc,dec,pk<br><br>name kA : message<br>name kAbis : message<br>name kB : message<br><br>name n0 : index -> message<br>name r0 : index -> message<br>name n0bis : index -> message<br>name r0bis : index -> message<br><br>name n : index -> message<br>name r : index -> message.</span>
<span class="output-line" id="out1"></span>
<span class="com-line" id="com1"><p>We first declare the communication channels, the function symbols for the public encryption scheme as well as the several names used in the protocol’s messages.</p>
</span>
</span>
<span class="squirrel-step" id="step2">
<span class="input-line" id="in2">abstract (++) : message -> message -> message.</span>
<span class="output-line" id="out2"></span>
<span class="com-line" id="com2"><p>We also declare a public function symbol <code>plus</code>, which we will use to model the addition of lengths of messages.</p>
</span>
</span>
<span class="squirrel-step" id="step3">
<span class="input-line" id="in3">process A(i:index) =<br> out(cA, enc(<pk(kA),n0(i)>,r0(i),pk(kB))).</span>
<span class="output-line" id="out3"></span>
<span class="com-line" id="com3"><p>The initiator A is indexed by <code>i</code> to represent an unbounded number of sessions and is defined by a single output.</p>
</span>
</span>
<span class="squirrel-step" id="step4">
<span class="input-line" id="in4">process Abis(i:index) =<br> out(cAbis, enc(<pk(kAbis),n0bis(i)>,r0bis(i),pk(kB))).</span>
<span class="output-line" id="out4"></span>
<span class="com-line" id="com4"><p>We define a similar process for the initiator Abis.</p>
</span>
</span>
<span class="squirrel-step" id="step5">
<span class="input-line" id="in5">process B(j:index) =<br> in(cB, mess);<br> let dmess = dec(mess, kB) in<br> out(cB,<br> enc(<br> (if fst(dmess) = diff(pk(kA),pk(kAbis)) && len(snd(dmess)) = len(n(j)) then<br> <snd(dmess), n(j)><br> else<br> <n(j), n(j)>),<br> r(j), pk(diff(kA,kAbis)))<br> ).</span>
<span class="output-line" id="out5"></span>
<span class="com-line" id="com5"><p>The responder B is indexed by <code>j</code> to represent an unbounded number of sessions.</p>
<p>In order to express anonymity using an equivalence property, we model two systems using the <code>diff</code> operator. On the left side, the key <code>kA</code> is used while the right side uses the key <code>kAbis</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step6">
<span class="input-line" id="in6">system O:<br> out(cO,<<pk(kA),pk(kAbis)>,pk(kB)>);<br> (!_i A(i) | !_ibis Abis(ibis) | !_j B(j)).</span>
<span class="output-line" id="out6">System before processing:<br> <br> O:<br> <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cO</span>,pair(pair(pk(kA),pk(kAbis)),pk(kB)));<br> (!_i <span class="pn" style="font-weight:bold; color: #0000AA">A</span> i) | ((!_ibis <span class="pn" style="font-weight:bold; color: #0000AA">Abis</span> ibis) | (!_j <span class="pn" style="font-weight:bold; color: #0000AA">B</span> j))<br><br>System after processing:<br> <br> O:<br> <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cO</span>,pair(pair(pk(kA),pk(kAbis)),pk(kB)));<br> (!_i A: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cA</span>,enc(pair(pk(kA),n0(i)),r0(i),pk(kB))); <span class="pn" style="font-weight:bold; color: #0000AA">null</span>) |<br> ((!_ibis<br> Abis:<br> <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cAbis</span>,enc(pair(pk(kAbis),n0bis(ibis)),r0bis(ibis),pk(kB))); <span class="pn" style="font-weight:bold; color: #0000AA">null</span>) |<br> (!_j<br> <span class="pio" style="font-weight: bold">in</span>(<span class="pc">cB</span>,<span class="pv" style="font-weight: bold; color: #AA00AA">mess</span>);<br> <span class="pk" style="font-weight: bold">let</span> <span class="pv" style="font-weight: bold; color: #AA00AA">dmess</span> = dec(mess,kB) <span class="pk" style="font-weight: bold">in</span><br> B:<br> <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cB</span>,<br> enc(<span>if</span><br> ((fst(dmess(j)) = <span>diff</span>(pk(kA),pk(kAbis))) &&<br> (len(snd(dmess(j))) = len(n(j))))<br> <span>then</span> pair(snd(dmess(j)),n(j)) <span>else</span> pair(n(j),n(j)),r(j),<br> pk(<span>diff</span>(kA,kAbis)))); <span class="pn" style="font-weight:bold; color: #0000AA">null</span>))<br><br>System default registered with actions (init,O,A,Abis,B).<br></span>
<span class="com-line" id="com6"><p>The protocol is finally defined by a system where an unbounded number of sessions for A, Abis and B play in parallel, after having outputted the public keys of A, Abis and B.</p>
</span>
</span>
<span class="squirrel-step" id="step7">
<span class="input-line" id="in7">include Basic.</span>
<span class="output-line" id="out7">Goal eq_sym :<br> (x = y) = (y = x)<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(x = y) = (y = x)<br><br>[> Line 11: by (rewrite ...) <br>[goal> Goal eq_sym is proved <br>Exiting proof mode.<br><br><br>Goal neq_sym :<br> (x <> y) = (y <> x)<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(x <> y) = (y <> x)<br><br>[> Line 14: by (rewrite ...) <br>[goal> Goal neq_sym is proved <br>Exiting proof mode.<br><br><br>Goal eq_refl :<br> (x = x) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(x = x) = true<br><br>[> Line 18: by (rewrite ...) <br>[goal> Goal eq_refl is proved <br>Exiting proof mode.<br><br><br>Goal false_true :<br> (false = true) = false<br>[goal> Focused goal (1/1):<br>System: any<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(false = true) = false<br><br>[> Line 30: by (rewrite ...) <br>[goal> Goal false_true is proved <br>Exiting proof mode.<br><br><br>Goal eq_true :<br> (b = true) = b<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(b = true) = b<br><br>[> Line 35: by (case b) <br>[goal> Goal eq_true is proved <br>Exiting proof mode.<br><br><br>Goal eq_true2 :<br> (true = b) = b<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(true = b) = b<br><br>[> Line 39: by (case b) <br>[goal> Goal eq_true2 is proved <br>Exiting proof mode.<br><br><br>Goal not_not :<br> not(not(b)) = b<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not(not(b)) = b<br><br>[> Line 54: by (case b) <br>[goal> Goal not_not is proved <br>Exiting proof mode.<br><br><br>Goal not_eq :<br> not(x = y) = (x <> y)<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not(x = y) = (x <> y)<br><br>[> Line 60: by (rewrite ...) <br>[goal> Goal not_eq is proved <br>Exiting proof mode.<br><br><br>Goal not_neq :<br> not(x <> y) = (x = y)<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not(x <> y) = (x = y)<br><br>[> Line 66: by (rewrite ...) <br>[goal> Goal not_neq is proved <br>Exiting proof mode.<br><br><br>Goal not_eqfalse :<br> (b = false) = not(b)<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(b = false) = not(b)<br><br>[> Line 72: by (case b) <br>[goal> Goal not_eqfalse is proved <br>Exiting proof mode.<br><br><br>Goal eq_false :<br> ((x = y) = false) = (x <> y)<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>((x = y) = false) = (x <> y)<br><br>[> Line 80: (rewrite ...) <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>((x = y) = false) = not(x = y)<br><br>[> Line 80: ((case (x = y));(intro _)) <br>[goal> Focused goal (1/2):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br>_: x = y<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(true = false) = not(true)<br><br>[> Line 80: simpl <br>[goal> Focused goal (1/2):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br>_: x = y<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>true<br><br>[> Line 80: auto <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br>_: not(x = y)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(false = false) = not(false)<br><br>[> Line 81: by (rewrite ...) <br>[goal> Goal eq_false is proved <br>Exiting proof mode.<br><br><br>Goal and_true_r :<br> (b && true) = b<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(b && true) = b<br><br>[> Line 94: by (rewrite ... ...) <br>[goal> Goal and_true_r is proved <br>Exiting proof mode.<br><br><br>Goal and_false_r :<br> (b && false) = false<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(b && false) = false<br><br>[> Line 101: by (rewrite ... ...) <br>[goal> Goal and_false_r is proved <br>Exiting proof mode.<br><br><br>Goal or_false_r :<br> (b || false) = b<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(b || false) = b<br><br>[> Line 112: by (rewrite ... ...) <br>[goal> Goal or_false_r is proved <br>Exiting proof mode.<br><br><br>Goal or_true_r :<br> (b || true) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(b || true) = true<br><br>[> Line 119: by (rewrite ... ...) <br>[goal> Goal or_true_r is proved <br>Exiting proof mode.<br><br><br>Goal not_and :<br> not((a && b)) = (not(a) || not(b))<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: a,b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not((a && b)) = (not(a) || not(b))<br><br>[> Line 128: (rewrite ...) <br>[goal> Focused goal (1/1):<br>System: any<br>Variables: a,b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not((a && b)) <=> not(a) || not(b)<br><br>[> Line 129: (((case a);(case b));(intro //=)) <br>[goal> Goal not_and is proved <br>Exiting proof mode.<br><br><br>Goal not_or :<br> not((a || b)) = (not(a) && not(b))<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: a,b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not((a || b)) = (not(a) && not(b))<br><br>[> Line 134: (rewrite ...) <br>[goal> Focused goal (1/1):<br>System: any<br>Variables: a,b:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not((a || b)) <=> not(a) && not(b)<br><br>[> Line 135: (((case a);(case b));(intro //=)) <br>[goal> Goal not_or is proved <br>Exiting proof mode.<br><br><br>Goal if_true :<br> b => if b then x else y = x<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>b => if b then x else y = x<br><br>[> Line 144: (intro *) <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br>H: b<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>if b then x else y = x<br><br>[> Line 145: (case <span>if</span> b <span>then</span> x <span>else</span> y) <br>[goal> Focused goal (1/2):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br>H: b<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>b && if b then x else y = x => x = x<br><br>[> Line 146: auto <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br>H: b<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not(b) && if b then x else y = y => y = x<br><br>[> Line 147: (intro [HH _]) <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br>H: b<br>HH: not(b)<br>_: if b then x else y = y<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>y = x<br><br>[> Line 147: by (have ... as ) <br>[goal> Goal if_true is proved <br>Exiting proof mode.<br><br><br>Goal if_true0 :<br> if true then x else y = x<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>if true then x else y = x<br><br>[> Line 153: by (rewrite ...) <br>[goal> Goal if_true0 is proved <br>Exiting proof mode.<br><br><br>Goal if_false :<br> not(b) => if b then x else y = y<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not(b) => if b then x else y = y<br><br>[> Line 160: ((intro *);(case <span>if</span> b <span>then</span> x <span>else</span> y)) <br>[goal> Focused goal (1/2):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br>H: not(b)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>b && if b then x else y = x => x = y<br><br>[> Line 161: (intro [HH _]) <br>[goal> Focused goal (1/2):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br>H: not(b)<br>HH: b<br>_: if b then x else y = x<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>x = y<br><br>[> Line 161: by (have ... as ) <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x,y:'a<br>H: not(b)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not(b) && if b then x else y = y => y = y<br><br>[> Line 162: auto <br>[goal> Goal if_false is proved <br>Exiting proof mode.<br><br><br>Goal if_false0 :<br> if false then x else y = y<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>if false then x else y = y<br><br>[> Line 168: by (rewrite ...) <br>[goal> Goal if_false0 is proved <br>Exiting proof mode.<br><br><br>Goal if_then_then :<br> if b then if b' then x else y else y = if (b && b') then x else y<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>if b then if b' then x else y else y = if (b && b') then x else y<br><br>[> Line 175: by ((case b);(case b')) <br>[goal> Goal if_then_then is proved <br>Exiting proof mode.<br><br><br>Goal if_then_implies :<br> if b then if b' then x else y else z =<br> if b then if (b => b') then x else y else z<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>if b then if b' then x else y else z =<br>if b then if (b => b') then x else y else z<br><br>[> Line 182: ((case b);<br> ((intro H);((case b');((intro H');(simpl;(try auto))))))<br><br>[goal> Focused goal (1/2):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br>H: b<br>H': b'<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>x = if (true => true) then x else y<br><br>[> Line 183: by (rewrite ...) <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br>H: b<br>H': not(b')<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>y = if (true => false) then x else y<br><br>[> Line 184: (rewrite ...) <br>[goal> Focused goal (1/2):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br>H: b<br>H': not(b')<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>not((true => false))<br><br>[> Line 185: ((intro Habs);by (have ... as )) <br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br>H: b<br>H': not(b')<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>y = y<br><br>[> Line 186: auto <br>[goal> Goal if_then_implies is proved <br>Exiting proof mode.<br><br><br>Goal if_same :<br> if b then x else x = x<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b:bool,x:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>if b then x else x = x<br><br>[> Line 192: by (case b) <br>[goal> Goal if_same is proved <br>Exiting proof mode.<br><br><br>Goal if_then :<br> b = b' => if b then if b' then x else y else z = if b then x else z<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>b = b' => if b then if b' then x else y else z = if b then x else z<br><br>[> Line 201: by ((intro ->);(case b')) <br>[goal> Goal if_then is proved <br>Exiting proof mode.<br><br><br>Goal if_else :<br> b = b' => if b then x else if b' then y else z = if b then x else z<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>b = b' => if b then x else if b' then y else z = if b then x else z<br><br>[> Line 210: by ((intro ->);(case b')) <br>[goal> Goal if_else is proved <br>Exiting proof mode.<br><br><br>Goal if_then_not :<br> b = not(b') => if b then if b' then x else y else z = if b then y else z<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>b = not(b') => if b then if b' then x else y else z = if b then y else z<br><br>[> Line 219: by ((intro ->);(case b')) <br>[goal> Goal if_then_not is proved <br>Exiting proof mode.<br><br><br>Goal if_else_not :<br> b = not(b') => if b then x else if b' then y else z = if b then x else y<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br>Variables: b,b':bool,x,y,z:'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>b = not(b') => if b then x else if b' then y else z = if b then x else y<br><br>[> Line 228: by ((intro ->);(case b')) <br>[goal> Goal if_else_not is proved <br>Exiting proof mode.<br><br><br>Goal fst_pair :<br> <span class="gf" style="font-weight: bold">fst</span>(<x,y>) = x<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: x,y:message<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gf" style="font-weight: bold">fst</span>(<x,y>) = x<br><br>[> Line 236: auto <br>[goal> Goal fst_pair is proved <br>Exiting proof mode.<br><br><br>Goal snd_pair :<br> <span class="gf" style="font-weight: bold">snd</span>(<x,y>) = y<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: x,y:message<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gf" style="font-weight: bold">snd</span>(<x,y>) = y<br><br>[> Line 240: auto <br>[goal> Goal snd_pair is proved <br>Exiting proof mode.<br><br><br>Goal iff_refl :<br> (x <=> x) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: x:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(x <=> x) = true<br><br>[> Line 248: by (rewrite ...) <br>[goal> Goal iff_refl is proved <br>Exiting proof mode.<br><br><br>Goal iff_sym :<br> (x <=> y) = (y <=> x)<br>[goal> Focused goal (1/1):<br>System: any<br>Variables: x,y:bool<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(x <=> y) = (y <=> x)<br><br>[> Line 254: by (rewrite ...) <br>[goal> Goal iff_sym is proved <br>Exiting proof mode.<br><br><br>Goal true_iff_false :<br> (true <=> false) = false<br>[goal> Focused goal (1/1):<br>System: any<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(true <=> false) = false<br><br>[> Line 259: by (rewrite ...) <br>[goal> Goal true_iff_false is proved <br>Exiting proof mode.<br><br><br>Goal false_iff_true :<br> (false <=> true) = false<br>[goal> Focused goal (1/1):<br>System: any<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(false <=> true) = false<br><br>[> Line 265: by (rewrite ...) <br>[goal> Goal false_iff_true is proved <br>Exiting proof mode.<br><br><br>Goal exists_false1 :<br> (exists (a:'a), false) = false<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(exists (a:'a), false) = false<br><br>[> Line 277: by (rewrite ...) <br>[goal> Goal exists_false1 is proved <br>Exiting proof mode.<br><br><br>Goal exists_false2 :<br> (exists (a:'a,b:'b), false) = false<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(exists (a:'a,b:'b), false) = false<br><br>[> Line 281: by (rewrite ...) <br>[goal> Goal exists_false2 is proved <br>Exiting proof mode.<br><br><br>Goal exists_false3 :<br> (exists (a:'a,b:'b,c:'c), false) = false<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(exists (a:'a,b:'b,c:'c), false) = false<br><br>[> Line 285: by (rewrite ...) <br>[goal> Goal exists_false3 is proved <br>Exiting proof mode.<br><br><br>Goal exists_false4 :<br> (exists (a:'a,b:'b,c:'c,d:'d), false) = false<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c, 'd<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(exists (a:'a,b:'b,c:'c,d:'d), false) = false<br><br>[> Line 289: by (rewrite ...) <br>[goal> Goal exists_false4 is proved <br>Exiting proof mode.<br><br><br>Goal exists_false5 :<br> (exists (a:'a,b:'b,c:'c,d:'d,e:'e), false) = false<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c, 'd, 'e<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(exists (a:'a,b:'b,c:'c,d:'d,e:'e), false) = false<br><br>[> Line 293: by (rewrite ...) <br>[goal> Goal exists_false5 is proved <br>Exiting proof mode.<br><br><br>Goal exists_false6 :<br> (exists (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), false) = false<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c, 'd, 'e, 'f<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(exists (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), false) = false<br><br>[> Line 297: by (rewrite ...) <br>[goal> Goal exists_false6 is proved <br>Exiting proof mode.<br><br><br>Goal forall_true1 :<br> (forall (a:'a), true) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (a:'a), true) = true<br><br>[> Line 307: auto <br>[goal> Goal forall_true1 is proved <br>Exiting proof mode.<br><br><br>Goal forall_true2 :<br> (forall (a:'a,b:'b), true) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (a:'a,b:'b), true) = true<br><br>[> Line 311: auto <br>[goal> Goal forall_true2 is proved <br>Exiting proof mode.<br><br><br>Goal forall_true3 :<br> (forall (a:'a,b:'b,c:'c), true) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (a:'a,b:'b,c:'c), true) = true<br><br>[> Line 315: auto <br>[goal> Goal forall_true3 is proved <br>Exiting proof mode.<br><br><br>Goal forall_true4 :<br> (forall (a:'a,b:'b,c:'c,d:'d), true) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c, 'd<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (a:'a,b:'b,c:'c,d:'d), true) = true<br><br>[> Line 319: auto <br>[goal> Goal forall_true4 is proved <br>Exiting proof mode.<br><br><br>Goal forall_true5 :<br> (forall (a:'a,b:'b,c:'c,d:'d,e:'e), true) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c, 'd, 'e<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (a:'a,b:'b,c:'c,d:'d,e:'e), true) = true<br><br>[> Line 323: auto <br>[goal> Goal forall_true5 is proved <br>Exiting proof mode.<br><br><br>Goal forall_true6 :<br> (forall (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), true) = true<br>[goal> Focused goal (1/1):<br>System: any<br>Type variables: 'a, 'b, 'c, 'd, 'e, 'f<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), true) = true<br><br>[> Line 327: auto <br>[goal> Goal forall_true6 is proved <br>Exiting proof mode.<br><br><br>[warning> loaded: Basic.sp <]<br></span>
<span class="com-line" id="com7"><p>This axiom states that the length of a pair is equal to the sum of the lengths of each component of the pair.</p>
</span>
</span>
<span class="squirrel-step" id="step8">
<span class="input-line" id="in8"><br><br>axiom length_pair (m1:message, m2:message): len(<m1,m2>) = len(m1) ++ len(m2).</span>
<span class="output-line" id="out8"></span>
</span>
<span class="squirrel-step" id="step9">
<span class="input-line" id="in9">goal if_len (b : boolean, y,z:message):<br> len(if b then y else z) =<br> (if b then len(y) else len(z)).</span>
<span class="output-line" id="out9">Goal if_len :<br> <span class="gf" style="font-weight: bold">len</span>(if b then y else z) = if b then <span class="gf" style="font-weight: bold">len</span>(y) else <span class="gf" style="font-weight: bold">len</span>(z)<br></span>
<span class="com-line" id="com9"><p>Helper lemma for pushing conditionals under the <code>len(_)</code> function.</p>
</span>
</span>
<span class="squirrel-step" id="step10">
<span class="input-line" id="in10"><br>Proof.</span>
<span class="output-line" id="out10">[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: b:bool,y,z:message<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gf" style="font-weight: bold">len</span>(if b then y else z) = if b then <span class="gf" style="font-weight: bold">len</span>(y) else <span class="gf" style="font-weight: bold">len</span>(z)<br><br></span>
</span>
<span class="squirrel-step" id="step11">
<span class="input-line" id="in11"><br> by case b.</span>
<span class="output-line" id="out11">[> Line 124: by (case b) <br>[goal> Goal if_len is proved <br></span>
</span>
<span class="squirrel-step" id="step12">
<span class="input-line" id="in12"><br>Qed.</span>
<span class="output-line" id="out12">Exiting proof mode.<br><br><br></span>
</span>
<span class="squirrel-step" id="step13">
<span class="input-line" id="in13"><br><br>(* Helper lemma *)<br>goal if_same_branch (x,y,z : message, b : boolean):<br> (b => y = x) =><br> (not b => z = x) =><br> (if b then y else z) = x.</span>
<span class="output-line" id="out13">Goal if_same_branch :<br> (b => y = x) => (not(b) => z = x) => if b then y else z = x<br></span>
</span>
<span class="squirrel-step" id="step14">
<span class="input-line" id="in14"><br>Proof.</span>
<span class="output-line" id="out14">[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: b:bool,x,y,z:message<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(b => y = x) => (not(b) => z = x) => if b then y else z = x<br><br></span>
</span>
<span class="squirrel-step" id="step15">
<span class="input-line" id="in15"><br> by intro *; case b.</span>
<span class="output-line" id="out15">[> Line 133: by ((intro *);(case b)) <br>[goal> Goal if_same_branch is proved <br></span>
</span>
<span class="squirrel-step" id="step16">
<span class="input-line" id="in16"><br>Qed.</span>
<span class="output-line" id="out16">Exiting proof mode.<br><br><br></span>
</span>
<span class="squirrel-step" id="step17">
<span class="input-line" id="in17">equiv anonymity.</span>
<span class="output-line" id="out17">Goal anonymity :<br> forall t:timestamp, equiv(<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@t)<br></span>
<span class="com-line" id="com17"><p>The anonymity property is expressed as an equivalence between the left side (the one using <code>kA</code> and the right side (the one using <code>kAbis</code>) of the system. This property is expressed by the logic formula <code>forall t:timestamp, frame@t</code> where <code>frame@t</code> is a bi-frame.</p>
</span>
</span>
<span class="squirrel-step" id="step18">
<span class="input-line" id="in18">Proof.</span>
<span class="output-line" id="out18">[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: t:timestamp<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(t)]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@t<br><br><br></span>
<span class="com-line" id="com18"><p>The high-level idea of the proof is as follows: we show that the message outputted by the role B does not give any element to the attacker to distinguish the left side from the right side, relying on the fact that encryption satisfies key privacy and IND-CCA1 assumptions.</p>
</span>
</span>
<span class="squirrel-step" id="step19">
<span class="input-line" id="in19"> enrich pk(kA), pk(kAbis), pk(kB).</span>
<span class="output-line" id="out19">[> Line 155: (enrich pk(kA), pk(kAbis), pk(kB)) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: t:timestamp<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(t)]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@t<br><br><br></span>
<span class="com-line" id="com19"><p>We start by adding to the frame the two public keys <code>pk(kA)</code>, <code>pk(kAbis)</code> and <code>pk(kB)</code> since any execution starts by the action <code>O</code> outputting them. This allows to simplify some cases in the proof below.</p>
</span>
</span>
<span class="squirrel-step" id="step20">
<span class="input-line" id="in20"><br><br> induction t.</span>
<span class="output-line" id="out20">[> Line 157: (induction t) <br>[goal> Focused goal (1/5):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">init</span>)]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">init</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step21">
<span class="input-line" id="in21"> auto.</span>
<span class="output-line" id="out21">[> Line 163: auto <br>[goal> Focused goal (1/4):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">O</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">O</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">O</span><br><br><br></span>
<span class="com-line" id="com21"><p><strong>Case where t = 0:</strong><br />
This case is trivial thanks to the addition of <code>pk(kA)</code>, <code>pk(kAbis)</code> and <code>pk(kB)</code> in the frame.</p>
</span>
</span>
<span class="squirrel-step" id="step22">
<span class="input-line" id="in22"><br><br> rewrite /*.</span>
<span class="output-line" id="out22">[> Line 165: (rewrite ...) <br>[goal> Focused goal (1/4):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">O</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">O</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">O</span>),<br> <<span class="gf" style="font-weight: bold">of_bool</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">O</span>) && true),<br> if (<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">O</span>) && true) then <<<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>),<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)>>><br><br><br></span>
</span>
<span class="squirrel-step" id="step23">
<span class="input-line" id="in23"><br> by apply IH.</span>
<span class="output-line" id="out23">[> Line 166: by (apply ... ) <br>[goal> Focused goal (1/3):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: i:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">A(i)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">A(i)</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step24">
<span class="input-line" id="in24"> expandall.</span>
<span class="output-line" id="out24">[> Line 178: expandall <br>[goal> Focused goal (1/3):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: i:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">A(i)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>),<br> <<span class="gf" style="font-weight: bold">of_bool</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>) && true),<br> if (<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>) && true) then <span class="gf" style="font-weight: bold">enc</span>(<<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>),<span class="gn" style="color: #AA5500">n0</span>(i)>,<span class="gn" style="color: #AA5500">r0</span>(i),<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>))>><br><br><br></span>
<span class="com-line" id="com24"><p><strong>Case where t = A(i):</strong><br />
The output of this action is the same on both sides. We show that this output can be removed from the frame so that we can conclude by induction hypothesis. We start by expanding all macros and splitting the pairs and function applications. We are then left with the two names <code>n0(i)</code> and <code>r0(i)</code> used for the encryption. These names are fresh (<em>i.e.</em> does not appear anywhere else in the frame) so we are able to remove them with the <code>fresh</code> tactic.</p>
</span>
</span>
<span class="squirrel-step" id="step25">
<span class="input-line" id="in25"><br> fa 3; fa 4; fa 4; fa 4; fa 4.</span>
<span class="output-line" id="out25">[> Line 179: ((fa 3);((fa 4);((fa 4);((fa 4);(fa 4))))) <br>[goal> Focused goal (1/3):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: i:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">A(i)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>)<br>4: <span class="gn" style="color: #AA5500">n0</span>(i)<br>5: <span class="gn" style="color: #AA5500">r0</span>(i)<br><br><br></span>
</span>
<span class="squirrel-step" id="step26">
<span class="input-line" id="in26"><br> fresh 5; rewrite if_true //.</span>
<span class="output-line" id="out26">[> Line 180: ((fresh 5);(rewrite ... //)) <br>[goal> Focused goal (1/3):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: i:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">A(i)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>)<br>4: <span class="gn" style="color: #AA5500">n0</span>(i)<br><br><br></span>
</span>
<span class="squirrel-step" id="step27">
<span class="input-line" id="in27"><br> by fresh 4; rewrite if_true //.</span>
<span class="output-line" id="out27">[> Line 181: by ((fresh 4);(rewrite ... //)) <br>[goal> Focused goal (1/2):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: ibis:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">Abis(ibis)</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step28">
<span class="input-line" id="in28"> expandall.</span>
<span class="output-line" id="out28">[> Line 186: expandall <br>[goal> Focused goal (1/2):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: ibis:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>),<br> <<span class="gf" style="font-weight: bold">of_bool</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>) && true),<br> if (<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>) && true) then<br> <span class="gf" style="font-weight: bold">enc</span>(<<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>),<span class="gn" style="color: #AA5500">n0bis</span>(ibis)>,<span class="gn" style="color: #AA5500">r0bis</span>(ibis),<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>))>><br><br><br></span>
<span class="com-line" id="com28"><p><strong>Case where t = Abis(ibis):</strong><br />
Similar to the previous case.</p>
</span>
</span>
<span class="squirrel-step" id="step29">
<span class="input-line" id="in29"><br> fa 3; fa 4; fa 4; fa 4; fa 4.</span>
<span class="output-line" id="out29">[> Line 187: ((fa 3);((fa 4);((fa 4);((fa 4);(fa 4))))) <br>[goal> Focused goal (1/2):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: ibis:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>)<br>4: <span class="gn" style="color: #AA5500">n0bis</span>(ibis)<br>5: <span class="gn" style="color: #AA5500">r0bis</span>(ibis)<br><br><br></span>
</span>
<span class="squirrel-step" id="step30">
<span class="input-line" id="in30"><br> fresh 5; rewrite if_true //.</span>
<span class="output-line" id="out30">[> Line 188: ((fresh 5);(rewrite ... //)) <br>[goal> Focused goal (1/2):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: ibis:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">Abis(ibis)</span>)<br>4: <span class="gn" style="color: #AA5500">n0bis</span>(ibis)<br><br><br></span>
</span>
<span class="squirrel-step" id="step31">
<span class="input-line" id="in31"><br> by fresh 4; rewrite if_true //.</span>
<span class="output-line" id="out31">[> Line 189: by ((fresh 4);(rewrite ... //)) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">B(j)</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step32">
<span class="input-line" id="in32"> expand frame, output, exec, cond, dmess.</span>
<span class="output-line" id="out32">[> Line 195: (expand frame, output, exec, cond, dmess) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<br> <<span class="gf" style="font-weight: bold">of_bool</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>) && true),<br> if (<span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>) && true) then<br> <span class="gf" style="font-weight: bold">enc</span>(if (<span class="gf" style="font-weight: bold">fst</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)) = <span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)) &&<br> <span class="gf" style="font-weight: bold">len</span>(<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>))) = <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))) then<br> <<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)),<span class="gn" style="color: #AA5500">n</span>(j)><br> else <<span class="gn" style="color: #AA5500">n</span>(j),<span class="gn" style="color: #AA5500">n</span>(j)>,<span class="gn" style="color: #AA5500">r</span>(j),<span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)))>><br><br><br></span>
<span class="com-line" id="com32"><p><strong>Case where t = B(j):</strong><br />
We have to show that the output message does not give any information to the attacker to distinguish the left side from the right side.</p>
</span>
</span>
<span class="squirrel-step" id="step33">
<span class="input-line" id="in33"><br> fa 3; fa 4; fa 4.</span>
<span class="output-line" id="out33">[> Line 196: ((fa 3);((fa 4);(fa 4))) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>4: <span class="gf" style="font-weight: bold">enc</span>(if (<span class="gf" style="font-weight: bold">fst</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)) = <span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)) &&<br> <span class="gf" style="font-weight: bold">len</span>(<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>))) = <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))) then<br> <<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)),<span class="gn" style="color: #AA5500">n</span>(j)><br> else <<span class="gn" style="color: #AA5500">n</span>(j),<span class="gn" style="color: #AA5500">n</span>(j)>,<span class="gn" style="color: #AA5500">r</span>(j),<span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)))<br><br><br></span>
</span>
<span class="squirrel-step" id="step34">
<span class="input-line" id="in34"> enckp 4; 1: auto.</span>
<span class="output-line" id="out34">[> Line 204: ((enckp 4); 1: auto) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>4: <span class="gf" style="font-weight: bold">enc</span>(if (<span class="gf" style="font-weight: bold">fst</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)) = <span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)) &&<br> <span class="gf" style="font-weight: bold">len</span>(<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>))) = <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))) then<br> <<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)),<span class="gn" style="color: #AA5500">n</span>(j)><br> else <<span class="gn" style="color: #AA5500">n</span>(j),<span class="gn" style="color: #AA5500">n</span>(j)>,<span class="gn" style="color: #AA5500">r</span>(j),<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>))<br><br><br></span>
<span class="com-line" id="com34"><p>We first use the key privacy assumption: knowing only a cipertext, it should not be possible to know which specific key was used. The corresponding <code>enckp</code> tactic allows here to replace <code>kAbis</code> by <code>kA</code> on the right side.</p>
</span>
</span>
<span class="squirrel-step" id="step35">
<span class="input-line" id="in35"> cca1 4; 2: auto.</span>
<span class="output-line" id="out35">[> Line 211: ((cca1 4); 2: auto) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>4: <span class="gf" style="font-weight: bold">len</span>(<br> if (<span class="gf" style="font-weight: bold">fst</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)) = <span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)) &&<br> <span class="gf" style="font-weight: bold">len</span>(<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>))) = <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))) then<br> <<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)),<span class="gn" style="color: #AA5500">n</span>(j)><br> else <<span class="gn" style="color: #AA5500">n</span>(j),<span class="gn" style="color: #AA5500">n</span>(j)>)<br><br><br></span>
<span class="com-line" id="com35"><p>We now use the ciphertext indistinguishability (IND-CCA1) assumption, which requires to show that the lengths of the plaintexts on both sides are equal.</p>
</span>
</span>
<span class="squirrel-step" id="step36">
<span class="input-line" id="in36"> rewrite if_len.</span>
<span class="output-line" id="out36">[> Line 214: (rewrite ...) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>4: if (<span class="gf" style="font-weight: bold">fst</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)) = <span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)) &&<br> <span class="gf" style="font-weight: bold">len</span>(<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>))) = <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))) then<br> <span class="gf" style="font-weight: bold">len</span>(<<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)),<span class="gn" style="color: #AA5500">n</span>(j)>)<br> else <span class="gf" style="font-weight: bold">len</span>(<<span class="gn" style="color: #AA5500">n</span>(j),<span class="gn" style="color: #AA5500">n</span>(j)>)<br><br><br></span>
<span class="com-line" id="com36"><p>We use the lemma <code>if_len</code> to push the conditional under len(_).</p>
</span>
</span>
<span class="squirrel-step" id="step37">
<span class="input-line" id="in37"><br><br> (* We use our axiom on the length of a pair.</span>
<span class="output-line" id="out37">[> Line 217: (rewrite ...) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>4: if (<span class="gf" style="font-weight: bold">fst</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>)) = <span class="gf" style="font-weight: bold">pk</span>(diff(<span class="gn" style="color: #AA5500">kA</span>, <span class="gn" style="color: #AA5500">kAbis</span>)) &&<br> <span class="gf" style="font-weight: bold">len</span>(<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>))) = <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))) then<br> <span class="gf" style="font-weight: bold">len</span>(<span class="gf" style="font-weight: bold">snd</span>(<span class="gf" style="font-weight: bold">dec</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span>,<span class="gn" style="color: #AA5500">kB</span>))) ++ <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))<br> else <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j)) ++ <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))<br><br><br></span>
</span>
<span class="squirrel-step" id="step38">
<span class="input-line" id="in38"> *)<br> rewrite !length_pair.</span>
<span class="output-line" id="out38">[> Line 221: (rewrite ... //) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>4: <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j)) ++ <span class="gf" style="font-weight: bold">len</span>(<span class="gn" style="color: #AA5500">n</span>(j))<br><br><br></span>
</span>
<span class="squirrel-step" id="step39">
<span class="input-line" id="in39"> rewrite (if_same_branch (len(n(j)) ++ len(n(j)))) //.</span>
<span class="output-line" id="out39">[> Line 224: ((fa 4);(fa 4)) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)]<br>IH: equiv(<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>), <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>), <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kB</span>)<br>1: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kAbis</span>)<br>2: <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">kA</span>)<br>3: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>4: <span class="gn" style="color: #AA5500">n</span>(j)<br><br><br></span>
<span class="com-line" id="com39"><p>We use the <code>if_same_branch</code> helper lemma to simplify the conditional using the fact that both branches are identical.</p>
</span>
</span>
<span class="squirrel-step" id="step40">
<span class="input-line" id="in40"> fa 4; fa 4.</span>
<span class="output-line" id="out40">[> Line 225: by ((fresh 4);(rewrite ... //)) <br>[goal> Goal anonymity is proved <br></span>
<span class="com-line" id="com40"><p>We conclude using the fact that <code>n(j)</code> is fresh.</p>
</span>
</span>
<span class="squirrel-step" id="step41">
<span class="input-line" id="in41"><br> by fresh 4; rewrite if_true //.</span>
<span class="output-line" id="out41">Exiting proof mode.<br><br><br></span>
</span>
</span>
<div class="page-header">
<img src="logo-circular.png" class="logo">
<h1 class="project-tagline">Squirrel Prover</h1>
<a href="https://squirrel-prover.github.io/examples.html" class="header-button">
<button type="button" class="header-button">Exit</button>
</a>
<button type="button" class="header-button" onclick="help()" id="button-panel">Help</button>
</div>
<div class="help-panel" id="help-panel">
Press the left and right arrows to do and undo an instruction.
<br><br>
Alternatively, you can double-click on an instruction.
<br><br>
<span style="color: #8B0000;" onmouseenter="highlightOn('in-zone')" onmouseleave="highlightOff('in-zone')">This zone</span> shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.
<br><br>
<span style="color: #8B0000;" onmouseenter="highlightOn('out-zone')" onmouseleave="highlightOff('out-zone')">This zone</span> shows the output given by Squirrel.
<br><br>
<span style="color: #8B0000;" onmouseenter="highlightOn('prec-zone')" onmouseleave="highlightOff('prec-zone')">This zone</span> shows the output of the previous instruction, to help identifying the change caused by the instruction.
</div>
<div class="mainsection" id="main">
<div class="example-grid">
<div class="example-col example-col-left" id="in-zone">
<p class="example-code"><span id="in-line"></span></p>
</div>
<div class="example-col example-col-right">
<div class="example-code example-code-right" style="height: 45%; border-bottom: 4px double #8B0000;" id="prec-zone"><span>Previously:</span><br><br><span id="prec-line"></span>
</div>
<div style="position: relative;">
<button type="button" class="prec-button" onclick="hidePrec()" id="prec-button" >Hide</button>
</div>
<div class="example-code example-code-right" style="height: 55%;" id="out-zone"><span id="out-line"></span>
</div>
</div>
</div>
</div>
<script src="script.js"></script>
</body>