doc-src/TutorialI/Protocol/document/NS_Public.tex
 changeset 35503 7bba12c3b7b6 parent 27094 2cf13a72e170 child 40406 313a24b66a8d
equal inserted replaced
34972:cc1d4c3ca9db 35503:7bba12c3b7b6
    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.