-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathbasic-hash.html
More file actions
340 lines (292 loc) · 84 KB
/
basic-hash.html
File metadata and controls
340 lines (292 loc) · 84 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
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
<!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="basic-hash">BASIC HASH</h1>
<p>The Basic Hash protocol as described in [A] is an RFID protocol involving:</p>
<ul>
<li>a tag associated to a secret key;</li>
<li>generic readers having access to a database containing all these keys.</li>
</ul>
<p>The protocol is as follows:</p>
<pre><code>T --> R : <nT, h(nT,key)>
R --> T : ok</code></pre>
<p>In this file, we prove two security properties for this protocol.</p>
<ul>
<li><p>We first prove an <strong>authentication</strong> property for the reader.</p></li>
<li><p>We then prove <strong>unlinkability</strong>, <em>i.e.</em> the equivalence between a <strong>real</strong> system (where each tag can play multiple sessions) and an <strong>ideal</strong> system (where each tag plays only one session).</p></li>
</ul>
<p>[A] Mayla Brusò, Kostas Chatzikokolakis, and Jerry den Hartog. Formal Verification of Privacy for RFID Systems. pages 75–88, July 2010.</p>
<p>When this option is set to <code>true</code>, Squirrel checks that proofs are also sound for quantum attackers.</p>
</span>
</span>
<span class="squirrel-step" id="step1">
<span class="input-line" id="in1">include Basic.</span>
<span class="output-line" id="out1">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="com1"><p>Include basic standard library, important helper lemmas and setting proof mode to autoIntro=false.</p>
</span>
</span>
<span class="squirrel-step" id="step2">
<span class="input-line" id="in2">hash h<br><br>abstract ok : message<br>abstract ko : message.</span>
<span class="output-line" id="out2"></span>
<span class="com-line" id="com2"><p>We start by declaring the function symbol <code>h</code> for the hash function, as well as two public constants <code>ok</code> and <code>ko</code> (used by the reader).</p>
</span>
</span>
<span class="squirrel-step" id="step3">
<span class="input-line" id="in3">name key : index -> message<br>name key' : index -> index -> message<br><br><br><br>channel cT<br>channel cR.</span>
<span class="output-line" id="out3"></span>
<span class="com-line" id="com3"><p>In order to model the real system and the ideal system, we will use two different name symbols for the tags’ secret keys. The symbol <code>key</code> has index arity 1 and will be used in the real system, while the symbol <code>key'</code> has index arity 2 and will be used in the ideal system so that each new session of a tag uses a new key.</p>
<p>Finally, we declare the channels used by the protocol.</p>
</span>
</span>
<span class="squirrel-step" id="step4">
<span class="input-line" id="in4">process tag(i:index,k:index) =<br> new nT;<br> out(cT, <nT, h(nT,diff(key(i),key'(i,k)))>).</span>
<span class="output-line" id="out4"></span>
<span class="com-line" id="com4"><p>The tag’s role is modelled by the following process, indexed by <code>i</code> (for the identity of the tag) and by <code>k</code> (for the session of a given identity). The tag starts by generating a fresh random name <code>nT</code>, then outputs a message built using <code>key(i)</code> in the real system and <code>key'(i,k)</code> in the ideal system.</p>
</span>
</span>
<span class="squirrel-step" id="step5">
<span class="input-line" id="in5">process reader(j:index) =<br> in(cT,x);<br> if exists (i,k:index), snd(x) = h(fst(x),diff(key(i),key'(i,k))) then<br> out(cR,ok)<br> else<br> out(cR,ko).</span>
<span class="output-line" id="out5"></span>
<span class="com-line" id="com5"><p>The reader’s role is modelled by the following process. Since readers are generic, the process is indexed only by <code>j</code> (for the session). The reader starts by inputting a message <code>x</code> before checking whether this message corresponds to a legitimate output performed by a tag. On the left side (the real system), the reader looks up for a key <code>key(i)</code> in the database (the one corresponding to the tag of identity <code>i</code>). On the right side (the ideal system), the reader looks up for a key <code>key(i,k)</code> in the database (the one used by the tag of identity <code>i</code> at session <code>k</code>).</p>
</span>
</span>
<span class="squirrel-step" id="step6">
<span class="input-line" id="in6">system [BasicHash] ((!_j R: reader(j)) | (!_i !_k T: tag(i,k))).</span>
<span class="output-line" id="out6">System before processing:<br> <br> (!_j R: <span class="pn" style="font-weight:bold; color: #0000AA">reader</span> j) | (!_i !_k T: <span class="pn" style="font-weight:bold; color: #0000AA">tag</span> i k)<br><br>System after processing:<br> <br> (!_j<br> <span class="pio" style="font-weight: bold">in</span>(<span class="pc">cT</span>,<span class="pv" style="font-weight: bold; color: #AA00AA">x</span>);<br> <span class="pc" style="text-decoration: underline; color: #AA0000">if</span> <span>exists</span> (i,k:index), (snd(x) = h(fst(x),<span>diff</span>(key(i),key'(i,k)))) <span class="pc" style="text-decoration: underline; color: #AA0000">then</span><br> R: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cR</span>,ok); <span class="pn" style="font-weight:bold; color: #0000AA">null</span> <span class="pc" style="text-decoration: underline; color: #AA0000">else</span> R1: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cR</span>,ko); <span class="pn" style="font-weight:bold; color: #0000AA">null</span>) |<br> (!_i !_k T: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cT</span>,pair(nT(i,k),h(nT(i,k),<span>diff</span>(key(i),key'(i,k))))); <span class="pn" style="font-weight:bold; color: #0000AA">null</span>)<br><br>System BasicHash registered with actions (init,R,R1,T).<br></span>
<span class="com-line" id="com6"><p>The system is finally defined by putting an unbounded number of tag and reader processes in parallel. This system is automatically translated to a set of actions:</p>
<ul>
<li>the initial action (<code>init</code>);</li>
<li>one action for the tag (<code>T</code>);</li>
<li>two actions for the reader, corresponding to the two branches of the conditional (respectively <code>R</code> and <code>R1</code>).</li>
</ul>
</span>
</span>
<span class="squirrel-step" id="step7">
<span class="input-line" id="in7">goal [BasicHash] wa_R :<br> forall (tau:timestamp),<br> happens(tau) =><br> ((exists (i,k:index),<br> snd(input@tau) = h(fst(input@tau),diff(key(i),key'(i,k))))<br> =<br> (exists (i,k:index), T(i,k) < tau &&<br> fst(output@T(i,k)) = fst(input@tau) &&<br> snd(output@T(i,k)) = snd(input@tau))).</span>
<span class="output-line" id="out7">Goal wa_R :<br> forall (tau:timestamp),<br> <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau) =><br> (exists (i,k:index),<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))) =<br> exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) &&<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br></span>
<span class="com-line" id="com7"><p>Whenever a reader accepts a message (<em>i.e.</em> the condition of the action <code>R(j)</code> evaluates to <code>true</code>), there exists an action <code>T(i,k)</code> that has been executed before the reader, and such that the input of the reader corresponds to the output of this tag (and conversely).</p>
<p>The same holds for <code>R1</code> (the else branch of the reader) but with a negation. We will prove once and for all a property that is generalized for any <code>tau</code>, which will be useful later for <code>tau = R(j)</code> and <code>tau = R1(j)</code>.</p>
<p>Note that we express our correspondence property on each projection of the pair. Indeed, for some implementations of the pairing primitive, the equality of projections does not imply the equality of pairs.</p>
</span>
</span>
<span class="squirrel-step" id="step8">
<span class="input-line" id="in8">Proof.</span>
<span class="output-line" id="out8">[goal> Focused goal (1/1):<br>System: left:BasicHash/left, right:BasicHash/right<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>forall (tau:timestamp),<br> <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau) =><br> (exists (i,k:index),<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))) =<br> exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) &&<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><br></span>
<span class="com-line" id="com8"><p>The high-level idea of the proof is to use the EUF cryptographic axiom: only the tag <code>T(i,k)</code> can forge <code>h(nT(i,k),key(i))</code> because the secret key is not known by the attacker. Therefore, any message accepted by the reader must come from a tag that has played before. The converse implication is trivial because any honest tag output is accepted by the reader.</p>
</span>
</span>
<span class="squirrel-step" id="step9">
<span class="input-line" id="in9"> intro tau Hap.</span>
<span class="output-line" id="out9">[> Line 130: (intro tau Hap) <br>[goal> Focused goal (1/1):<br>System: left:BasicHash/left, right:BasicHash/right<br>Variables: tau:timestamp<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(exists (i,k:index),<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))) =<br>exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) && <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><br></span>
<span class="com-line" id="com9"><p>We start by introducing the variable <code>j</code> and the hypothesis <code>happens(R(j))</code>, before unfolding the definiton of the <code>cond</code> macro, which corresponds to an existential quantification.</p>
</span>
</span>
<span class="squirrel-step" id="step10">
<span class="input-line" id="in10"> rewrite eq_iff; split => [i k Meq].</span>
<span class="output-line" id="out10">[> Line 133: (((rewrite ...);split);(intro [i k Meq])) <br>[goal> Focused goal (1/2):<br>System: left:BasicHash/left, right:BasicHash/right<br>Variables: i,k:index,tau:timestamp<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau)<br>Meq: <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) && <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><br></span>
<span class="com-line" id="com10"><p>We have to prove two implications (<code><=></code>): we thus split the proof in two parts. We now have two different goals to prove.</p>
</span>
</span>
<span class="squirrel-step" id="step11">
<span class="input-line" id="in11"> + project.</span>
<span class="output-line" id="out11">[> Line 136: project <br>[goal> Focused goal (1/3):<br>System: left:BasicHash/left<br>Variables: i,k:index,tau:timestamp<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau)<br>Meq: <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),<span class="gn" style="color: #AA5500">key</span>(i))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) && <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><br></span>
<span class="com-line" id="com11"><p>For the first implication (=>), we actually prove it separately for the real system (left) and the ideal system (right).</p>
</span>
</span>
<span class="squirrel-step" id="step12">
<span class="input-line" id="in12"> ++ (* LEFT *)<br> euf Meq => *.</span>
<span class="output-line" id="out12">[> Line 144: ((euf Meq);(intro *)) <br>[goal> Focused goal (1/3):<br>System: left:BasicHash/left<br>Variables: i,k,k0:index,tau:timestamp<br>Clt: <span class="ga" style="color: #00AA00">T(i,k0)</span> < tau<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau)<br>Meq: <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),<span class="gn" style="color: #AA5500">key</span>(i))<br>Meq0: <span class="gn" style="color: #AA5500">nT</span>(i,k0) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) && <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><br></span>
<span class="com-line" id="com12"><p>The proof is very similar on both sides and relies on the <code>euf</code> tactic. Applying the <code>euf</code> tactic on the <code>Meq</code> hypothesis generates a new hypothesis stating that <code>fst(input@R(j))</code> must be equal to some message that has already been hashed before. The only possibility is that this hash comes from the output of a tag that has played before (thus the new hypothesis on timestamps).</p>
</span>
</span>
<span class="squirrel-step" id="step13">
<span class="input-line" id="in13"> by exists i,k0.</span>
<span class="output-line" id="out13">[> Line 144: by (exists i, k0) <br>[goal> Focused goal (1/2):<br>System: right:BasicHash/right<br>Variables: i,k:index,tau:timestamp<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau)<br>Meq: <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),<span class="gn" style="color: #AA5500">key'</span>(i,k))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) && <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><br></span>
</span>
<span class="squirrel-step" id="step14">
<span class="input-line" id="in14"><br> ++ (* RIGHT *)<br> euf Meq => *.</span>
<span class="output-line" id="out14">[> Line 146: ((euf Meq);(intro *)) <br>[goal> Focused goal (1/2):<br>System: right:BasicHash/right<br>Variables: i,k:index,tau:timestamp<br>Clt: <span class="ga" style="color: #00AA00">T(i,k)</span> < tau<br>H: i = i && k = k<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau)<br>Meq: <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),<span class="gn" style="color: #AA5500">key'</span>(i,k))<br>Meq0: <span class="gn" style="color: #AA5500">nT</span>(i,k) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) && <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><br></span>
</span>
<span class="squirrel-step" id="step15">
<span class="input-line" id="in15"> by exists i,k.</span>
<span class="output-line" id="out15">[> Line 146: by (exists i, k) <br>[goal> Focused goal (1/1):<br>System: left:BasicHash/left, right:BasicHash/right<br>Variables: i,k:index,tau:timestamp<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(tau)<br>Meq: <span class="ga" style="color: #00AA00">T(i,k)</span> < tau &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) &&<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i,k:index),<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau) = <span class="gf" style="font-weight: bold">h</span>(<span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))<br><br></span>
</span>
<span class="squirrel-step" id="step16">
<span class="input-line" id="in16"> + by exists i,k.</span>
<span class="output-line" id="out16">[> Line 149: by (exists i, k) <br>[goal> Goal wa_R is proved <br></span>
<span class="com-line" id="com16"><p>For the second implication (<=), the conclusion of the goal can directly be obtained from the hypotheses.</p>
</span>
</span>
<span class="squirrel-step" id="step17">
<span class="input-line" id="in17"><br>Qed.</span>
<span class="output-line" id="out17">Exiting proof mode.<br><br><br></span>
</span>
<span class="squirrel-step" id="step18">
<span class="input-line" id="in18">equiv [BasicHash] unlinkability.</span>
<span class="output-line" id="out18">Goal unlinkability :<br> forall t:timestamp, equiv(<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@t)<br></span>
<span class="com-line" id="com18"><p>We now prove an equivalence property expressing unlinkability of the protocol. This property is expressed by the logic formula <code>forall t:timestamp, frame@t</code> where <code>frame@t</code> is actually a bi-frame. We will have to prove that the left projection of <code>frame@t</code> (<em>i.e.</em> the real system) is indistinguishable from the right projection of <code>frame@t</code> (<em>i.e.</em> the ideal system).</p>
</span>
</span>
<span class="squirrel-step" id="step19">
<span class="input-line" id="in19">Proof.</span>
<span class="output-line" id="out19">[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/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="com19"><p>The high-level idea of the proof is as follows:</p>
<ul>
<li><p>if <code>t</code> corresponds to a reader’s action, we show that the outcome of the conditional is the same on both sides and that this outcome only depends on information already available to the attacker;</p></li>
<li><p>if <code>t</code> corresponds to a tag’s action, we show that the new message added in the frame (<em>i.e.</em> the tag’s output) does not give any information to the attacker to distinguish the real system from the ideal one since hashes can intuitively be seen as fresh names thanks to the PRF cryptographic axiom.</p></li>
</ul>
</span>
</span>
<span class="squirrel-step" id="step20">
<span class="input-line" id="in20"> induction t; 1: auto.</span>
<span class="output-line" id="out20">[> Line 177: ((induction t); 1: auto) <br>[goal> Focused goal (1/3):<br>Systems: left:BasicHash/left, right:BasicHash/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">R(j)</span>)]<br>IH: equiv(<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">R(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">R(j)</span><br><br><br></span>
<span class="com-line" id="com20"><p>The proof is done by induction over the timestamp <code>t</code>. The <code>induction</code> tactic also automatically introduces a case analysis over all the possible values for <code>t</code>. The first case, where <code>t = init</code>, is trivial. The other cases correspond to the 3 different actions of the protocol.</p>
</span>
</span>
<span class="squirrel-step" id="step21">
<span class="input-line" id="in21"> + expand frame, exec, output.</span>
<span class="output-line" id="out21">[> Line 181: (expand frame, exec, output) <br>[goal> Focused goal (1/3):<br>Systems: left:BasicHash/left, right:BasicHash/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">R(j)</span>)]<br>IH: equiv(<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">R(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <<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">R(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">R(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">R(j)</span>),<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">R(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">R(j)</span>) then <span class="gf" style="font-weight: bold">ok</span>>><br><br><br></span>
<span class="com-line" id="com21"><p><strong>Case where t = R(j):</strong> We start by expanding the macros and splitting the pairs.</p>
</span>
</span>
<span class="squirrel-step" id="step22">
<span class="input-line" id="in22"> fa !<_,_>.</span>
<span class="output-line" id="out22">[> Line 181: (fa !pair(_,_)) <br>[goal> Focused goal (1/3):<br>Systems: left:BasicHash/left, right:BasicHash/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">R(j)</span>)]<br>IH: equiv(<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">R(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">R(j)</span>)<br>1: <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">R(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">R(j)</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step23">
<span class="input-line" id="in23"> rewrite /cond (wa_R (R(j)) H).</span>
<span class="output-line" id="out23">[> Line 186: (rewrite ... ...) <br>[goal> Focused goal (1/3):<br>Systems: left:BasicHash/left, right:BasicHash/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">R(j)</span>)]<br>IH: equiv(<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">R(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">R(j)</span>)<br>1: <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">R(j)</span>) &&<br> exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < <span class="ga" style="color: #00AA00">R(j)</span> &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>) &&<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>)<br><br><br></span>
<span class="com-line" id="com23"><p>Using the authentication goal <code>wa_R</code> previously proved, we replace the formula <code>cond@R(j)</code> by an equivalent formula expressing the fact that a tag <code>T(i,k)</code> has played before and that the output of this tag is the message inputted by the reader.</p>
</span>
</span>
<span class="squirrel-step" id="step24">
<span class="input-line" id="in24"> by fadup 1.</span>
<span class="output-line" id="out24">[> Line 191: by (fadup 1) <br>[goal> Focused goal (1/2):<br>Systems: left:BasicHash/left, right:BasicHash/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">R1(j)</span>)]<br>IH: equiv(<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">R1(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">R1(j)</span><br><br><br></span>
<span class="com-line" id="com24"><p>We are now able to remove this formula from the frame because the attacker is able to compute it using information obtained in the past. Indeed, each element of this formula is already available in <code>frame@pred(R(j))</code>. This is done by the <code>fadup</code> tactic.</p>
</span>
</span>
<span class="squirrel-step" id="step25">
<span class="input-line" id="in25"> + expand frame, exec, output.</span>
<span class="output-line" id="out25">[> Line 195: (expand frame, exec, output) <br>[goal> Focused goal (1/2):<br>Systems: left:BasicHash/left, right:BasicHash/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">R1(j)</span>)]<br>IH: equiv(<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">R1(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <<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">R1(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">R1(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">R1(j)</span>),<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">R1(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">R1(j)</span>) then <span class="gf" style="font-weight: bold">ko</span>>><br><br><br></span>
<span class="com-line" id="com25"><p><strong>Case where t = R1(j):</strong><br />
This case is similar to the previous one.</p>
</span>
</span>
<span class="squirrel-step" id="step26">
<span class="input-line" id="in26"> fa !<_,_>.</span>
<span class="output-line" id="out26">[> Line 195: (fa !pair(_,_)) <br>[goal> Focused goal (1/2):<br>Systems: left:BasicHash/left, right:BasicHash/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">R1(j)</span>)]<br>IH: equiv(<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">R1(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">R1(j)</span>)<br>1: <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">R1(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">R1(j)</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step27">
<span class="input-line" id="in27"><br> rewrite /cond (wa_R (R1(j)) H).</span>
<span class="output-line" id="out27">[> Line 196: (rewrite ... ...) <br>[goal> Focused goal (1/2):<br>Systems: left:BasicHash/left, right:BasicHash/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">R1(j)</span>)]<br>IH: equiv(<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">R1(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">R1(j)</span>)<br>1: <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">R1(j)</span>) &&<br> not(exists (i,k:index),<br> <span class="ga" style="color: #00AA00">T(i,k)</span> < <span class="ga" style="color: #00AA00">R1(j)</span> &&<br> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>) &&<br> <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">output</span>@<span class="ga" style="color: #00AA00">T(i,k)</span>) = <span class="gf" style="font-weight: bold">snd</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>))<br><br><br></span>
</span>
<span class="squirrel-step" id="step28">
<span class="input-line" id="in28"><br> by fadup 1.</span>
<span class="output-line" id="out28">[> Line 197: by (fadup 1) <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">T(i,k)</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step29">
<span class="input-line" id="in29"> + expand frame, exec, cond, output.</span>
<span class="output-line" id="out29">[> Line 201: (expand frame, exec, cond, output) <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <<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">T(i,k)</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">T(i,k)</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">T(i,k)</span>) && true) then<br> <<span class="gn" style="color: #AA5500">nT</span>(i,k),<span class="gf" style="font-weight: bold">h</span>(<span class="gn" style="color: #AA5500">nT</span>(i,k),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))>>><br><br><br></span>
<span class="com-line" id="com29"><p><strong>Case where t = T(i,k):</strong><br />
We start by expanding the macros and splitting the pairs.</p>
</span>
</span>
<span class="squirrel-step" id="step30">
<span class="input-line" id="in30"><br> fa !<_,_>, if _ then _, <_,_>.</span>
<span class="output-line" id="out30">[> Line 202: (fa !pair(_,_) <span>if</span> _ <span>then</span> _ <span>else</span> zero pair(_,_)) <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">T(i,k)</span>)<br>1: <span class="gn" style="color: #AA5500">nT</span>(i,k)<br>2: <span class="gf" style="font-weight: bold">h</span>(<span class="gn" style="color: #AA5500">nT</span>(i,k),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))<br><br><br></span>
</span>
<span class="squirrel-step" id="step31">
<span class="input-line" id="in31"> prf 2.</span>
<span class="output-line" id="out31">[> Line 208: (prf 2) <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">T(i,k)</span>)<br>1: <span class="gn" style="color: #AA5500">nT</span>(i,k)<br>2: if (true &&<br> diff(<br> forall (j,i0:index),<br> <span class="ga" style="color: #00AA00">R(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>),<br> forall (j,i0,k0:index),<br> <span class="ga" style="color: #00AA00">R(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>)) &&<br> diff(<br> (forall (j,i0:index),<br> <span class="ga" style="color: #00AA00">R1(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>)) &&<br> forall (i0,k0:index),<br> <span class="ga" style="color: #00AA00">T(i0,k0)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gn" style="color: #AA5500">nT</span>(i0,k0),<br> (forall (j,i0,k0:index),<br> <span class="ga" style="color: #00AA00">R1(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>)) &&<br> forall (i0,k0:index),<br> <span class="ga" style="color: #00AA00">T(i0,k0)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gn" style="color: #AA5500">nT</span>(i0,k0)))<br> then <span class="gn" style="color: #AA5500">n_PRF</span><br> else <span class="gf" style="font-weight: bold">h</span>(<span class="gn" style="color: #AA5500">nT</span>(i,k),diff(<span class="gn" style="color: #AA5500">key</span>(i), <span class="gn" style="color: #AA5500">key'</span>(i,k)))<br><br><br></span>
<span class="com-line" id="com31"><p>We now apply the <code>prf</code> tactic, in order to replace the hash by a fresh name. The tactic actually replaces the hash by a conditional term in which the then branch is the fresh name. The goal is now to prove that this condition always evaluates to <code>true</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step32">
<span class="input-line" id="in32"> rewrite if_true.</span>
<span class="output-line" id="out32">[> Line 208: (rewrite ...) <br>[goal> Focused goal (1/2):<br>System: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>true &&<br>diff(<br> forall (j,i0:index), <span class="ga" style="color: #00AA00">R(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>),<br> forall (j,i0,k0:index),<br> <span class="ga" style="color: #00AA00">R(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>)) &&<br>diff(<br> (forall (j,i0:index),<br> <span class="ga" style="color: #00AA00">R1(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>)) &&<br> forall (i0,k0:index), <span class="ga" style="color: #00AA00">T(i0,k0)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gn" style="color: #AA5500">nT</span>(i0,k0),<br> (forall (j,i0,k0:index),<br> <span class="ga" style="color: #00AA00">R1(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>)) &&<br> forall (i0,k0:index),<br> <span class="ga" style="color: #00AA00">T(i0,k0)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gn" style="color: #AA5500">nT</span>(i0,k0))<br><br></span>
</span>
<span class="squirrel-step" id="step33">
<span class="input-line" id="in33"> {<br> split; 1: true.</span>
<span class="output-line" id="out33">[> Line 209: (split; 1: true) <br>[goal> Focused goal (1/2):<br>System: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>diff(<br> forall (j,i0:index), <span class="ga" style="color: #00AA00">R(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>),<br> forall (j,i0,k0:index),<br> <span class="ga" style="color: #00AA00">R(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R(j)</span>)) &&<br>diff(<br> (forall (j,i0:index),<br> <span class="ga" style="color: #00AA00">R1(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>)) &&<br> forall (i0,k0:index), <span class="ga" style="color: #00AA00">T(i0,k0)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gn" style="color: #AA5500">nT</span>(i0,k0),<br> (forall (j,i0,k0:index),<br> <span class="ga" style="color: #00AA00">R1(j)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gf" style="font-weight: bold">fst</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">R1(j)</span>)) &&<br> forall (i0,k0:index),<br> <span class="ga" style="color: #00AA00">T(i0,k0)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i = i0 && k = k0 => <span class="gn" style="color: #AA5500">nT</span>(i,k) <> <span class="gn" style="color: #AA5500">nT</span>(i0,k0))<br><br></span>
</span>
<span class="squirrel-step" id="step34">
<span class="input-line" id="in34"> project; repeat split; intro *; by fresh Meq.</span>
<span class="output-line" id="out34">[> Line 224: (project;((repeat split);((intro *);by (fresh Meq)))) <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">T(i,k)</span>)<br>1: <span class="gn" style="color: #AA5500">nT</span>(i,k)<br>2: <span class="gn" style="color: #AA5500">n_PRF</span><br><br><br></span>
<span class="com-line" id="com34"><p>Several conjuncts must now be proved, the same tactic can be used on all of them. Here are representative cases:</p>
<ul>
<li>In one case, <code>nT(i,k)</code> cannot occur in <code>input@R(j)</code> because <code>R(j) < T(i,k)</code>.</li>
<li>In another case, <code>nT(i,k) = nT(i0,k0)</code> implies that <code>i=i0</code> and <code>k=k0</code>, contradicting <code>T(i0,k0)<T(i,k)</code>.</li>
</ul>
<p>In both cases, the reasoning is performed by the fresh tactic on the message equality hypothesis <code>Meq</code> whose negation must initially be proved. To be able to use (split and) fresh, we first project the goal into into one goal for the left projection and one goal for the right projection of the initial bi-system.</p>
</span>
</span>
<span class="squirrel-step" id="step35">
<span class="input-line" id="in35"><br> }.</span>
<span class="output-line" id="out35">[> Line 225: ?? <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">T(i,k)</span>)<br>1: <span class="gn" style="color: #AA5500">nT</span>(i,k)<br>2: <span class="gn" style="color: #AA5500">n_PRF</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step36">
<span class="input-line" id="in36"> fresh 2.</span>
<span class="output-line" id="out36">[> Line 230: (fresh 2) <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">T(i,k)</span>)<br>1: <span class="gn" style="color: #AA5500">nT</span>(i,k)<br><br><br></span>
<span class="com-line" id="com36"><p>We have now replaced the hash by a fresh name occurring nowhere else, so we can remove it using the <code>fresh</code> tactic.</p>
</span>
</span>
<span class="squirrel-step" id="step37">
<span class="input-line" id="in37"> fresh 1.</span>
<span class="output-line" id="out37">[> Line 233: (fresh 1) <br>[goal> Focused goal (1/1):<br>Systems: left:BasicHash/left, right:BasicHash/right (same for equivalences)<br>Variables: i,k:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">T(i,k)</span>)]<br>IH: equiv(<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">T(i,k)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <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">T(i,k)</span>)<br>1: if (forall (i0,k0:index), <span class="ga" style="color: #00AA00">T(i0,k0)</span> < <span class="ga" style="color: #00AA00">T(i,k)</span> => i0 <> i || k0 <> k) then<br> <span class="gf" style="font-weight: bold">zero</span><br> else <span class="gn" style="color: #AA5500">nT</span>(i,k)<br><br><br></span>
<span class="com-line" id="com37"><p>We can also remove the name <code>nT(i,k)</code>, and conclude by induction hypothesis.</p>
</span>
</span>
<span class="squirrel-step" id="step38">
<span class="input-line" id="in38"><br> by rewrite if_true.</span>
<span class="output-line" id="out38">[> Line 234: by (rewrite ...) <br>[goal> Goal unlinkability is proved <br></span>
</span>
<span class="squirrel-step" id="step39">
<span class="input-line" id="in39"><br>Qed.</span>
<span class="output-line" id="out39">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>