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