-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathtoy-counter.html
More file actions
277 lines (236 loc) · 30.3 KB
/
toy-counter.html
File metadata and controls
277 lines (236 loc) · 30.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
<!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">hash h<br><br>name secret : message<br>name key : message<br><br>abstract error : message<br>abstract myZero : message<br><br><br>mutable d : message = myZero<br><br>channel cA<br>channel cB.</span>
<span class="output-line" id="out0"></span>
<span class="com-line" id="com0"><h1 id="toy-counter">TOY-COUNTER</h1>
<p>V. Cheval, V. Cortier, and M. Turuani,<br />
<em>A Little More Conversation, a Little Less Action, a Lot More Satisfaction: Global States in ProVerif</em>,<br />
in 2018 IEEE 31st Computer Security Foundations Symposium (CSF), Oxford, Jul. 2018, pp. 344–358,<br />
doi: 10.1109/CSF.2018.00032.</p>
<ul>
<li><code>A = in(d, i : nat); out(c, h(i, s)); out(d, i + 1)</code></li>
<li><code>B = in(d, i : nat); in(c, y);</code><br />
<code>if y = h(i, s) then</code><br />
<code>out(c, s); out(d, i + 1)</code><br />
<code>else</code><br />
<code>out(d, i + 1)</code></li>
<li><code>P = ! A | ! B | out(d, 0) | ! in(d, i : nat); out(d, i)</code></li>
</ul>
<h4 id="comments">COMMENTS</h4>
<ul>
<li>In this model, we do not use private channels since actions (input/condition/ update/output) are atomic.</li>
<li>The goal is to prove that the secret s is never leaked because B receives only hashes with old values of the counter.</li>
</ul>
<h4 id="security-properties">SECURITY PROPERTIES</h4>
<ul>
<li>monotonicity of the counter</li>
<li>secrecy (as a reachability property)</li>
</ul>
<p>We declare here a mutable state symbol, initialized with the public constant <code>myZero</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step1">
<span class="input-line" id="in1">abstract mySucc : message->message<br>abstract (~<) : message -> message -> boolean.</span>
<span class="output-line" id="out1"></span>
<span class="com-line" id="com1"><p>In order to model counter values, we use:</p>
<ul>
<li>a function <code>mySucc</code> modelling the successor of a value;</li>
<li>an order relation <code>~<</code> modelling the usual order on natural numbers.</li>
</ul>
</span>
</span>
<span class="squirrel-step" id="step2">
<span class="input-line" id="in2">process A =<br> let m = h(<d,secret>,key) in<br> d := mySucc(d);<br> out(cA, m)<br><br>process B =<br> in(cA,y);<br> if y = h(<d,secret>,key) then<br> d := mySucc(d);<br> out(cB,secret)<br> else<br> d := mySucc(d);<br> out(cB,error)<br><br>system ((!_i A) | (!_j B)).</span>
<span class="output-line" id="out2">System before processing:<br> <br> (!_i <span class="pn" style="font-weight:bold; color: #0000AA">A</span> ) | (!_j <span class="pn" style="font-weight:bold; color: #0000AA">B</span> )<br><br>System after processing:<br> <br> (!_i <span class="pk" style="font-weight: bold">let</span> <span class="pv" style="font-weight: bold; color: #AA00AA">m</span> = h(pair(d,secret),key) <span class="pk" style="font-weight: bold">in</span><br> d <span class="pk" style="font-weight: bold">:=</span> mySucc(d); A: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cA</span>,m(i)); <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">cA</span>,<span class="pv" style="font-weight: bold; color: #AA00AA">y</span>);<br> <span class="pc" style="text-decoration: underline; color: #AA0000">if</span> (y = h(pair(d,secret),key)) <span class="pc" style="text-decoration: underline; color: #AA0000">then</span><br> d <span class="pk" style="font-weight: bold">:=</span> mySucc(d); B: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cB</span>,secret); <span class="pn" style="font-weight:bold; color: #0000AA">null</span> <span class="pc" style="text-decoration: underline; color: #AA0000">else</span><br> d <span class="pk" style="font-weight: bold">:=</span> mySucc(d); B1: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cB</span>,error); <span class="pn" style="font-weight:bold; color: #0000AA">null</span>)<br><br>System default registered with actions (init,A,B,B1).<br></span>
<span class="com-line" id="com2"><p>Processes A and B are defined as follows. They both access to the mutable state <code>d</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step3">
<span class="input-line" id="in3">axiom orderSucc (n:message): n ~< mySucc(n).</span>
<span class="output-line" id="out3"></span>
<span class="com-line" id="com3"><h4 id="axioms">AXIOMS</h4>
<p>We now axiomatize the order relation <code>~<</code> defined above in order to be able to reason on counter values.</p>
</span>
</span>
<span class="squirrel-step" id="step4">
<span class="input-line" id="in4"><br>axiom orderTrans (n1,n2,n3:message): n1 ~< n2 && n2 ~< n3 => n1 ~< n3.</span>
<span class="output-line" id="out4"></span>
</span>
<span class="squirrel-step" id="step5">
<span class="input-line" id="in5"><br>axiom orderStrict (n1,n2:message): n1 = n2 => n1 ~< n2 => false.</span>
<span class="output-line" id="out5"></span>
</span>
<span class="squirrel-step" id="step6">
<span class="input-line" id="in6">goal counterIncreasePred (t:timestamp):<br> t > init => d@pred(t) ~< d@t.</span>
<span class="output-line" id="out6">Goal counterIncreasePred :<br> t > <span class="ga" style="color: #00AA00">init</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t) ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br></span>
<span class="com-line" id="com6"><h4 id="security-properties">SECURITY PROPERTIES</h4>
<p>We first show that the counter increases strictly at each update.</p>
</span>
</span>
<span class="squirrel-step" id="step7">
<span class="input-line" id="in7"><br>Proof.</span>
<span class="output-line" id="out7">[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t:timestamp<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>t > <span class="ga" style="color: #00AA00">init</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t) ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step8">
<span class="input-line" id="in8"><br> intro Hc.</span>
<span class="output-line" id="out8">[> Line 93: (intro Hc) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t:timestamp<br>Hc: t > <span class="ga" style="color: #00AA00">init</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t) ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step9">
<span class="input-line" id="in9"><br> use orderSucc with d@pred(t).</span>
<span class="output-line" id="out9">[> Line 94: (have ... as ) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t:timestamp<br>H: <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t) ~< <span class="gf" style="font-weight: bold">mySucc</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t))<br>Hc: t > <span class="ga" style="color: #00AA00">init</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t) ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step10">
<span class="input-line" id="in10"><br> case t => //.</span>
<span class="output-line" id="out10">[> Line 95: ((case t);(intro //)) <br>[goal> Goal counterIncreasePred is proved <br></span>
</span>
<span class="squirrel-step" id="step11">
<span class="input-line" id="in11"><br>Qed.</span>
<span class="output-line" id="out11">Exiting proof mode.<br><br><br></span>
</span>
<span class="squirrel-step" id="step12">
<span class="input-line" id="in12">goal counterIncrease (t,t':timestamp):<br> t' < t => d@t' ~< d@t.</span>
<span class="output-line" id="out12">Goal counterIncrease :<br> t' < t => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br></span>
<span class="com-line" id="com12"><p>We also show a more general result than counterIncreasePred, stating here that the counter strictly increases between two distinct timestamps.</p>
<p>The proof is done by induction, and relies on the previous result counterIncreasePred.</p>
</span>
</span>
<span class="squirrel-step" id="step13">
<span class="input-line" id="in13"><br>Proof.</span>
<span class="output-line" id="out13">[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>t' < t => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step14">
<span class="input-line" id="in14"><br> induction t => t Hind Ht.</span>
<span class="output-line" id="out14">[> Line 108: ((induction t);(intro t Hind Ht)) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step15">
<span class="input-line" id="in15"> assert (t' < pred(t) || t' >= pred(t)) as H0 by case t.</span>
<span class="output-line" id="out15">[> Line 110: ((have ((t' < pred(t)) || (t' >= pred(t))), H0); 1: by (case t)) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>H0: t' < <span class="gf" style="font-weight: bold">pred</span>(t) || t' >= <span class="gf" style="font-weight: bold">pred</span>(t)<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
<span class="com-line" id="com15"><p>We use the <code>assert</code> tactic to introduce two cases.</p>
</span>
</span>
<span class="squirrel-step" id="step16">
<span class="input-line" id="in16"><br> case H0.</span>
<span class="output-line" id="out16">[> Line 111: (case H0) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>H0: t' < <span class="gf" style="font-weight: bold">pred</span>(t)<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step17">
<span class="input-line" id="in17"> + apply Hind in H0 => //.</span>
<span class="output-line" id="out17">[> Line 118: ((apply ... in H0);(intro //)) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>H0: <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t)<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
<span class="com-line" id="com17"><p><strong>Case where t’ < pred(t):</strong> We first apply the induction hypothesis on <code>t'</code> to get <code>d@t' ~< d@pred(t)</code>, then use the lemma counterIncreasePred with <code>t</code> to get <code>d@pred(t) ~< d@t</code>. It then remains to conclude by transitivity (applying <code>orderTrans</code>).</p>
</span>
</span>
<span class="squirrel-step" id="step18">
<span class="input-line" id="in18"><br> use counterIncreasePred with t; 2: by constraints.</span>
<span class="output-line" id="out18">[> Line 119: ((have ... as ); 2: by constraints) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>H: <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t) ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br>H0: <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t)<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step19">
<span class="input-line" id="in19"><br> by apply orderTrans _ (d@pred(t)).</span>
<span class="output-line" id="out19">[> Line 120: by (apply ... ) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>H0: t' >= <span class="gf" style="font-weight: bold">pred</span>(t)<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step20">
<span class="input-line" id="in20"> + assert t' = pred(t) as Ceq by constraints.</span>
<span class="output-line" id="out20">[> Line 126: ((have (t' = pred(t)), Ceq); 1: by constraints) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>Ceq: t' = <span class="gf" style="font-weight: bold">pred</span>(t)<br>H0: t' >= <span class="gf" style="font-weight: bold">pred</span>(t)<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
<span class="com-line" id="com20"><p><strong>Case where t’ >= pred(t).</strong> Since <code>t' < t</code> we can deduce that <code>t' = pred(t)</code>. It is then directly a consequence of the counterIncreasePred lemma.</p>
</span>
</span>
<span class="squirrel-step" id="step21">
<span class="input-line" id="in21"><br> use counterIncreasePred with t; 2: auto.</span>
<span class="output-line" id="out21">[> Line 127: ((have ... as ); 2: auto) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: t,t':timestamp<br>Ceq: t' = <span class="gf" style="font-weight: bold">pred</span>(t)<br>H: <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(t) ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br>H0: t' >= <span class="gf" style="font-weight: bold">pred</span>(t)<br>Hind: forall (t0:timestamp), t0 < t => t' < t0 => <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t0<br>Ht: t' < t<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t' ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@t<br><br></span>
</span>
<span class="squirrel-step" id="step22">
<span class="input-line" id="in22"><br> by rewrite Ceq; auto.</span>
<span class="output-line" id="out22">[> Line 128: by ((rewrite ...);auto) <br>[goal> Goal counterIncrease is proved <br></span>
</span>
<span class="squirrel-step" id="step23">
<span class="input-line" id="in23"><br>Qed.</span>
<span class="output-line" id="out23">Exiting proof mode.<br><br><br></span>
</span>
<span class="squirrel-step" id="step24">
<span class="input-line" id="in24">goal secretReach (j:index):<br> happens(B(j)) => cond@B(j) => false.</span>
<span class="output-line" id="out24">Goal secretReach :<br> <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>) => <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">B(j)</span> => false<br></span>
<span class="com-line" id="com24"><p>The following reachability property states that the secret s is never leaked (<em>i.e.</em> the condition of the action <code>B(j)</code> is never satisfied).</p>
<p>The proof relies on the EUF assumption: if <code>cond@B(j)</code> is satisfied, it would mean that the attacker has been able to forge the message <code>h(<d,secret>,key)</code> with <code>d</code> corresponding to the value of the counter at timepoint <code>B(j)</code>, because all messages outputted so far correspond to older values of <code>d</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step25">
<span class="input-line" id="in25"><br>Proof.</span>
<span class="output-line" id="out25">[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: j:index<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>) => <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">B(j)</span> => false<br><br></span>
</span>
<span class="squirrel-step" id="step26">
<span class="input-line" id="in26"> intro Hap Hcond.</span>
<span class="output-line" id="out26">[> Line 144: (intro Hap Hcond) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: j:index<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>Hcond: <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">B(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
<span class="com-line" id="com26"><p>We start by introducing the hypotheses and expanding the <code>cond</code> macro.</p>
</span>
</span>
<span class="squirrel-step" id="step27">
<span class="input-line" id="in27"><br> expand cond.</span>
<span class="output-line" id="out27">[> Line 145: (expand cond) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: j:index<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>Hcond: <span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span> = <span class="gf" style="font-weight: bold">h</span>(<<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<span class="gn" style="color: #AA5500">secret</span>>,<span class="gn" style="color: #AA5500">key</span>)<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
</span>
<span class="squirrel-step" id="step28">
<span class="input-line" id="in28"> euf Hcond => Ht Heq.</span>
<span class="output-line" id="out28">[> Line 147: ((euf Hcond);(intro Ht Heq)) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: i,j:index<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>Hcond: <span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span> = <span class="gf" style="font-weight: bold">h</span>(<<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<span class="gn" style="color: #AA5500">secret</span>>,<span class="gn" style="color: #AA5500">key</span>)<br>Heq: <<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>),<span class="gn" style="color: #AA5500">secret</span>> = <<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<span class="gn" style="color: #AA5500">secret</span>><br>Ht: <span class="ga" style="color: #00AA00">A(i)</span> < <span class="ga" style="color: #00AA00">B(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
<span class="com-line" id="com28"><p>Applying the <code>euf</code> tactic generates two new hypotheses, <code>Ht</code> and <code>Heq</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step29">
<span class="input-line" id="in29"> assert pred(A(i)) < pred(B(j)) as H by constraints.</span>
<span class="output-line" id="out29">[> Line 150: ((have (pred(A(i)) < pred(B(j))), H); 1: by constraints) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: i,j:index<br>H: <span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>) < <span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>Hcond: <span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span> = <span class="gf" style="font-weight: bold">h</span>(<<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<span class="gn" style="color: #AA5500">secret</span>>,<span class="gn" style="color: #AA5500">key</span>)<br>Heq: <<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>),<span class="gn" style="color: #AA5500">secret</span>> = <<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<span class="gn" style="color: #AA5500">secret</span>><br>Ht: <span class="ga" style="color: #00AA00">A(i)</span> < <span class="ga" style="color: #00AA00">B(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
<span class="com-line" id="com29"><p>We use here the counterIncrease lemma to show that the equality <code>Heq</code> is not possible.</p>
</span>
</span>
<span class="squirrel-step" id="step30">
<span class="input-line" id="in30"><br> apply counterIncrease in H.</span>
<span class="output-line" id="out30">[> Line 151: (apply ... in H) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: i,j:index<br>H: <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>) ~< <span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">B(j)</span>)<br>Hcond: <span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">B(j)</span> = <span class="gf" style="font-weight: bold">h</span>(<<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<span class="gn" style="color: #AA5500">secret</span>>,<span class="gn" style="color: #AA5500">key</span>)<br>Heq: <<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">A(i)</span>),<span class="gn" style="color: #AA5500">secret</span>> = <<span class="gm" style="font-weight: bold; color: #AA00AA">d</span>@<span class="gf" style="font-weight: bold">pred</span>(<span class="ga" style="color: #00AA00">B(j)</span>),<span class="gn" style="color: #AA5500">secret</span>><br>Ht: <span class="ga" style="color: #00AA00">A(i)</span> < <span class="ga" style="color: #00AA00">B(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
</span>
<span class="squirrel-step" id="step31">
<span class="input-line" id="in31"><br> by apply orderStrict in H.</span>
<span class="output-line" id="out31">[> Line 152: by (apply ... in H) <br>[goal> Goal secretReach is proved <br></span>
</span>
<span class="squirrel-step" id="step32">
<span class="input-line" id="in32"><br>Qed.</span>
<span class="output-line" id="out32">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>