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