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