|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Message}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isadelimML |
|
19 % |
|
20 \endisadelimML |
|
21 % |
|
22 \isatagML |
|
23 % |
|
24 \endisatagML |
|
25 {\isafoldML}% |
|
26 % |
|
27 \isadelimML |
|
28 % |
|
29 \endisadelimML |
|
30 % |
|
31 \isadelimproof |
|
32 % |
|
33 \endisadelimproof |
|
34 % |
|
35 \isatagproof |
|
36 % |
|
37 \endisatagproof |
|
38 {\isafoldproof}% |
|
39 % |
|
40 \isadelimproof |
|
41 % |
|
42 \endisadelimproof |
|
43 % |
|
44 \isamarkupsection{Agents and Messages% |
|
45 } |
|
46 \isamarkuptrue% |
|
47 % |
|
48 \begin{isamarkuptext}% |
|
49 All protocol specifications refer to a syntactic theory of messages. |
|
50 Datatype |
|
51 \isa{agent} introduces the constant \isa{Server} (a trusted central |
|
52 machine, needed for some protocols), an infinite population of |
|
53 friendly agents, and the~\isa{Spy}:% |
|
54 \end{isamarkuptext}% |
|
55 \isamarkuptrue% |
|
56 \isacommand{datatype}\isamarkupfalse% |
|
57 \ agent\ {\isaliteral{3D}{\isacharequal}}\ Server\ {\isaliteral{7C}{\isacharbar}}\ Friend\ nat\ {\isaliteral{7C}{\isacharbar}}\ Spy% |
|
58 \begin{isamarkuptext}% |
|
59 Keys are just natural numbers. Function \isa{invKey} maps a public key to |
|
60 the matching private key, and vice versa:% |
|
61 \end{isamarkuptext}% |
|
62 \isamarkuptrue% |
|
63 \isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse% |
|
64 \ key\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline |
|
65 \isacommand{consts}\isamarkupfalse% |
|
66 \ invKey\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}key\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}% |
|
67 \isadelimproof |
|
68 % |
|
69 \endisadelimproof |
|
70 % |
|
71 \isatagproof |
|
72 % |
|
73 \endisatagproof |
|
74 {\isafoldproof}% |
|
75 % |
|
76 \isadelimproof |
|
77 % |
|
78 \endisadelimproof |
|
79 % |
|
80 \begin{isamarkuptext}% |
|
81 Datatype |
|
82 \isa{msg} introduces the message forms, which include agent names, nonces, |
|
83 keys, compound messages, and encryptions.% |
|
84 \end{isamarkuptext}% |
|
85 \isamarkuptrue% |
|
86 \isacommand{datatype}\isamarkupfalse% |
|
87 \isanewline |
|
88 \ \ \ \ \ msg\ {\isaliteral{3D}{\isacharequal}}\ Agent\ \ agent\isanewline |
|
89 \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Nonce\ \ nat\isanewline |
|
90 \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Key\ \ \ \ key\isanewline |
|
91 \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ MPair\ \ msg\ msg\isanewline |
|
92 \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Crypt\ \ key\ msg% |
|
93 \begin{isamarkuptext}% |
|
94 \noindent |
|
95 The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ |
|
96 abbreviates |
|
97 $\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. |
|
98 |
|
99 Since datatype constructors are injective, we have the theorem |
|
100 \begin{isabelle}% |
|
101 Crypt\ K\ X\ {\isaliteral{3D}{\isacharequal}}\ Crypt\ K{\isaliteral{27}{\isacharprime}}\ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ K\ {\isaliteral{3D}{\isacharequal}}\ K{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ X\ {\isaliteral{3D}{\isacharequal}}\ X{\isaliteral{27}{\isacharprime}}% |
|
102 \end{isabelle} |
|
103 A ciphertext can be decrypted using only one key and |
|
104 can yield only one plaintext. In the real world, decryption with the |
|
105 wrong key succeeds but yields garbage. Our model of encryption is |
|
106 realistic if encryption adds some redundancy to the plaintext, such as a |
|
107 checksum, so that garbage can be detected.% |
|
108 \end{isamarkuptext}% |
|
109 \isamarkuptrue% |
|
110 % |
|
111 \isadelimproof |
|
112 % |
|
113 \endisadelimproof |
|
114 % |
|
115 \isatagproof |
|
116 % |
|
117 \endisatagproof |
|
118 {\isafoldproof}% |
|
119 % |
|
120 \isadelimproof |
|
121 % |
|
122 \endisadelimproof |
|
123 % |
|
124 \isadelimproof |
|
125 % |
|
126 \endisadelimproof |
|
127 % |
|
128 \isatagproof |
|
129 % |
|
130 \endisatagproof |
|
131 {\isafoldproof}% |
|
132 % |
|
133 \isadelimproof |
|
134 % |
|
135 \endisadelimproof |
|
136 % |
|
137 \isadelimproof |
|
138 % |
|
139 \endisadelimproof |
|
140 % |
|
141 \isatagproof |
|
142 % |
|
143 \endisatagproof |
|
144 {\isafoldproof}% |
|
145 % |
|
146 \isadelimproof |
|
147 % |
|
148 \endisadelimproof |
|
149 % |
|
150 \isadelimproof |
|
151 % |
|
152 \endisadelimproof |
|
153 % |
|
154 \isatagproof |
|
155 % |
|
156 \endisatagproof |
|
157 {\isafoldproof}% |
|
158 % |
|
159 \isadelimproof |
|
160 % |
|
161 \endisadelimproof |
|
162 % |
|
163 \isadelimproof |
|
164 % |
|
165 \endisadelimproof |
|
166 % |
|
167 \isatagproof |
|
168 % |
|
169 \endisatagproof |
|
170 {\isafoldproof}% |
|
171 % |
|
172 \isadelimproof |
|
173 % |
|
174 \endisadelimproof |
|
175 % |
|
176 \isadelimproof |
|
177 % |
|
178 \endisadelimproof |
|
179 % |
|
180 \isatagproof |
|
181 % |
|
182 \endisatagproof |
|
183 {\isafoldproof}% |
|
184 % |
|
185 \isadelimproof |
|
186 % |
|
187 \endisadelimproof |
|
188 % |
|
189 \isadelimproof |
|
190 % |
|
191 \endisadelimproof |
|
192 % |
|
193 \isatagproof |
|
194 % |
|
195 \endisatagproof |
|
196 {\isafoldproof}% |
|
197 % |
|
198 \isadelimproof |
|
199 % |
|
200 \endisadelimproof |
|
201 % |
|
202 \isadelimproof |
|
203 % |
|
204 \endisadelimproof |
|
205 % |
|
206 \isatagproof |
|
207 % |
|
208 \endisatagproof |
|
209 {\isafoldproof}% |
|
210 % |
|
211 \isadelimproof |
|
212 % |
|
213 \endisadelimproof |
|
214 % |
|
215 \isadelimproof |
|
216 % |
|
217 \endisadelimproof |
|
218 % |
|
219 \isatagproof |
|
220 % |
|
221 \endisatagproof |
|
222 {\isafoldproof}% |
|
223 % |
|
224 \isadelimproof |
|
225 % |
|
226 \endisadelimproof |
|
227 % |
|
228 \isadelimproof |
|
229 % |
|
230 \endisadelimproof |
|
231 % |
|
232 \isatagproof |
|
233 % |
|
234 \endisatagproof |
|
235 {\isafoldproof}% |
|
236 % |
|
237 \isadelimproof |
|
238 % |
|
239 \endisadelimproof |
|
240 % |
|
241 \isadelimproof |
|
242 % |
|
243 \endisadelimproof |
|
244 % |
|
245 \isatagproof |
|
246 % |
|
247 \endisatagproof |
|
248 {\isafoldproof}% |
|
249 % |
|
250 \isadelimproof |
|
251 % |
|
252 \endisadelimproof |
|
253 % |
|
254 \isadelimproof |
|
255 % |
|
256 \endisadelimproof |
|
257 % |
|
258 \isatagproof |
|
259 % |
|
260 \endisatagproof |
|
261 {\isafoldproof}% |
|
262 % |
|
263 \isadelimproof |
|
264 % |
|
265 \endisadelimproof |
|
266 % |
|
267 \isadelimproof |
|
268 % |
|
269 \endisadelimproof |
|
270 % |
|
271 \isatagproof |
|
272 % |
|
273 \endisatagproof |
|
274 {\isafoldproof}% |
|
275 % |
|
276 \isadelimproof |
|
277 % |
|
278 \endisadelimproof |
|
279 % |
|
280 \isadelimproof |
|
281 % |
|
282 \endisadelimproof |
|
283 % |
|
284 \isatagproof |
|
285 % |
|
286 \endisatagproof |
|
287 {\isafoldproof}% |
|
288 % |
|
289 \isadelimproof |
|
290 % |
|
291 \endisadelimproof |
|
292 % |
|
293 \isadelimproof |
|
294 % |
|
295 \endisadelimproof |
|
296 % |
|
297 \isatagproof |
|
298 % |
|
299 \endisatagproof |
|
300 {\isafoldproof}% |
|
301 % |
|
302 \isadelimproof |
|
303 % |
|
304 \endisadelimproof |
|
305 % |
|
306 \isadelimproof |
|
307 % |
|
308 \endisadelimproof |
|
309 % |
|
310 \isatagproof |
|
311 % |
|
312 \endisatagproof |
|
313 {\isafoldproof}% |
|
314 % |
|
315 \isadelimproof |
|
316 % |
|
317 \endisadelimproof |
|
318 % |
|
319 \isadelimproof |
|
320 % |
|
321 \endisadelimproof |
|
322 % |
|
323 \isatagproof |
|
324 % |
|
325 \endisatagproof |
|
326 {\isafoldproof}% |
|
327 % |
|
328 \isadelimproof |
|
329 % |
|
330 \endisadelimproof |
|
331 % |
|
332 \isadelimproof |
|
333 % |
|
334 \endisadelimproof |
|
335 % |
|
336 \isatagproof |
|
337 % |
|
338 \endisatagproof |
|
339 {\isafoldproof}% |
|
340 % |
|
341 \isadelimproof |
|
342 % |
|
343 \endisadelimproof |
|
344 % |
|
345 \isadelimproof |
|
346 % |
|
347 \endisadelimproof |
|
348 % |
|
349 \isatagproof |
|
350 % |
|
351 \endisatagproof |
|
352 {\isafoldproof}% |
|
353 % |
|
354 \isadelimproof |
|
355 % |
|
356 \endisadelimproof |
|
357 % |
|
358 \isadelimproof |
|
359 % |
|
360 \endisadelimproof |
|
361 % |
|
362 \isatagproof |
|
363 % |
|
364 \endisatagproof |
|
365 {\isafoldproof}% |
|
366 % |
|
367 \isadelimproof |
|
368 % |
|
369 \endisadelimproof |
|
370 % |
|
371 \isadelimproof |
|
372 % |
|
373 \endisadelimproof |
|
374 % |
|
375 \isatagproof |
|
376 % |
|
377 \endisatagproof |
|
378 {\isafoldproof}% |
|
379 % |
|
380 \isadelimproof |
|
381 % |
|
382 \endisadelimproof |
|
383 % |
|
384 \isadelimproof |
|
385 % |
|
386 \endisadelimproof |
|
387 % |
|
388 \isatagproof |
|
389 % |
|
390 \endisatagproof |
|
391 {\isafoldproof}% |
|
392 % |
|
393 \isadelimproof |
|
394 % |
|
395 \endisadelimproof |
|
396 % |
|
397 \isadelimproof |
|
398 % |
|
399 \endisadelimproof |
|
400 % |
|
401 \isatagproof |
|
402 % |
|
403 \endisatagproof |
|
404 {\isafoldproof}% |
|
405 % |
|
406 \isadelimproof |
|
407 % |
|
408 \endisadelimproof |
|
409 % |
|
410 \isadelimproof |
|
411 % |
|
412 \endisadelimproof |
|
413 % |
|
414 \isatagproof |
|
415 % |
|
416 \endisatagproof |
|
417 {\isafoldproof}% |
|
418 % |
|
419 \isadelimproof |
|
420 % |
|
421 \endisadelimproof |
|
422 % |
|
423 \isadelimproof |
|
424 % |
|
425 \endisadelimproof |
|
426 % |
|
427 \isatagproof |
|
428 % |
|
429 \endisatagproof |
|
430 {\isafoldproof}% |
|
431 % |
|
432 \isadelimproof |
|
433 % |
|
434 \endisadelimproof |
|
435 % |
|
436 \isadelimproof |
|
437 % |
|
438 \endisadelimproof |
|
439 % |
|
440 \isatagproof |
|
441 % |
|
442 \endisatagproof |
|
443 {\isafoldproof}% |
|
444 % |
|
445 \isadelimproof |
|
446 % |
|
447 \endisadelimproof |
|
448 % |
|
449 \isadelimproof |
|
450 % |
|
451 \endisadelimproof |
|
452 % |
|
453 \isatagproof |
|
454 % |
|
455 \endisatagproof |
|
456 {\isafoldproof}% |
|
457 % |
|
458 \isadelimproof |
|
459 % |
|
460 \endisadelimproof |
|
461 % |
|
462 \isadelimproof |
|
463 % |
|
464 \endisadelimproof |
|
465 % |
|
466 \isatagproof |
|
467 % |
|
468 \endisatagproof |
|
469 {\isafoldproof}% |
|
470 % |
|
471 \isadelimproof |
|
472 % |
|
473 \endisadelimproof |
|
474 % |
|
475 \isadelimproof |
|
476 % |
|
477 \endisadelimproof |
|
478 % |
|
479 \isatagproof |
|
480 % |
|
481 \endisatagproof |
|
482 {\isafoldproof}% |
|
483 % |
|
484 \isadelimproof |
|
485 % |
|
486 \endisadelimproof |
|
487 % |
|
488 \isadelimproof |
|
489 % |
|
490 \endisadelimproof |
|
491 % |
|
492 \isatagproof |
|
493 % |
|
494 \endisatagproof |
|
495 {\isafoldproof}% |
|
496 % |
|
497 \isadelimproof |
|
498 % |
|
499 \endisadelimproof |
|
500 % |
|
501 \isadelimproof |
|
502 % |
|
503 \endisadelimproof |
|
504 % |
|
505 \isatagproof |
|
506 % |
|
507 \endisatagproof |
|
508 {\isafoldproof}% |
|
509 % |
|
510 \isadelimproof |
|
511 % |
|
512 \endisadelimproof |
|
513 % |
|
514 \isadelimproof |
|
515 % |
|
516 \endisadelimproof |
|
517 % |
|
518 \isatagproof |
|
519 % |
|
520 \endisatagproof |
|
521 {\isafoldproof}% |
|
522 % |
|
523 \isadelimproof |
|
524 % |
|
525 \endisadelimproof |
|
526 % |
|
527 \isadelimproof |
|
528 % |
|
529 \endisadelimproof |
|
530 % |
|
531 \isatagproof |
|
532 % |
|
533 \endisatagproof |
|
534 {\isafoldproof}% |
|
535 % |
|
536 \isadelimproof |
|
537 % |
|
538 \endisadelimproof |
|
539 % |
|
540 \isadelimproof |
|
541 % |
|
542 \endisadelimproof |
|
543 % |
|
544 \isatagproof |
|
545 % |
|
546 \endisatagproof |
|
547 {\isafoldproof}% |
|
548 % |
|
549 \isadelimproof |
|
550 % |
|
551 \endisadelimproof |
|
552 % |
|
553 \isadelimproof |
|
554 % |
|
555 \endisadelimproof |
|
556 % |
|
557 \isatagproof |
|
558 % |
|
559 \endisatagproof |
|
560 {\isafoldproof}% |
|
561 % |
|
562 \isadelimproof |
|
563 % |
|
564 \endisadelimproof |
|
565 % |
|
566 \isadelimproof |
|
567 % |
|
568 \endisadelimproof |
|
569 % |
|
570 \isatagproof |
|
571 % |
|
572 \endisatagproof |
|
573 {\isafoldproof}% |
|
574 % |
|
575 \isadelimproof |
|
576 % |
|
577 \endisadelimproof |
|
578 % |
|
579 \isadelimproof |
|
580 % |
|
581 \endisadelimproof |
|
582 % |
|
583 \isatagproof |
|
584 % |
|
585 \endisatagproof |
|
586 {\isafoldproof}% |
|
587 % |
|
588 \isadelimproof |
|
589 % |
|
590 \endisadelimproof |
|
591 % |
|
592 \isadelimproof |
|
593 % |
|
594 \endisadelimproof |
|
595 % |
|
596 \isatagproof |
|
597 % |
|
598 \endisatagproof |
|
599 {\isafoldproof}% |
|
600 % |
|
601 \isadelimproof |
|
602 % |
|
603 \endisadelimproof |
|
604 % |
|
605 \isadelimproof |
|
606 % |
|
607 \endisadelimproof |
|
608 % |
|
609 \isatagproof |
|
610 % |
|
611 \endisatagproof |
|
612 {\isafoldproof}% |
|
613 % |
|
614 \isadelimproof |
|
615 % |
|
616 \endisadelimproof |
|
617 % |
|
618 \isadelimproof |
|
619 % |
|
620 \endisadelimproof |
|
621 % |
|
622 \isatagproof |
|
623 % |
|
624 \endisatagproof |
|
625 {\isafoldproof}% |
|
626 % |
|
627 \isadelimproof |
|
628 % |
|
629 \endisadelimproof |
|
630 % |
|
631 \isadelimproof |
|
632 % |
|
633 \endisadelimproof |
|
634 % |
|
635 \isatagproof |
|
636 % |
|
637 \endisatagproof |
|
638 {\isafoldproof}% |
|
639 % |
|
640 \isadelimproof |
|
641 % |
|
642 \endisadelimproof |
|
643 % |
|
644 \isadelimproof |
|
645 % |
|
646 \endisadelimproof |
|
647 % |
|
648 \isatagproof |
|
649 % |
|
650 \endisatagproof |
|
651 {\isafoldproof}% |
|
652 % |
|
653 \isadelimproof |
|
654 % |
|
655 \endisadelimproof |
|
656 % |
|
657 \isadelimproof |
|
658 % |
|
659 \endisadelimproof |
|
660 % |
|
661 \isatagproof |
|
662 % |
|
663 \endisatagproof |
|
664 {\isafoldproof}% |
|
665 % |
|
666 \isadelimproof |
|
667 % |
|
668 \endisadelimproof |
|
669 % |
|
670 \isamarkupsection{Modelling the Adversary% |
|
671 } |
|
672 \isamarkuptrue% |
|
673 % |
|
674 \begin{isamarkuptext}% |
|
675 The spy is part of the system and must be built into the model. He is |
|
676 a malicious user who does not have to follow the protocol. He |
|
677 watches the network and uses any keys he knows to decrypt messages. |
|
678 Thus he accumulates additional keys and nonces. These he can use to |
|
679 compose new messages, which he may send to anybody. |
|
680 |
|
681 Two functions enable us to formalize this behaviour: \isa{analz} and |
|
682 \isa{synth}. Each function maps a sets of messages to another set of |
|
683 messages. The set \isa{analz\ H} formalizes what the adversary can learn |
|
684 from the set of messages~$H$. The closure properties of this set are |
|
685 defined inductively.% |
|
686 \end{isamarkuptext}% |
|
687 \isamarkuptrue% |
|
688 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
|
689 \isanewline |
|
690 \ \ analz\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
691 \ \ \isakeyword{for}\ H\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
692 \ \ \isakeyword{where}\isanewline |
|
693 \ \ \ \ Inj\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{2C}{\isacharcomma}}simp{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
694 \ \ {\isaliteral{7C}{\isacharbar}}\ Fst{\isaliteral{3A}{\isacharcolon}}\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}X{\isaliteral{2C}{\isacharcomma}}Y{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
695 \ \ {\isaliteral{7C}{\isacharbar}}\ Snd{\isaliteral{3A}{\isacharcolon}}\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}X{\isaliteral{2C}{\isacharcomma}}Y{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
696 \ \ {\isaliteral{7C}{\isacharbar}}\ Decrypt\ {\isaliteral{5B}{\isacharbrackleft}}dest{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ \isanewline |
|
697 \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Crypt\ K\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{3B}{\isacharsemicolon}}\ Key{\isaliteral{28}{\isacharparenleft}}invKey\ K{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
698 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}% |
|
699 \isadelimproof |
|
700 % |
|
701 \endisadelimproof |
|
702 % |
|
703 \isatagproof |
|
704 % |
|
705 \endisatagproof |
|
706 {\isafoldproof}% |
|
707 % |
|
708 \isadelimproof |
|
709 % |
|
710 \endisadelimproof |
|
711 % |
|
712 \isadelimproof |
|
713 % |
|
714 \endisadelimproof |
|
715 % |
|
716 \isatagproof |
|
717 % |
|
718 \endisatagproof |
|
719 {\isafoldproof}% |
|
720 % |
|
721 \isadelimproof |
|
722 % |
|
723 \endisadelimproof |
|
724 % |
|
725 \isadelimproof |
|
726 % |
|
727 \endisadelimproof |
|
728 % |
|
729 \isatagproof |
|
730 % |
|
731 \endisatagproof |
|
732 {\isafoldproof}% |
|
733 % |
|
734 \isadelimproof |
|
735 % |
|
736 \endisadelimproof |
|
737 % |
|
738 \isadelimproof |
|
739 % |
|
740 \endisadelimproof |
|
741 % |
|
742 \isatagproof |
|
743 % |
|
744 \endisatagproof |
|
745 {\isafoldproof}% |
|
746 % |
|
747 \isadelimproof |
|
748 % |
|
749 \endisadelimproof |
|
750 % |
|
751 \isadelimproof |
|
752 % |
|
753 \endisadelimproof |
|
754 % |
|
755 \isatagproof |
|
756 % |
|
757 \endisatagproof |
|
758 {\isafoldproof}% |
|
759 % |
|
760 \isadelimproof |
|
761 % |
|
762 \endisadelimproof |
|
763 % |
|
764 \isadelimproof |
|
765 % |
|
766 \endisadelimproof |
|
767 % |
|
768 \isatagproof |
|
769 % |
|
770 \endisatagproof |
|
771 {\isafoldproof}% |
|
772 % |
|
773 \isadelimproof |
|
774 % |
|
775 \endisadelimproof |
|
776 % |
|
777 \isadelimproof |
|
778 % |
|
779 \endisadelimproof |
|
780 % |
|
781 \isatagproof |
|
782 % |
|
783 \endisatagproof |
|
784 {\isafoldproof}% |
|
785 % |
|
786 \isadelimproof |
|
787 % |
|
788 \endisadelimproof |
|
789 % |
|
790 \isadelimproof |
|
791 % |
|
792 \endisadelimproof |
|
793 % |
|
794 \isatagproof |
|
795 % |
|
796 \endisatagproof |
|
797 {\isafoldproof}% |
|
798 % |
|
799 \isadelimproof |
|
800 % |
|
801 \endisadelimproof |
|
802 % |
|
803 \isadelimproof |
|
804 % |
|
805 \endisadelimproof |
|
806 % |
|
807 \isatagproof |
|
808 % |
|
809 \endisatagproof |
|
810 {\isafoldproof}% |
|
811 % |
|
812 \isadelimproof |
|
813 % |
|
814 \endisadelimproof |
|
815 % |
|
816 \isadelimproof |
|
817 % |
|
818 \endisadelimproof |
|
819 % |
|
820 \isatagproof |
|
821 % |
|
822 \endisatagproof |
|
823 {\isafoldproof}% |
|
824 % |
|
825 \isadelimproof |
|
826 % |
|
827 \endisadelimproof |
|
828 % |
|
829 \isadelimproof |
|
830 % |
|
831 \endisadelimproof |
|
832 % |
|
833 \isatagproof |
|
834 % |
|
835 \endisatagproof |
|
836 {\isafoldproof}% |
|
837 % |
|
838 \isadelimproof |
|
839 % |
|
840 \endisadelimproof |
|
841 % |
|
842 \isadelimproof |
|
843 % |
|
844 \endisadelimproof |
|
845 % |
|
846 \isatagproof |
|
847 % |
|
848 \endisatagproof |
|
849 {\isafoldproof}% |
|
850 % |
|
851 \isadelimproof |
|
852 % |
|
853 \endisadelimproof |
|
854 % |
|
855 \isadelimproof |
|
856 % |
|
857 \endisadelimproof |
|
858 % |
|
859 \isatagproof |
|
860 % |
|
861 \endisatagproof |
|
862 {\isafoldproof}% |
|
863 % |
|
864 \isadelimproof |
|
865 % |
|
866 \endisadelimproof |
|
867 % |
|
868 \isadelimproof |
|
869 % |
|
870 \endisadelimproof |
|
871 % |
|
872 \isatagproof |
|
873 % |
|
874 \endisatagproof |
|
875 {\isafoldproof}% |
|
876 % |
|
877 \isadelimproof |
|
878 % |
|
879 \endisadelimproof |
|
880 % |
|
881 \isadelimproof |
|
882 % |
|
883 \endisadelimproof |
|
884 % |
|
885 \isatagproof |
|
886 % |
|
887 \endisatagproof |
|
888 {\isafoldproof}% |
|
889 % |
|
890 \isadelimproof |
|
891 % |
|
892 \endisadelimproof |
|
893 % |
|
894 \isadelimproof |
|
895 % |
|
896 \endisadelimproof |
|
897 % |
|
898 \isatagproof |
|
899 % |
|
900 \endisatagproof |
|
901 {\isafoldproof}% |
|
902 % |
|
903 \isadelimproof |
|
904 % |
|
905 \endisadelimproof |
|
906 % |
|
907 \isadelimproof |
|
908 % |
|
909 \endisadelimproof |
|
910 % |
|
911 \isatagproof |
|
912 % |
|
913 \endisatagproof |
|
914 {\isafoldproof}% |
|
915 % |
|
916 \isadelimproof |
|
917 % |
|
918 \endisadelimproof |
|
919 % |
|
920 \isadelimproof |
|
921 % |
|
922 \endisadelimproof |
|
923 % |
|
924 \isatagproof |
|
925 % |
|
926 \endisatagproof |
|
927 {\isafoldproof}% |
|
928 % |
|
929 \isadelimproof |
|
930 % |
|
931 \endisadelimproof |
|
932 % |
|
933 \isadelimproof |
|
934 % |
|
935 \endisadelimproof |
|
936 % |
|
937 \isatagproof |
|
938 % |
|
939 \endisatagproof |
|
940 {\isafoldproof}% |
|
941 % |
|
942 \isadelimproof |
|
943 % |
|
944 \endisadelimproof |
|
945 % |
|
946 \isadelimproof |
|
947 % |
|
948 \endisadelimproof |
|
949 % |
|
950 \isatagproof |
|
951 % |
|
952 \endisatagproof |
|
953 {\isafoldproof}% |
|
954 % |
|
955 \isadelimproof |
|
956 % |
|
957 \endisadelimproof |
|
958 % |
|
959 \isadelimproof |
|
960 % |
|
961 \endisadelimproof |
|
962 % |
|
963 \isatagproof |
|
964 % |
|
965 \endisatagproof |
|
966 {\isafoldproof}% |
|
967 % |
|
968 \isadelimproof |
|
969 % |
|
970 \endisadelimproof |
|
971 % |
|
972 \isadelimproof |
|
973 % |
|
974 \endisadelimproof |
|
975 % |
|
976 \isatagproof |
|
977 % |
|
978 \endisatagproof |
|
979 {\isafoldproof}% |
|
980 % |
|
981 \isadelimproof |
|
982 % |
|
983 \endisadelimproof |
|
984 % |
|
985 \isadelimproof |
|
986 % |
|
987 \endisadelimproof |
|
988 % |
|
989 \isatagproof |
|
990 % |
|
991 \endisatagproof |
|
992 {\isafoldproof}% |
|
993 % |
|
994 \isadelimproof |
|
995 % |
|
996 \endisadelimproof |
|
997 % |
|
998 \isadelimproof |
|
999 % |
|
1000 \endisadelimproof |
|
1001 % |
|
1002 \isatagproof |
|
1003 % |
|
1004 \endisatagproof |
|
1005 {\isafoldproof}% |
|
1006 % |
|
1007 \isadelimproof |
|
1008 % |
|
1009 \endisadelimproof |
|
1010 % |
|
1011 \isadelimproof |
|
1012 % |
|
1013 \endisadelimproof |
|
1014 % |
|
1015 \isatagproof |
|
1016 % |
|
1017 \endisatagproof |
|
1018 {\isafoldproof}% |
|
1019 % |
|
1020 \isadelimproof |
|
1021 % |
|
1022 \endisadelimproof |
|
1023 % |
|
1024 \isadelimproof |
|
1025 % |
|
1026 \endisadelimproof |
|
1027 % |
|
1028 \isatagproof |
|
1029 % |
|
1030 \endisatagproof |
|
1031 {\isafoldproof}% |
|
1032 % |
|
1033 \isadelimproof |
|
1034 % |
|
1035 \endisadelimproof |
|
1036 % |
|
1037 \isadelimproof |
|
1038 % |
|
1039 \endisadelimproof |
|
1040 % |
|
1041 \isatagproof |
|
1042 % |
|
1043 \endisatagproof |
|
1044 {\isafoldproof}% |
|
1045 % |
|
1046 \isadelimproof |
|
1047 % |
|
1048 \endisadelimproof |
|
1049 % |
|
1050 \isadelimproof |
|
1051 % |
|
1052 \endisadelimproof |
|
1053 % |
|
1054 \isatagproof |
|
1055 % |
|
1056 \endisatagproof |
|
1057 {\isafoldproof}% |
|
1058 % |
|
1059 \isadelimproof |
|
1060 % |
|
1061 \endisadelimproof |
|
1062 % |
|
1063 \isadelimproof |
|
1064 % |
|
1065 \endisadelimproof |
|
1066 % |
|
1067 \isatagproof |
|
1068 % |
|
1069 \endisatagproof |
|
1070 {\isafoldproof}% |
|
1071 % |
|
1072 \isadelimproof |
|
1073 % |
|
1074 \endisadelimproof |
|
1075 % |
|
1076 \isadelimproof |
|
1077 % |
|
1078 \endisadelimproof |
|
1079 % |
|
1080 \isatagproof |
|
1081 % |
|
1082 \endisatagproof |
|
1083 {\isafoldproof}% |
|
1084 % |
|
1085 \isadelimproof |
|
1086 % |
|
1087 \endisadelimproof |
|
1088 % |
|
1089 \isadelimproof |
|
1090 % |
|
1091 \endisadelimproof |
|
1092 % |
|
1093 \isatagproof |
|
1094 % |
|
1095 \endisatagproof |
|
1096 {\isafoldproof}% |
|
1097 % |
|
1098 \isadelimproof |
|
1099 % |
|
1100 \endisadelimproof |
|
1101 % |
|
1102 \isadelimproof |
|
1103 % |
|
1104 \endisadelimproof |
|
1105 % |
|
1106 \isatagproof |
|
1107 % |
|
1108 \endisatagproof |
|
1109 {\isafoldproof}% |
|
1110 % |
|
1111 \isadelimproof |
|
1112 % |
|
1113 \endisadelimproof |
|
1114 % |
|
1115 \begin{isamarkuptext}% |
|
1116 Note the \isa{Decrypt} rule: the spy can decrypt a |
|
1117 message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. |
|
1118 Properties proved by rule induction include the following: |
|
1119 \begin{isabelle}% |
|
1120 G\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ analz\ G\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ analz\ H\rulename{analz{\isaliteral{5F}{\isacharunderscore}}mono}\par\smallskip% |
|
1121 analz\ {\isaliteral{28}{\isacharparenleft}}analz\ H{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ analz\ H\rulename{analz{\isaliteral{5F}{\isacharunderscore}}idem}% |
|
1122 \end{isabelle} |
|
1123 |
|
1124 The set of fake messages that an intruder could invent |
|
1125 starting from~\isa{H} is \isa{synth{\isaliteral{28}{\isacharparenleft}}analz\ H{\isaliteral{29}{\isacharparenright}}}, where \isa{synth\ H} |
|
1126 formalizes what the adversary can build from the set of messages~$H$.% |
|
1127 \end{isamarkuptext}% |
|
1128 \isamarkuptrue% |
|
1129 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
|
1130 \isanewline |
|
1131 \ \ synth\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1132 \ \ \isakeyword{for}\ H\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1133 \ \ \isakeyword{where}\isanewline |
|
1134 \ \ \ \ Inj\ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1135 \ \ {\isaliteral{7C}{\isacharbar}}\ Agent\ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Agent\ agt\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1136 \ \ {\isaliteral{7C}{\isacharbar}}\ MPair\ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
1137 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{3B}{\isacharsemicolon}}\ \ Y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}X{\isaliteral{2C}{\isacharcomma}}Y{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1138 \ \ {\isaliteral{7C}{\isacharbar}}\ Crypt\ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
1139 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{3B}{\isacharsemicolon}}\ \ Key\ K\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Crypt\ K\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1140 \isadelimproof |
|
1141 % |
|
1142 \endisadelimproof |
|
1143 % |
|
1144 \isatagproof |
|
1145 % |
|
1146 \endisatagproof |
|
1147 {\isafoldproof}% |
|
1148 % |
|
1149 \isadelimproof |
|
1150 % |
|
1151 \endisadelimproof |
|
1152 % |
|
1153 \isadelimproof |
|
1154 % |
|
1155 \endisadelimproof |
|
1156 % |
|
1157 \isatagproof |
|
1158 % |
|
1159 \endisatagproof |
|
1160 {\isafoldproof}% |
|
1161 % |
|
1162 \isadelimproof |
|
1163 % |
|
1164 \endisadelimproof |
|
1165 % |
|
1166 \isadelimproof |
|
1167 % |
|
1168 \endisadelimproof |
|
1169 % |
|
1170 \isatagproof |
|
1171 % |
|
1172 \endisatagproof |
|
1173 {\isafoldproof}% |
|
1174 % |
|
1175 \isadelimproof |
|
1176 % |
|
1177 \endisadelimproof |
|
1178 % |
|
1179 \begin{isamarkuptext}% |
|
1180 The set includes all agent names. Nonces and keys are assumed to be |
|
1181 unguessable, so none are included beyond those already in~$H$. Two |
|
1182 elements of \isa{synth\ H} can be combined, and an element can be encrypted |
|
1183 using a key present in~$H$. |
|
1184 |
|
1185 Like \isa{analz}, this set operator is monotone and idempotent. It also |
|
1186 satisfies an interesting equation involving \isa{analz}: |
|
1187 \begin{isabelle}% |
|
1188 analz\ {\isaliteral{28}{\isacharparenleft}}synth\ H{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ analz\ H\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ synth\ H\rulename{analz{\isaliteral{5F}{\isacharunderscore}}synth}% |
|
1189 \end{isabelle} |
|
1190 Rule inversion plays a major role in reasoning about \isa{synth}, through |
|
1191 declarations such as this one:% |
|
1192 \end{isamarkuptext}% |
|
1193 \isamarkuptrue% |
|
1194 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}\isamarkupfalse% |
|
1195 \ Nonce{\isaliteral{5F}{\isacharunderscore}}synth\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Nonce\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1196 \begin{isamarkuptext}% |
|
1197 \noindent |
|
1198 The resulting elimination rule replaces every assumption of the form |
|
1199 \isa{Nonce\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H} by \isa{Nonce\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H}, |
|
1200 expressing that a nonce cannot be guessed. |
|
1201 |
|
1202 A third operator, \isa{parts}, is useful for stating correctness |
|
1203 properties. The set |
|
1204 \isa{parts\ H} consists of the components of elements of~$H$. This set |
|
1205 includes~\isa{H} and is closed under the projections from a compound |
|
1206 message to its immediate parts. |
|
1207 Its definition resembles that of \isa{analz} except in the rule |
|
1208 corresponding to the constructor \isa{Crypt}: |
|
1209 \begin{isabelle}% |
|
1210 \ \ \ \ \ Crypt\ K\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ H% |
|
1211 \end{isabelle} |
|
1212 The body of an encrypted message is always regarded as part of it. We can |
|
1213 use \isa{parts} to express general well-formedness properties of a protocol, |
|
1214 for example, that an uncompromised agent's private key will never be |
|
1215 included as a component of any message.% |
|
1216 \end{isamarkuptext}% |
|
1217 \isamarkuptrue% |
|
1218 % |
|
1219 \isadelimproof |
|
1220 % |
|
1221 \endisadelimproof |
|
1222 % |
|
1223 \isatagproof |
|
1224 % |
|
1225 \endisatagproof |
|
1226 {\isafoldproof}% |
|
1227 % |
|
1228 \isadelimproof |
|
1229 % |
|
1230 \endisadelimproof |
|
1231 % |
|
1232 \isadelimproof |
|
1233 % |
|
1234 \endisadelimproof |
|
1235 % |
|
1236 \isatagproof |
|
1237 % |
|
1238 \endisatagproof |
|
1239 {\isafoldproof}% |
|
1240 % |
|
1241 \isadelimproof |
|
1242 % |
|
1243 \endisadelimproof |
|
1244 % |
|
1245 \isadelimproof |
|
1246 % |
|
1247 \endisadelimproof |
|
1248 % |
|
1249 \isatagproof |
|
1250 % |
|
1251 \endisatagproof |
|
1252 {\isafoldproof}% |
|
1253 % |
|
1254 \isadelimproof |
|
1255 % |
|
1256 \endisadelimproof |
|
1257 % |
|
1258 \isadelimproof |
|
1259 % |
|
1260 \endisadelimproof |
|
1261 % |
|
1262 \isatagproof |
|
1263 % |
|
1264 \endisatagproof |
|
1265 {\isafoldproof}% |
|
1266 % |
|
1267 \isadelimproof |
|
1268 % |
|
1269 \endisadelimproof |
|
1270 % |
|
1271 \isadelimproof |
|
1272 % |
|
1273 \endisadelimproof |
|
1274 % |
|
1275 \isatagproof |
|
1276 % |
|
1277 \endisatagproof |
|
1278 {\isafoldproof}% |
|
1279 % |
|
1280 \isadelimproof |
|
1281 % |
|
1282 \endisadelimproof |
|
1283 % |
|
1284 \isadelimproof |
|
1285 % |
|
1286 \endisadelimproof |
|
1287 % |
|
1288 \isatagproof |
|
1289 % |
|
1290 \endisatagproof |
|
1291 {\isafoldproof}% |
|
1292 % |
|
1293 \isadelimproof |
|
1294 % |
|
1295 \endisadelimproof |
|
1296 % |
|
1297 \isadelimproof |
|
1298 % |
|
1299 \endisadelimproof |
|
1300 % |
|
1301 \isatagproof |
|
1302 % |
|
1303 \endisatagproof |
|
1304 {\isafoldproof}% |
|
1305 % |
|
1306 \isadelimproof |
|
1307 % |
|
1308 \endisadelimproof |
|
1309 % |
|
1310 \isadelimproof |
|
1311 % |
|
1312 \endisadelimproof |
|
1313 % |
|
1314 \isatagproof |
|
1315 % |
|
1316 \endisatagproof |
|
1317 {\isafoldproof}% |
|
1318 % |
|
1319 \isadelimproof |
|
1320 % |
|
1321 \endisadelimproof |
|
1322 % |
|
1323 \isadelimproof |
|
1324 % |
|
1325 \endisadelimproof |
|
1326 % |
|
1327 \isatagproof |
|
1328 % |
|
1329 \endisatagproof |
|
1330 {\isafoldproof}% |
|
1331 % |
|
1332 \isadelimproof |
|
1333 % |
|
1334 \endisadelimproof |
|
1335 % |
|
1336 \isadelimproof |
|
1337 % |
|
1338 \endisadelimproof |
|
1339 % |
|
1340 \isatagproof |
|
1341 % |
|
1342 \endisatagproof |
|
1343 {\isafoldproof}% |
|
1344 % |
|
1345 \isadelimproof |
|
1346 % |
|
1347 \endisadelimproof |
|
1348 % |
|
1349 \isadelimproof |
|
1350 % |
|
1351 \endisadelimproof |
|
1352 % |
|
1353 \isatagproof |
|
1354 % |
|
1355 \endisatagproof |
|
1356 {\isafoldproof}% |
|
1357 % |
|
1358 \isadelimproof |
|
1359 % |
|
1360 \endisadelimproof |
|
1361 % |
|
1362 \isadelimproof |
|
1363 % |
|
1364 \endisadelimproof |
|
1365 % |
|
1366 \isatagproof |
|
1367 % |
|
1368 \endisatagproof |
|
1369 {\isafoldproof}% |
|
1370 % |
|
1371 \isadelimproof |
|
1372 % |
|
1373 \endisadelimproof |
|
1374 % |
|
1375 \isadelimproof |
|
1376 % |
|
1377 \endisadelimproof |
|
1378 % |
|
1379 \isatagproof |
|
1380 % |
|
1381 \endisatagproof |
|
1382 {\isafoldproof}% |
|
1383 % |
|
1384 \isadelimproof |
|
1385 % |
|
1386 \endisadelimproof |
|
1387 % |
|
1388 \isadelimproof |
|
1389 % |
|
1390 \endisadelimproof |
|
1391 % |
|
1392 \isatagproof |
|
1393 % |
|
1394 \endisatagproof |
|
1395 {\isafoldproof}% |
|
1396 % |
|
1397 \isadelimproof |
|
1398 % |
|
1399 \endisadelimproof |
|
1400 % |
|
1401 \isadelimproof |
|
1402 % |
|
1403 \endisadelimproof |
|
1404 % |
|
1405 \isatagproof |
|
1406 % |
|
1407 \endisatagproof |
|
1408 {\isafoldproof}% |
|
1409 % |
|
1410 \isadelimproof |
|
1411 % |
|
1412 \endisadelimproof |
|
1413 % |
|
1414 \isadelimproof |
|
1415 % |
|
1416 \endisadelimproof |
|
1417 % |
|
1418 \isatagproof |
|
1419 % |
|
1420 \endisatagproof |
|
1421 {\isafoldproof}% |
|
1422 % |
|
1423 \isadelimproof |
|
1424 % |
|
1425 \endisadelimproof |
|
1426 % |
|
1427 \isadelimproof |
|
1428 % |
|
1429 \endisadelimproof |
|
1430 % |
|
1431 \isatagproof |
|
1432 % |
|
1433 \endisatagproof |
|
1434 {\isafoldproof}% |
|
1435 % |
|
1436 \isadelimproof |
|
1437 % |
|
1438 \endisadelimproof |
|
1439 % |
|
1440 \isadelimproof |
|
1441 % |
|
1442 \endisadelimproof |
|
1443 % |
|
1444 \isatagproof |
|
1445 % |
|
1446 \endisatagproof |
|
1447 {\isafoldproof}% |
|
1448 % |
|
1449 \isadelimproof |
|
1450 % |
|
1451 \endisadelimproof |
|
1452 % |
|
1453 \isadelimproof |
|
1454 % |
|
1455 \endisadelimproof |
|
1456 % |
|
1457 \isatagproof |
|
1458 % |
|
1459 \endisatagproof |
|
1460 {\isafoldproof}% |
|
1461 % |
|
1462 \isadelimproof |
|
1463 % |
|
1464 \endisadelimproof |
|
1465 % |
|
1466 \isadelimproof |
|
1467 % |
|
1468 \endisadelimproof |
|
1469 % |
|
1470 \isatagproof |
|
1471 % |
|
1472 \endisatagproof |
|
1473 {\isafoldproof}% |
|
1474 % |
|
1475 \isadelimproof |
|
1476 % |
|
1477 \endisadelimproof |
|
1478 % |
|
1479 \isadelimproof |
|
1480 % |
|
1481 \endisadelimproof |
|
1482 % |
|
1483 \isatagproof |
|
1484 % |
|
1485 \endisatagproof |
|
1486 {\isafoldproof}% |
|
1487 % |
|
1488 \isadelimproof |
|
1489 % |
|
1490 \endisadelimproof |
|
1491 % |
|
1492 \isadelimproof |
|
1493 % |
|
1494 \endisadelimproof |
|
1495 % |
|
1496 \isatagproof |
|
1497 % |
|
1498 \endisatagproof |
|
1499 {\isafoldproof}% |
|
1500 % |
|
1501 \isadelimproof |
|
1502 % |
|
1503 \endisadelimproof |
|
1504 % |
|
1505 \isadelimproof |
|
1506 % |
|
1507 \endisadelimproof |
|
1508 % |
|
1509 \isatagproof |
|
1510 % |
|
1511 \endisatagproof |
|
1512 {\isafoldproof}% |
|
1513 % |
|
1514 \isadelimproof |
|
1515 % |
|
1516 \endisadelimproof |
|
1517 % |
|
1518 \isadelimML |
|
1519 % |
|
1520 \endisadelimML |
|
1521 % |
|
1522 \isatagML |
|
1523 % |
|
1524 \endisatagML |
|
1525 {\isafoldML}% |
|
1526 % |
|
1527 \isadelimML |
|
1528 % |
|
1529 \endisadelimML |
|
1530 % |
|
1531 \isadelimproof |
|
1532 % |
|
1533 \endisadelimproof |
|
1534 % |
|
1535 \isatagproof |
|
1536 % |
|
1537 \endisatagproof |
|
1538 {\isafoldproof}% |
|
1539 % |
|
1540 \isadelimproof |
|
1541 % |
|
1542 \endisadelimproof |
|
1543 % |
|
1544 \isadelimproof |
|
1545 % |
|
1546 \endisadelimproof |
|
1547 % |
|
1548 \isatagproof |
|
1549 % |
|
1550 \endisatagproof |
|
1551 {\isafoldproof}% |
|
1552 % |
|
1553 \isadelimproof |
|
1554 % |
|
1555 \endisadelimproof |
|
1556 % |
|
1557 \isadelimproof |
|
1558 % |
|
1559 \endisadelimproof |
|
1560 % |
|
1561 \isatagproof |
|
1562 % |
|
1563 \endisatagproof |
|
1564 {\isafoldproof}% |
|
1565 % |
|
1566 \isadelimproof |
|
1567 % |
|
1568 \endisadelimproof |
|
1569 % |
|
1570 \isadelimproof |
|
1571 % |
|
1572 \endisadelimproof |
|
1573 % |
|
1574 \isatagproof |
|
1575 % |
|
1576 \endisatagproof |
|
1577 {\isafoldproof}% |
|
1578 % |
|
1579 \isadelimproof |
|
1580 % |
|
1581 \endisadelimproof |
|
1582 % |
|
1583 \isadelimproof |
|
1584 % |
|
1585 \endisadelimproof |
|
1586 % |
|
1587 \isatagproof |
|
1588 % |
|
1589 \endisatagproof |
|
1590 {\isafoldproof}% |
|
1591 % |
|
1592 \isadelimproof |
|
1593 % |
|
1594 \endisadelimproof |
|
1595 % |
|
1596 \isadelimproof |
|
1597 % |
|
1598 \endisadelimproof |
|
1599 % |
|
1600 \isatagproof |
|
1601 % |
|
1602 \endisatagproof |
|
1603 {\isafoldproof}% |
|
1604 % |
|
1605 \isadelimproof |
|
1606 % |
|
1607 \endisadelimproof |
|
1608 % |
|
1609 \isadelimML |
|
1610 % |
|
1611 \endisadelimML |
|
1612 % |
|
1613 \isatagML |
|
1614 % |
|
1615 \endisatagML |
|
1616 {\isafoldML}% |
|
1617 % |
|
1618 \isadelimML |
|
1619 % |
|
1620 \endisadelimML |
|
1621 % |
|
1622 \isadelimtheory |
|
1623 % |
|
1624 \endisadelimtheory |
|
1625 % |
|
1626 \isatagtheory |
|
1627 % |
|
1628 \endisatagtheory |
|
1629 {\isafoldtheory}% |
|
1630 % |
|
1631 \isadelimtheory |
|
1632 % |
|
1633 \endisadelimtheory |
|
1634 \end{isabellebody}% |
|
1635 %%% Local Variables: |
|
1636 %%% mode: latex |
|
1637 %%% TeX-master: "root" |
|
1638 %%% End: |