equal
deleted
inserted
replaced
10 55-61 |
10 55-61 |
11 *) |
11 *) |
12 |
12 |
13 theory ZhouGollmann imports Public begin |
13 theory ZhouGollmann imports Public begin |
14 |
14 |
15 syntax |
15 abbreviation |
16 TTP :: agent |
16 TTP :: agent |
17 |
17 "TTP == Server" |
18 translations |
18 |
19 "TTP" == " Server " |
|
20 |
|
21 syntax |
|
22 f_sub :: nat |
19 f_sub :: nat |
|
20 "f_sub == 5" |
23 f_nro :: nat |
21 f_nro :: nat |
|
22 "f_nro == 2" |
24 f_nrr :: nat |
23 f_nrr :: nat |
|
24 "f_nrr == 3" |
25 f_con :: nat |
25 f_con :: nat |
26 |
26 "f_con == 4" |
27 translations |
|
28 "f_sub" == " 5 " |
|
29 "f_nro" == " 2 " |
|
30 "f_nrr" == " 3 " |
|
31 "f_con" == " 4 " |
|
32 |
27 |
33 |
28 |
34 constdefs |
29 constdefs |
35 broken :: "agent set" |
30 broken :: "agent set" |
36 --{*the compromised honest agents; TTP is included as it's not allowed to |
31 --{*the compromised honest agents; TTP is included as it's not allowed to |