doc-src/TutorialI/Protocol/NS_Public.thy
 changeset 35503 7bba12c3b7b6 parent 32960 69916a850301 child 42637 381fdcab0f36
equal inserted replaced
34972:cc1d4c3ca9db 35503:7bba12c3b7b6
`    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.`