-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathsigned-ddh-S.html
More file actions
282 lines (233 loc) · 101 KB
/
Copy pathsigned-ddh-S.html
File metadata and controls
282 lines (233 loc) · 101 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
<!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">abstract ok : message<br>abstract ko : message<br><br>name skP : message<br>name skS : message<br><br>channel cP<br>channel cS<br><br>name a : index -> message<br>name b : index -> message<br>name k : index -> index -> message<br><br>ddh g, (^) where group:message exponents:message.</span>
<span class="output-line" id="out0"></span>
<span class="com-line" id="com0"><h1 id="signed-ddh">SIGNED DDH</h1>
<p>The signed DDH protocol as described in [G] features two roles, P and S. Each role is associated to a secret key (skP and skS).</p>
<ul>
<li>P -> S : <pk(skP), g^a></li>
<li>S -> P : <pk(skS),g<sup>b>,sign(<<g</sup>a,g^b>,pk(skP)>,skS)</li>
<li>P -> S : sign(<<g<sup>b,g</sup>a>,pk(skS)>,skP)</li>
</ul>
<p>We consider multiple sessions but two agents only (one agent for the role P and one agent for the role S) and show the strong secrecy of the shared key.</p>
<ul>
<li>In this file <code>signed-ddh-S.sp</code>, we show that the key g<sup>a</sup>b as computed by S is indistinguishable from g^k with k fresh (system secretS).</li>
<li>In another file <code>signed-ddh-P.sp</code>, we show that the key g<sup>a</sup>b as computed by P is indistinguishable from g^k with k fresh (system secretP).</li>
</ul>
<p>[G] ISO/IEC 9798-3:2019, IT Security techniques – Entity authentication – Part 3: Mechanisms using digital signature techniques.</p>
<hr />
<p>Declarations are identical to the ones in <code>signed-ddh-P.sp</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step1">
<span class="input-line" id="in1">signature sign,checksign,pk<br><br><br>process P(i:index) =<br> out(cP, <pk(skP),g^a(i)>);<br> in(cP, x2);<br> let gs = snd(fst(x2)) in<br> let pks = fst(fst(x2)) in<br> if checksign(snd(x2),pks) = <<g^a(i),gs>,pk(skP)> && pks = pk(skS) then<br> out(cP,sign(<<gs,g^a(i)>,pks>,skP))<br><br>process Schall(j:index) =<br> in(cS, x1);<br> let gp = snd(x1) in<br> let pkp = fst(x1) in<br> if pkp = pk(skP) then<br> out(cS, < <pk(skS),g^b(j)>, sign(<<gp,g^b(j)>,pkp>,skS)>);<br> in(cS, x3);<br> if checksign(x3,pkp) = <<g^b(j),gp>,pk(skS)> then<br> out(cS,ok);<br> in(cS, challenge);<br> try find i such that gp = g^a(i) in<br> out(cS, diff(g^a(i)^b(j),g^k(i,j)))<br> else<br> out(cS, diff(ok,ko))<br><br>system (!_i P(i) | !_j Schall(j)).</span>
<span class="output-line" id="out1">System before processing:<br> <br> (!_i <span class="pn" style="font-weight:bold; color: #0000AA">P</span> i) | (!_j <span class="pn" style="font-weight:bold; color: #0000AA">Schall</span> j)<br><br>System after processing:<br> <br> (!_i<br> P:<br> <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cP</span>,pair(pk(skP),(g ^ a(i))));<br> <span class="pio" style="font-weight: bold">in</span>(<span class="pc">cP</span>,<span class="pv" style="font-weight: bold; color: #AA00AA">x2</span>);<br> <span class="pk" style="font-weight: bold">let</span> <span class="pv" style="font-weight: bold; color: #AA00AA">gs</span> = snd(fst(x2)) <span class="pk" style="font-weight: bold">in</span><br> <span class="pk" style="font-weight: bold">let</span> <span class="pv" style="font-weight: bold; color: #AA00AA">pks</span> = fst(fst(x2)) <span class="pk" style="font-weight: bold">in</span><br> <span class="pc" style="text-decoration: underline; color: #AA0000">if</span> ((checksign(snd(x2),pks(i)) = pair(pair((g ^ a(i)),gs(i)),pk(skP)))<br> && (pks(i) = pk(skS))) <span class="pc" style="text-decoration: underline; color: #AA0000">then</span><br> P1: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cP</span>,sign(pair(pair(gs(i),(g ^ a(i))),pks(i)),skP)); <span class="pn" style="font-weight:bold; color: #0000AA">null</span> <span class="pc" style="text-decoration: underline; color: #AA0000">else</span><br> P2: <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">cS</span>,<span class="pv" style="font-weight: bold; color: #AA00AA">x1</span>);<br> <span class="pk" style="font-weight: bold">let</span> <span class="pv" style="font-weight: bold; color: #AA00AA">gp</span> = snd(x1) <span class="pk" style="font-weight: bold">in</span><br> <span class="pk" style="font-weight: bold">let</span> <span class="pv" style="font-weight: bold; color: #AA00AA">pkp</span> = fst(x1) <span class="pk" style="font-weight: bold">in</span><br> <span class="pc" style="text-decoration: underline; color: #AA0000">if</span> (pkp(j) = pk(skP)) <span class="pc" style="text-decoration: underline; color: #AA0000">then</span><br> Schall:<br> <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cS</span>,<br> pair(pair(pk(skS),(g ^ b(j))),<br> sign(pair(pair(gp(j),(g ^ b(j))),pkp(j)),skS)));<br> <span class="pio" style="font-weight: bold">in</span>(<span class="pc">cS</span>,<span class="pv" style="font-weight: bold; color: #AA00AA">x3</span>);<br> <span class="pc" style="text-decoration: underline; color: #AA0000">if</span> (checksign(x3,pkp(j)) = pair(pair((g ^ b(j)),gp(j)),pk(skS))) <span class="pc" style="text-decoration: underline; color: #AA0000">then</span><br> Schall1:<br> <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cS</span>,ok);<br> <span class="pio" style="font-weight: bold">in</span>(<span class="pc">cS</span>,<span class="pv" style="font-weight: bold; color: #AA00AA">challenge</span>);<br> <span class="pc" style="text-decoration: underline; color: #AA0000">find</span> (i) <span class="pc" style="text-decoration: underline; color: #AA0000">such that</span> (gp(j) = (g ^ a(i))) <span class="pc" style="text-decoration: underline; color: #AA0000">in</span><br> Schall2: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cS</span>,<span>diff</span>(((g ^ a(i)) ^ b(j)),(g ^ k(i,j)))); <span class="pn" style="font-weight:bold; color: #0000AA">null</span> <span class="pc" style="text-decoration: underline; color: #AA0000">else</span><br> Schall3: <span class="pio" style="font-weight: bold">out</span>(<span class="pc">cS</span>,<span>diff</span>(ok,ko)); <span class="pn" style="font-weight:bold; color: #0000AA">null</span> <span class="pc" style="text-decoration: underline; color: #AA0000">else</span> Schall4: <span class="pn" style="font-weight:bold; color: #0000AA">null</span> <span class="pc" style="text-decoration: underline; color: #AA0000">else</span><br> Schall5: <span class="pn" style="font-weight:bold; color: #0000AA">null</span>)<br><br>System default registered with actions (init,P,P1,P2,Schall,Schall1,Schall2,<br> Schall3,Schall4,Schall5).<br></span>
<span class="com-line" id="com1"><p>The system <code>secretS</code> is the counterpart of the system <code>secretP</code> defined in the file <code>signed-ddh-P.sp</code>.</p>
<p>This time, we add an output at the end of the role of S.</p>
</span>
</span>
<span class="squirrel-step" id="step2">
<span class="input-line" id="in2"><br><br>include Basic.</span>
<span class="output-line" id="out2">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>
<span class="squirrel-step" id="step3">
<span class="input-line" id="in3">goal S_charac (j:index):<br> happens(Schall1(j)) =><br> exec@Schall1(j) =><br> exists (i:index), snd(input@Schall(j)) = g^a(i).</span>
<span class="output-line" id="out3">Goal S_charac :<br> <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall1(j)</span>) =><br> <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span> => exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br></span>
<span class="com-line" id="com3"><p>In the proof of strong secrecy for the system <code>secretS</code>, we will use the following property, stating that whenever S accepts a message from P, this message is of the form <code><<_,x>,_></code> where <code>x = g^a(i)</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step4">
<span class="input-line" id="in4"><br>Proof.</span>
<span class="output-line" id="out4">[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">Schall1(j)</span>) =><br><span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span> => exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step5">
<span class="input-line" id="in5"><br> intro Hap Hexec.</span>
<span class="output-line" id="out5">[> Line 87: (intro Hap Hexec) <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">Schall1(j)</span>)<br>Hexec: <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step6">
<span class="input-line" id="in6"><br> executable pred(Schall1(j)) => //.</span>
<span class="output-line" id="out6">[> Line 88: ((executable pred(Schall1(j)));(intro //)) <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">Schall1(j)</span>)<br>Hexec: <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t) =><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step7">
<span class="input-line" id="in7"><br> depends Schall(j), Schall1(j) => //.</span>
<span class="output-line" id="out7">[> Line 89: ((depends Schall(j), Schall1(j));(intro //)) <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">Schall1(j)</span>)<br>Hexec: <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span> =><br>(forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t) =><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step8">
<span class="input-line" id="in8"><br> intro Ord Hexec'.</span>
<span class="output-line" id="out8">[> Line 90: (intro Ord Hexec') <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">Schall1(j)</span>)<br>Hexec: <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step9">
<span class="input-line" id="in9"><br> use Hexec' with Schall(j) as Hyp => //.</span>
<span class="output-line" id="out9">[> Line 91: ((have ... as Hyp);(intro //)) <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">Schall1(j)</span>)<br>Hexec: <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hyp: <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall(j)</span><br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step10">
<span class="input-line" id="in10"><br> expand exec, cond, pkp(j)@Schall1(j).</span>
<span class="output-line" id="out10">[> Line 92: (expand exec, cond, pkp(j)@Schall1(j)) <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">Schall1(j)</span>)<br>Hexec: <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">Schall1(j)</span>) &&<br> <span class="gf" style="font-weight: bold">checksign</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">Schall1(j)</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">Schall(j)</span>)) =<br> <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)><br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hyp: <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">Schall(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">pkp</span>(j)@<span class="ga" style="color: #00AA00">Schall(j)</span> = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step11">
<span class="input-line" id="in11"><br> assert fst(input@Schall(j)) = pk(skP) as Meq' => //.</span>
<span class="output-line" id="out11">[> Line 93: ((have (fst(input@Schall(j)) = pk(skP)), Meq');(intro //)) <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">Schall1(j)</span>)<br>Hexec: <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">Schall1(j)</span>) &&<br> <span class="gf" style="font-weight: bold">checksign</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">Schall1(j)</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">Schall(j)</span>)) =<br> <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)><br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hyp: <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">Schall(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">pkp</span>(j)@<span class="ga" style="color: #00AA00">Schall(j)</span> = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Meq': <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step12">
<span class="input-line" id="in12"><br> rewrite Meq' in Hexec.</span>
<span class="output-line" id="out12">[> Line 94: (rewrite ... in Hexec) <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">Schall1(j)</span>)<br>Hexec: <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">Schall1(j)</span>) &&<br> <span class="gf" style="font-weight: bold">checksign</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)) =<br> <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)><br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hyp: <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">Schall(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">pkp</span>(j)@<span class="ga" style="color: #00AA00">Schall(j)</span> = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Meq': <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step13">
<span class="input-line" id="in13"> destruct Hexec as [Hexec Hcheck].</span>
<span class="output-line" id="out13">[> Line 94: (destruct Hexec, [Hexec Hcheck]) <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">Schall1(j)</span>)<br>Hcheck: <span class="gf" style="font-weight: bold">checksign</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)) =<br> <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)><br>Hexec: <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">Schall1(j)</span>)<br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hyp: <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">Schall(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">pkp</span>(j)@<span class="ga" style="color: #00AA00">Schall(j)</span> = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Meq': <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step14">
<span class="input-line" id="in14"><br> euf Hcheck.</span>
<span class="output-line" id="out14">[> Line 95: (euf Hcheck) <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">Schall1(j)</span>)<br>Hcheck: <span class="gf" style="font-weight: bold">checksign</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)) =<br> <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)><br>Hexec: <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">Schall1(j)</span>)<br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hyp: <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">Schall(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">pkp</span>(j)@<span class="ga" style="color: #00AA00">Schall(j)</span> = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Meq': <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="ga" style="color: #00AA00">P1(i)</span> <= <span class="ga" style="color: #00AA00">Schall1(j)</span> || <span class="ga" style="color: #00AA00">P1(i)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span> =><br><<<span class="gm" style="font-weight: bold; color: #AA00AA">gs</span>(i)@<span class="ga" style="color: #00AA00">P1(i)</span>,<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)>,<span class="gm" style="font-weight: bold; color: #AA00AA">pks</span>(i)@<span class="ga" style="color: #00AA00">P1(i)</span>> = <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)> =><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step15">
<span class="input-line" id="in15"><br> intro *.</span>
<span class="output-line" id="out15">[> Line 96: (intro *) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/right<br>Variables: i,j:index<br>H: <span class="ga" style="color: #00AA00">P1(i)</span> <= <span class="ga" style="color: #00AA00">Schall1(j)</span> || <span class="ga" style="color: #00AA00">P1(i)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br>Hap: <span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall1(j)</span>)<br>Hcheck: <span class="gf" style="font-weight: bold">checksign</span>(<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)) =<br> <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)><br>Hexec: <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">Schall1(j)</span>)<br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall1(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hyp: <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">Schall(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">pkp</span>(j)@<span class="ga" style="color: #00AA00">Schall(j)</span> = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Meq: <<<span class="gm" style="font-weight: bold; color: #AA00AA">gs</span>(i)@<span class="ga" style="color: #00AA00">P1(i)</span>,<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)>,<span class="gm" style="font-weight: bold; color: #AA00AA">pks</span>(i)@<span class="ga" style="color: #00AA00">P1(i)</span>> =<br> <<<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j),<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall1(j)</span>>,<span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skS</span>)><br>Meq': <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">pk</span>(<span class="gn" style="color: #AA5500">skP</span>)<br>Ord: <span class="ga" style="color: #00AA00">Schall(j)</span> < <span class="ga" style="color: #00AA00">Schall1(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>exists (i:index), <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)<br><br></span>
</span>
<span class="squirrel-step" id="step16">
<span class="input-line" id="in16"><br> by exists i.</span>
<span class="output-line" id="out16">[> Line 97: by (exists i) <br>[goal> Goal S_charac is proved <br></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 strongSecS.</span>
<span class="output-line" id="out18">Goal strongSecS :<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 show the counterpart of the property <code>strongSecP</code>, this time for the system <code>secretS</code>. The proof is carried out exactly in the same way.</p>
</span>
</span>
<span class="squirrel-step" id="step19">
<span class="input-line" id="in19"><br>Proof.</span>
<span class="output-line" id="out19">[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: t:timestamp<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(t)]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@t<br><br><br></span>
</span>
<span class="squirrel-step" id="step20">
<span class="input-line" id="in20"><br> enrich<br> skP, skS,<br> seq(i:index ->g^a(i)),<br> seq(j:index ->g^b(j)),<br> seq(i,j:index ->diff( g ^ a(i), g) ^ diff( b(j), k(i,j))).</span>
<span class="output-line" id="out20">[> Line 110: (enrich skP, skS, <span>seq</span>(i:index->(g ^ a(i))),<br> <span>seq</span>(j:index->(g ^ b(j))),<br> <span>seq</span>(i,j:index->(<span>diff</span>((g ^ a(i)),g) ^ <span>diff</span>(b(j),k(i,j)))))<br><br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: t:timestamp<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(t)]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br>5: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@t<br><br><br></span>
</span>
<span class="squirrel-step" id="step21">
<span class="input-line" id="in21"><br><br> induction t; try (by expandall; apply IH).</span>
<span class="output-line" id="out21">[> Line 112: ((induction t);(try by (expandall;(apply ... )))) <br>[goal> Focused goal (1/2):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">init</span>)]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br>5: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">init</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step22">
<span class="input-line" id="in22"><br><br> + (* init *)<br> expandall.</span>
<span class="output-line" id="out22">[> Line 115: expandall <br>[goal> Focused goal (1/2):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">init</span>)]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step23">
<span class="input-line" id="in23"><br> by ddh g,a,b,k.</span>
<span class="output-line" id="out23">[> Line 116: by (ddh g, a, b, k) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br>5: <span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@<span class="ga" style="color: #00AA00">Schall3(j)</span><br><br><br></span>
</span>
<span class="squirrel-step" id="step24">
<span class="input-line" id="in24"><br><br> + (* Schall3 *)<br> expand frame, exec, output.</span>
<span class="output-line" id="out24">[> Line 119: (expand frame, exec, output) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br>5: <<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">Schall3(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">Schall3(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">Schall3(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">Schall3(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">Schall3(j)</span>) then diff(<span class="gf" style="font-weight: bold">ok</span>, <span class="gf" style="font-weight: bold">ko</span>)>><br><br><br></span>
</span>
<span class="squirrel-step" id="step25">
<span class="input-line" id="in25"><br> have ->: (exec@pred(Schall3(j)) && cond@Schall3(j)) <=> False.</span>
<span class="output-line" id="out25">[> Line 120: (have ((exec@pred(Schall3(j)) && cond@Schall3(j)) <=> <span>False</span>),<br> ->)<br><br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><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">Schall3(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">Schall3(j)</span> <=> false<br><br></span>
</span>
<span class="squirrel-step" id="step26">
<span class="input-line" id="in26"><br> {split => //.</span>
<span class="output-line" id="out26">[> Line 121: (split;(intro //)) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><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">Schall3(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">Schall3(j)</span> => false<br><br></span>
</span>
<span class="squirrel-step" id="step27">
<span class="input-line" id="in27"> <br> intro [Hexec Hcond].</span>
<span class="output-line" id="out27">[> Line 122: (intro [Hexec Hcond]) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">Schall3(j)</span><br>Hexec: <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">Schall3(j)</span>)<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</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"><br> expand cond.</span>
<span class="output-line" id="out28">[> Line 123: (expand cond) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
</span>
<span class="squirrel-step" id="step29">
<span class="input-line" id="in29"><br> depends Schall1(j), Schall3(j) => //.</span>
<span class="output-line" id="out29">[> Line 124: ((depends Schall1(j), Schall3(j));(intro //)) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="ga" style="color: #00AA00">Schall1(j)</span> < <span class="ga" style="color: #00AA00">Schall3(j)</span> => false<br><br></span>
</span>
<span class="squirrel-step" id="step30">
<span class="input-line" id="in30"><br> intro Ord.</span>
<span class="output-line" id="out30">[> Line 125: (intro Ord) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br>Ord: <span class="ga" style="color: #00AA00">Schall1(j)</span> < <span class="ga" style="color: #00AA00">Schall3(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> executable pred(Schall3(j)) => //.</span>
<span class="output-line" id="out31">[> Line 126: ((executable pred(Schall3(j)));(intro //)) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br>Ord: <span class="ga" style="color: #00AA00">Schall1(j)</span> < <span class="ga" style="color: #00AA00">Schall3(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>(forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall3(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t) => false<br><br></span>
</span>
<span class="squirrel-step" id="step32">
<span class="input-line" id="in32"><br> intro Hexec'.</span>
<span class="output-line" id="out32">[> Line 127: (intro Hexec') <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall3(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br>Ord: <span class="ga" style="color: #00AA00">Schall1(j)</span> < <span class="ga" style="color: #00AA00">Schall3(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
</span>
<span class="squirrel-step" id="step33">
<span class="input-line" id="in33"><br> use Hexec' with Schall1(j) as Hexec1 => //.</span>
<span class="output-line" id="out33">[> Line 128: ((have ... as Hexec1);(intro //)) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall3(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hexec1: <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br>Ord: <span class="ga" style="color: #00AA00">Schall1(j)</span> < <span class="ga" style="color: #00AA00">Schall3(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
</span>
<span class="squirrel-step" id="step34">
<span class="input-line" id="in34"><br> expand exec.</span>
<span class="output-line" id="out34">[> Line 129: (expand exec) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall3(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hexec1: <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">Schall1(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br>Ord: <span class="ga" style="color: #00AA00">Schall1(j)</span> < <span class="ga" style="color: #00AA00">Schall3(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
</span>
<span class="squirrel-step" id="step35">
<span class="input-line" id="in35"><br> use S_charac with j as [j0 Hyp] => //.</span>
<span class="output-line" id="out35">[> Line 130: ((have ... as [j0 Hyp]);(intro //)) <br>[goal> Focused goal (1/2):<br>System: left:default/left, right:default/right (same for equivalences)<br>Variables: j,j0:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>Hcond: forall (i:index), not(<span class="gm" style="font-weight: bold; color: #AA00AA">gp</span>(j)@<span class="ga" style="color: #00AA00">Schall3(j)</span> = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))<br>Hexec: <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">Schall3(j)</span>)<br>Hexec': forall (t:timestamp), t < <span class="ga" style="color: #00AA00">Schall3(j)</span> => <span class="gm" style="font-weight: bold; color: #AA00AA">exec</span>@t<br>Hexec1: <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">Schall1(j)</span>) && <span class="gm" style="font-weight: bold; color: #AA00AA">cond</span>@<span class="ga" style="color: #00AA00">Schall1(j)</span><br>Hyp: <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">Schall(j)</span>) = <span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(j0)<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br>Ord: <span class="ga" style="color: #00AA00">Schall1(j)</span> < <span class="ga" style="color: #00AA00">Schall3(j)</span><br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
</span>
<span class="squirrel-step" id="step36">
<span class="input-line" id="in36"><br> by use Hcond with j0.</span>
<span class="output-line" id="out36">[> Line 131: by (have ... as ) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br>5: <<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">Schall3(j)</span>),<<span class="gf" style="font-weight: bold">of_bool</span>(false),if false then diff(<span class="gf" style="font-weight: bold">ok</span>, <span class="gf" style="font-weight: bold">ko</span>)>><br><br><br></span>
</span>
<span class="squirrel-step" id="step37">
<span class="input-line" id="in37">}<br><br> fa 5.</span>
<span class="output-line" id="out37">[> Line 133: (fa 5) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br>5: <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">Schall3(j)</span>)<br>6: <<span class="gf" style="font-weight: bold">of_bool</span>(false),if false then diff(<span class="gf" style="font-weight: bold">ok</span>, <span class="gf" style="font-weight: bold">ko</span>)><br><br><br></span>
</span>
<span class="squirrel-step" id="step38">
<span class="input-line" id="in38"> fa 6.</span>
<span class="output-line" id="out38">[> Line 133: (fa 6) <br>[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/right (same for equivalences)<br>Variables: j:index<br>H: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="ga" style="color: #00AA00">Schall3(j)</span>)]<br>IH: equiv(seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j)))),<br> seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j))), seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i))), <span class="gn" style="color: #AA5500">skS</span>, <span class="gn" style="color: #AA5500">skP</span>,<br> <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">Schall3(j)</span>))<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>0: seq(i,j:index->(diff(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i), <span class="gf" style="font-weight: bold">g</span>) ^ diff(<span class="gn" style="color: #AA5500">b</span>(j), <span class="gn" style="color: #AA5500">k</span>(i,j))))<br>1: seq(j:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">b</span>(j)))<br>2: seq(i:index->(<span class="gf" style="font-weight: bold">g</span> ^ <span class="gn" style="color: #AA5500">a</span>(i)))<br>3: <span class="gn" style="color: #AA5500">skS</span><br>4: <span class="gn" style="color: #AA5500">skP</span><br>5: <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">Schall3(j)</span>)<br>6: if false then diff(<span class="gf" style="font-weight: bold">ok</span>, <span class="gf" style="font-weight: bold">ko</span>)<br><br><br></span>
</span>
<span class="squirrel-step" id="step39">
<span class="input-line" id="in39"><br> by rewrite if_false.</span>
<span class="output-line" id="out39">[> Line 134: by (rewrite ...) <br>[goal> Goal strongSecS is proved <br></span>
</span>
<span class="squirrel-step" id="step40">
<span class="input-line" id="in40"><br>Qed.</span>
<span class="output-line" id="out40">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>