|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Event}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isadelimproof |
|
19 % |
|
20 \endisadelimproof |
|
21 % |
|
22 \isatagproof |
|
23 % |
|
24 \endisatagproof |
|
25 {\isafoldproof}% |
|
26 % |
|
27 \isadelimproof |
|
28 % |
|
29 \endisadelimproof |
|
30 % |
|
31 \isadelimproof |
|
32 % |
|
33 \endisadelimproof |
|
34 % |
|
35 \isatagproof |
|
36 % |
|
37 \endisatagproof |
|
38 {\isafoldproof}% |
|
39 % |
|
40 \isadelimproof |
|
41 % |
|
42 \endisadelimproof |
|
43 % |
|
44 \isadelimproof |
|
45 % |
|
46 \endisadelimproof |
|
47 % |
|
48 \isatagproof |
|
49 % |
|
50 \endisatagproof |
|
51 {\isafoldproof}% |
|
52 % |
|
53 \isadelimproof |
|
54 % |
|
55 \endisadelimproof |
|
56 % |
|
57 \isadelimproof |
|
58 % |
|
59 \endisadelimproof |
|
60 % |
|
61 \isatagproof |
|
62 % |
|
63 \endisatagproof |
|
64 {\isafoldproof}% |
|
65 % |
|
66 \isadelimproof |
|
67 % |
|
68 \endisadelimproof |
|
69 % |
|
70 \isadelimproof |
|
71 % |
|
72 \endisadelimproof |
|
73 % |
|
74 \isatagproof |
|
75 % |
|
76 \endisatagproof |
|
77 {\isafoldproof}% |
|
78 % |
|
79 \isadelimproof |
|
80 % |
|
81 \endisadelimproof |
|
82 % |
|
83 \isadelimproof |
|
84 % |
|
85 \endisadelimproof |
|
86 % |
|
87 \isatagproof |
|
88 % |
|
89 \endisatagproof |
|
90 {\isafoldproof}% |
|
91 % |
|
92 \isadelimproof |
|
93 % |
|
94 \endisadelimproof |
|
95 % |
|
96 \isadelimproof |
|
97 % |
|
98 \endisadelimproof |
|
99 % |
|
100 \isatagproof |
|
101 % |
|
102 \endisatagproof |
|
103 {\isafoldproof}% |
|
104 % |
|
105 \isadelimproof |
|
106 % |
|
107 \endisadelimproof |
|
108 % |
|
109 \isadelimproof |
|
110 % |
|
111 \endisadelimproof |
|
112 % |
|
113 \isatagproof |
|
114 % |
|
115 \endisatagproof |
|
116 {\isafoldproof}% |
|
117 % |
|
118 \isadelimproof |
|
119 % |
|
120 \endisadelimproof |
|
121 % |
|
122 \isadelimproof |
|
123 % |
|
124 \endisadelimproof |
|
125 % |
|
126 \isatagproof |
|
127 % |
|
128 \endisatagproof |
|
129 {\isafoldproof}% |
|
130 % |
|
131 \isadelimproof |
|
132 % |
|
133 \endisadelimproof |
|
134 % |
|
135 \isadelimproof |
|
136 % |
|
137 \endisadelimproof |
|
138 % |
|
139 \isatagproof |
|
140 % |
|
141 \endisatagproof |
|
142 {\isafoldproof}% |
|
143 % |
|
144 \isadelimproof |
|
145 % |
|
146 \endisadelimproof |
|
147 % |
|
148 \isadelimproof |
|
149 % |
|
150 \endisadelimproof |
|
151 % |
|
152 \isatagproof |
|
153 % |
|
154 \endisatagproof |
|
155 {\isafoldproof}% |
|
156 % |
|
157 \isadelimproof |
|
158 % |
|
159 \endisadelimproof |
|
160 % |
|
161 \isadelimproof |
|
162 % |
|
163 \endisadelimproof |
|
164 % |
|
165 \isatagproof |
|
166 % |
|
167 \endisatagproof |
|
168 {\isafoldproof}% |
|
169 % |
|
170 \isadelimproof |
|
171 % |
|
172 \endisadelimproof |
|
173 % |
|
174 \isadelimproof |
|
175 % |
|
176 \endisadelimproof |
|
177 % |
|
178 \isatagproof |
|
179 % |
|
180 \endisatagproof |
|
181 {\isafoldproof}% |
|
182 % |
|
183 \isadelimproof |
|
184 % |
|
185 \endisadelimproof |
|
186 % |
|
187 \isadelimproof |
|
188 % |
|
189 \endisadelimproof |
|
190 % |
|
191 \isatagproof |
|
192 % |
|
193 \endisatagproof |
|
194 {\isafoldproof}% |
|
195 % |
|
196 \isadelimproof |
|
197 % |
|
198 \endisadelimproof |
|
199 % |
|
200 \isadelimproof |
|
201 % |
|
202 \endisadelimproof |
|
203 % |
|
204 \isatagproof |
|
205 % |
|
206 \endisatagproof |
|
207 {\isafoldproof}% |
|
208 % |
|
209 \isadelimproof |
|
210 % |
|
211 \endisadelimproof |
|
212 % |
|
213 \isadelimproof |
|
214 % |
|
215 \endisadelimproof |
|
216 % |
|
217 \isatagproof |
|
218 % |
|
219 \endisatagproof |
|
220 {\isafoldproof}% |
|
221 % |
|
222 \isadelimproof |
|
223 % |
|
224 \endisadelimproof |
|
225 % |
|
226 \isadelimproof |
|
227 % |
|
228 \endisadelimproof |
|
229 % |
|
230 \isatagproof |
|
231 % |
|
232 \endisatagproof |
|
233 {\isafoldproof}% |
|
234 % |
|
235 \isadelimproof |
|
236 % |
|
237 \endisadelimproof |
|
238 % |
|
239 \isadelimproof |
|
240 % |
|
241 \endisadelimproof |
|
242 % |
|
243 \isatagproof |
|
244 % |
|
245 \endisatagproof |
|
246 {\isafoldproof}% |
|
247 % |
|
248 \isadelimproof |
|
249 % |
|
250 \endisadelimproof |
|
251 % |
|
252 \isadelimproof |
|
253 % |
|
254 \endisadelimproof |
|
255 % |
|
256 \isatagproof |
|
257 % |
|
258 \endisatagproof |
|
259 {\isafoldproof}% |
|
260 % |
|
261 \isadelimproof |
|
262 % |
|
263 \endisadelimproof |
|
264 % |
|
265 \isadelimproof |
|
266 % |
|
267 \endisadelimproof |
|
268 % |
|
269 \isatagproof |
|
270 % |
|
271 \endisatagproof |
|
272 {\isafoldproof}% |
|
273 % |
|
274 \isadelimproof |
|
275 % |
|
276 \endisadelimproof |
|
277 % |
|
278 \isadelimproof |
|
279 % |
|
280 \endisadelimproof |
|
281 % |
|
282 \isatagproof |
|
283 % |
|
284 \endisatagproof |
|
285 {\isafoldproof}% |
|
286 % |
|
287 \isadelimproof |
|
288 % |
|
289 \endisadelimproof |
|
290 % |
|
291 \isadelimproof |
|
292 % |
|
293 \endisadelimproof |
|
294 % |
|
295 \isatagproof |
|
296 % |
|
297 \endisatagproof |
|
298 {\isafoldproof}% |
|
299 % |
|
300 \isadelimproof |
|
301 % |
|
302 \endisadelimproof |
|
303 % |
|
304 \isadelimproof |
|
305 % |
|
306 \endisadelimproof |
|
307 % |
|
308 \isatagproof |
|
309 % |
|
310 \endisatagproof |
|
311 {\isafoldproof}% |
|
312 % |
|
313 \isadelimproof |
|
314 % |
|
315 \endisadelimproof |
|
316 % |
|
317 \isadelimproof |
|
318 % |
|
319 \endisadelimproof |
|
320 % |
|
321 \isatagproof |
|
322 % |
|
323 \endisatagproof |
|
324 {\isafoldproof}% |
|
325 % |
|
326 \isadelimproof |
|
327 % |
|
328 \endisadelimproof |
|
329 % |
|
330 \isadelimproof |
|
331 % |
|
332 \endisadelimproof |
|
333 % |
|
334 \isatagproof |
|
335 % |
|
336 \endisatagproof |
|
337 {\isafoldproof}% |
|
338 % |
|
339 \isadelimproof |
|
340 % |
|
341 \endisadelimproof |
|
342 % |
|
343 \isadelimproof |
|
344 % |
|
345 \endisadelimproof |
|
346 % |
|
347 \isatagproof |
|
348 % |
|
349 \endisatagproof |
|
350 {\isafoldproof}% |
|
351 % |
|
352 \isadelimproof |
|
353 % |
|
354 \endisadelimproof |
|
355 % |
|
356 \isadelimproof |
|
357 % |
|
358 \endisadelimproof |
|
359 % |
|
360 \isatagproof |
|
361 % |
|
362 \endisatagproof |
|
363 {\isafoldproof}% |
|
364 % |
|
365 \isadelimproof |
|
366 % |
|
367 \endisadelimproof |
|
368 % |
|
369 \isadelimproof |
|
370 % |
|
371 \endisadelimproof |
|
372 % |
|
373 \isatagproof |
|
374 % |
|
375 \endisatagproof |
|
376 {\isafoldproof}% |
|
377 % |
|
378 \isadelimproof |
|
379 % |
|
380 \endisadelimproof |
|
381 % |
|
382 \isadelimML |
|
383 % |
|
384 \endisadelimML |
|
385 % |
|
386 \isatagML |
|
387 % |
|
388 \endisatagML |
|
389 {\isafoldML}% |
|
390 % |
|
391 \isadelimML |
|
392 % |
|
393 \endisadelimML |
|
394 % |
|
395 \isadelimproof |
|
396 % |
|
397 \endisadelimproof |
|
398 % |
|
399 \isatagproof |
|
400 % |
|
401 \endisatagproof |
|
402 {\isafoldproof}% |
|
403 % |
|
404 \isadelimproof |
|
405 % |
|
406 \endisadelimproof |
|
407 % |
|
408 \isadelimproof |
|
409 % |
|
410 \endisadelimproof |
|
411 % |
|
412 \isatagproof |
|
413 % |
|
414 \endisatagproof |
|
415 {\isafoldproof}% |
|
416 % |
|
417 \isadelimproof |
|
418 % |
|
419 \endisadelimproof |
|
420 % |
|
421 \isadelimproof |
|
422 % |
|
423 \endisadelimproof |
|
424 % |
|
425 \isatagproof |
|
426 % |
|
427 \endisatagproof |
|
428 {\isafoldproof}% |
|
429 % |
|
430 \isadelimproof |
|
431 % |
|
432 \endisadelimproof |
|
433 % |
|
434 \isadelimML |
|
435 % |
|
436 \endisadelimML |
|
437 % |
|
438 \isatagML |
|
439 % |
|
440 \endisatagML |
|
441 {\isafoldML}% |
|
442 % |
|
443 \isadelimML |
|
444 % |
|
445 \endisadelimML |
|
446 % |
|
447 \isadelimML |
|
448 % |
|
449 \endisadelimML |
|
450 % |
|
451 \isatagML |
|
452 % |
|
453 \endisatagML |
|
454 {\isafoldML}% |
|
455 % |
|
456 \isadelimML |
|
457 % |
|
458 \endisadelimML |
|
459 % |
|
460 \isamarkupsection{Event Traces \label{sec:events}% |
|
461 } |
|
462 \isamarkuptrue% |
|
463 % |
|
464 \begin{isamarkuptext}% |
|
465 The system's behaviour is formalized as a set of traces of |
|
466 \emph{events}. The most important event, \isa{Says\ A\ B\ X}, expresses |
|
467 $A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$. |
|
468 A trace is simply a list, constructed in reverse |
|
469 using~\isa{{\isaliteral{23}{\isacharhash}}}. Other event types include reception of messages (when |
|
470 we want to make it explicit) and an agent's storing a fact. |
|
471 |
|
472 Sometimes the protocol requires an agent to generate a new nonce. The |
|
473 probability that a 20-byte random number has appeared before is effectively |
|
474 zero. To formalize this important property, the set \isa{used\ evs} |
|
475 denotes the set of all items mentioned in the trace~\isa{evs}. |
|
476 The function \isa{used} has a straightforward |
|
477 recursive definition. Here is the case for \isa{Says} event: |
|
478 \begin{isabelle}% |
|
479 \ \ \ \ \ used\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ parts\ {\isaliteral{7B}{\isacharbraceleft}}X{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ used\ evs% |
|
480 \end{isabelle} |
|
481 |
|
482 The function \isa{knows} formalizes an agent's knowledge. Mostly we only |
|
483 care about the spy's knowledge, and \isa{knows\ Spy\ evs} is the set of items |
|
484 available to the spy in the trace~\isa{evs}. Already in the empty trace, |
|
485 the spy starts with some secrets at his disposal, such as the private keys |
|
486 of compromised users. After each \isa{Says} event, the spy learns the |
|
487 message that was sent: |
|
488 \begin{isabelle}% |
|
489 \ \ \ \ \ knows\ Spy\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ X\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}% |
|
490 \end{isabelle} |
|
491 Combinations of functions express other important |
|
492 sets of messages derived from~\isa{evs}: |
|
493 \begin{itemize} |
|
494 \item \isa{analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}} is everything that the spy could |
|
495 learn by decryption |
|
496 \item \isa{synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is everything that the spy |
|
497 could generate |
|
498 \end{itemize}% |
|
499 \end{isamarkuptext}% |
|
500 \isamarkuptrue% |
|
501 % |
|
502 \isadelimtheory |
|
503 % |
|
504 \endisadelimtheory |
|
505 % |
|
506 \isatagtheory |
|
507 % |
|
508 \endisatagtheory |
|
509 {\isafoldtheory}% |
|
510 % |
|
511 \isadelimtheory |
|
512 % |
|
513 \endisadelimtheory |
|
514 \end{isabellebody}% |
|
515 %%% Local Variables: |
|
516 %%% mode: latex |
|
517 %%% TeX-master: "root" |
|
518 %%% End: |