equal
deleted
inserted
replaced
82 \end{isabelle} |
82 \end{isabelle} |
83 may be extended by an event of the form |
83 may be extended by an event of the form |
84 \begin{isabelle}% |
84 \begin{isabelle}% |
85 \ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}% |
85 \ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}% |
86 \end{isabelle} |
86 \end{isabelle} |
87 where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}. |
87 where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}}. |
88 Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not |
88 Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not |
89 know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather |
89 know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather |
90 than simply \isa{evs} helps us know where we are in a proof after many |
90 than simply \isa{evs} helps us know where we are in a proof after many |
91 case-splits: every subgoal mentioning \isa{evs{\isadigit{2}}} involves message~2 of the |
91 case-splits: every subgoal mentioning \isa{evs{\isadigit{2}}} involves message~2 of the |
92 protocol. |
92 protocol. |