equal
deleted
inserted
replaced
486 can occur only once in a trace. The following lemma states that a nonce |
486 can occur only once in a trace. The following lemma states that a nonce |
487 cannot be used both as $Na$ and as $Nb$ unless |
487 cannot be used both as $Na$ and as $Nb$ unless |
488 it is known to the spy. Intuitively, it holds because honest agents |
488 it is known to the spy. Intuitively, it holds because honest agents |
489 always choose fresh values as nonces; only the spy might reuse a value, |
489 always choose fresh values as nonces; only the spy might reuse a value, |
490 and he doesn't know this particular value. The proof script is short: |
490 and he doesn't know this particular value. The proof script is short: |
491 induction, simplification, \isa{blast}. |
491 induction, simplification, \isa{blast}. The first line uses the rule |
|
492 \isa{rev_mp} to prepare the induction by moving two assumptions into the |
|
493 induction formula. |
492 \begin{isabelle} |
494 \begin{isabelle} |
493 \isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline |
495 \isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline |
494 \ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\ |
496 \ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\ |
495 NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\ |
497 NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\ |
496 evs);\isanewline |
498 evs);\isanewline |