summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/Protocol/document/NS_Public.tex

changeset 35503 | 7bba12c3b7b6 |

parent 27094 | 2cf13a72e170 |

child 40406 | 313a24b66a8d |

equal
deleted
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. |