equal
deleted
inserted
replaced
74 Here is a detailed explanation of rule @{text NS2}. |
74 Here is a detailed explanation of rule @{text NS2}. |
75 A trace containing an event of the form |
75 A trace containing an event of the form |
76 @{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"} |
76 @{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"} |
77 may be extended by an event of the form |
77 may be extended by an event of the form |
78 @{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"} |
78 @{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"} |
79 where @{text NB} is a fresh nonce: @{term "Nonce NB \<in> used evs2"}. |
79 where @{text NB} is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}. |
80 Writing the sender as @{text A'} indicates that @{text B} does not |
80 Writing the sender as @{text A'} indicates that @{text B} does not |
81 know who sent the message. Calling the trace variable @{text evs2} rather |
81 know who sent the message. Calling the trace variable @{text evs2} rather |
82 than simply @{text evs} helps us know where we are in a proof after many |
82 than simply @{text evs} helps us know where we are in a proof after many |
83 case-splits: every subgoal mentioning @{text evs2} involves message~2 of the |
83 case-splits: every subgoal mentioning @{text evs2} involves message~2 of the |
84 protocol. |
84 protocol. |