equal
deleted
inserted
replaced
238 done |
238 done |
239 |
239 |
240 |
240 |
241 subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*} |
241 subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*} |
242 |
242 |
243 text{*Beware of [rule_format] and the universal quantifier!*} |
243 text{*Beware of @{text "[rule_format]"} and the universal quantifier!*} |
244 lemma secrecy_lemma: |
244 lemma secrecy_lemma: |
245 "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, |
245 "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, |
246 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) |
246 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) |
247 \<in> set evs; |
247 \<in> set evs; |
248 A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
248 A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |