equal
deleted
inserted
replaced
14 |
14 |
15 abbreviation |
15 abbreviation |
16 Tgs :: agent where "Tgs == Friend 0" |
16 Tgs :: agent where "Tgs == Friend 0" |
17 |
17 |
18 |
18 |
19 axioms |
19 axiomatization where |
20 Tgs_not_bad [iff]: "Tgs \<notin> bad" |
20 Tgs_not_bad [iff]: "Tgs \<notin> bad" |
21 --{*Tgs is secure --- we already know that Kas is secure*} |
21 --{*Tgs is secure --- we already know that Kas is secure*} |
22 |
22 |
23 definition |
23 definition |
24 (* authKeys are those contained in an authTicket *) |
24 (* authKeys are those contained in an authTicket *) |