equal
deleted
inserted
replaced
6 |
6 |
7 theory KerberosV imports Public begin |
7 theory KerberosV imports Public begin |
8 |
8 |
9 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
9 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
10 |
10 |
11 syntax |
11 abbreviation |
12 Kas :: agent |
12 Kas :: agent |
13 Tgs :: agent --{*the two servers are translations...*} |
13 "Kas == Server" |
14 |
14 |
15 |
15 Tgs :: agent |
16 translations |
16 "Tgs == Friend 0" |
17 "Kas" == "Server " |
|
18 "Tgs" == "Friend 0" |
|
19 |
17 |
20 |
18 |
21 axioms |
19 axioms |
22 Tgs_not_bad [iff]: "Tgs \<notin> bad" |
20 Tgs_not_bad [iff]: "Tgs \<notin> bad" |
23 --{*Tgs is secure --- we already know that Kas is secure*} |
21 --{*Tgs is secure --- we already know that Kas is secure*} |
24 |
|
25 (*The current time is just the length of the trace!*) |
|
26 syntax |
|
27 CT :: "event list=>nat" |
|
28 |
|
29 expiredAK :: "[nat, event list] => bool" |
|
30 |
|
31 expiredSK :: "[nat, event list] => bool" |
|
32 |
|
33 expiredA :: "[nat, event list] => bool" |
|
34 |
|
35 valid :: "[nat, nat] => bool" ("valid _ wrt _") |
|
36 |
|
37 |
22 |
38 constdefs |
23 constdefs |
39 (* authKeys are those contained in an authTicket *) |
24 (* authKeys are those contained in an authTicket *) |
40 authKeys :: "event list => key set" |
25 authKeys :: "event list => key set" |
41 "authKeys evs == {authK. \<exists>A Peer Ta. |
26 "authKeys evs == {authK. \<exists>A Peer Ta. |
79 |
64 |
80 specification (replylife) |
65 specification (replylife) |
81 replylife_LB [iff]: "Suc 0 \<le> replylife" |
66 replylife_LB [iff]: "Suc 0 \<le> replylife" |
82 by blast |
67 by blast |
83 |
68 |
84 translations |
69 abbreviation |
85 "CT" == "length " |
70 (*The current time is just the length of the trace!*) |
86 |
71 CT :: "event list=>nat" |
87 "expiredAK T evs" == "authKlife + T < CT evs" |
72 "CT == length" |
88 |
73 |
89 "expiredSK T evs" == "servKlife + T < CT evs" |
74 expiredAK :: "[nat, event list] => bool" |
90 |
75 "expiredAK T evs == authKlife + T < CT evs" |
91 "expiredA T evs" == "authlife + T < CT evs" |
76 |
92 |
77 expiredSK :: "[nat, event list] => bool" |
93 "valid T1 wrt T2" == "T1 <= replylife + T2" |
78 "expiredSK T evs == servKlife + T < CT evs" |
|
79 |
|
80 expiredA :: "[nat, event list] => bool" |
|
81 "expiredA T evs == authlife + T < CT evs" |
|
82 |
|
83 valid :: "[nat, nat] => bool" ("valid _ wrt _") |
|
84 "valid T1 wrt T2 == T1 <= replylife + T2" |
94 |
85 |
95 (*---------------------------------------------------------------------*) |
86 (*---------------------------------------------------------------------*) |
96 |
87 |
97 |
88 |
98 (* Predicate formalising the association between authKeys and servKeys *) |
89 (* Predicate formalising the association between authKeys and servKeys *) |