equal
deleted
inserted
replaced
87 |
87 |
88 (*---------------------------------------------------------------------*) |
88 (*---------------------------------------------------------------------*) |
89 |
89 |
90 |
90 |
91 (* Predicate formalising the association between authKeys and servKeys *) |
91 (* Predicate formalising the association between authKeys and servKeys *) |
92 constdefs |
92 definition AKcryptSK :: "[key, key, event list] => bool" where |
93 AKcryptSK :: "[key, key, event list] => bool" |
|
94 "AKcryptSK authK servK evs == |
93 "AKcryptSK authK servK evs == |
95 \<exists>A B Ts. |
94 \<exists>A B Ts. |
96 Says Tgs A (Crypt authK |
95 Says Tgs A (Crypt authK |
97 \<lbrace>Key servK, Agent B, Number Ts, |
96 \<lbrace>Key servK, Agent B, Number Ts, |
98 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>) |
97 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>) |