1.1 --- a/doc-src/TutorialI/Protocol/document/Event.tex Thu Jul 26 16:08:16 2012 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,518 +0,0 @@
1.4 -%
1.5 -\begin{isabellebody}%
1.6 -\def\isabellecontext{Event}%
1.7 -%
1.8 -\isadelimtheory
1.9 -%
1.10 -\endisadelimtheory
1.11 -%
1.12 -\isatagtheory
1.13 -%
1.14 -\endisatagtheory
1.15 -{\isafoldtheory}%
1.16 -%
1.17 -\isadelimtheory
1.18 -%
1.19 -\endisadelimtheory
1.20 -%
1.21 -\isadelimproof
1.22 -%
1.23 -\endisadelimproof
1.24 -%
1.25 -\isatagproof
1.26 -%
1.27 -\endisatagproof
1.28 -{\isafoldproof}%
1.29 -%
1.30 -\isadelimproof
1.31 -%
1.32 -\endisadelimproof
1.33 -%
1.34 -\isadelimproof
1.35 -%
1.36 -\endisadelimproof
1.37 -%
1.38 -\isatagproof
1.39 -%
1.40 -\endisatagproof
1.41 -{\isafoldproof}%
1.42 -%
1.43 -\isadelimproof
1.44 -%
1.45 -\endisadelimproof
1.46 -%
1.47 -\isadelimproof
1.48 -%
1.49 -\endisadelimproof
1.50 -%
1.51 -\isatagproof
1.52 -%
1.53 -\endisatagproof
1.54 -{\isafoldproof}%
1.55 -%
1.56 -\isadelimproof
1.57 -%
1.58 -\endisadelimproof
1.59 -%
1.60 -\isadelimproof
1.61 -%
1.62 -\endisadelimproof
1.63 -%
1.64 -\isatagproof
1.65 -%
1.66 -\endisatagproof
1.67 -{\isafoldproof}%
1.68 -%
1.69 -\isadelimproof
1.70 -%
1.71 -\endisadelimproof
1.72 -%
1.73 -\isadelimproof
1.74 -%
1.75 -\endisadelimproof
1.76 -%
1.77 -\isatagproof
1.78 -%
1.79 -\endisatagproof
1.80 -{\isafoldproof}%
1.81 -%
1.82 -\isadelimproof
1.83 -%
1.84 -\endisadelimproof
1.85 -%
1.86 -\isadelimproof
1.87 -%
1.88 -\endisadelimproof
1.89 -%
1.90 -\isatagproof
1.91 -%
1.92 -\endisatagproof
1.93 -{\isafoldproof}%
1.94 -%
1.95 -\isadelimproof
1.96 -%
1.97 -\endisadelimproof
1.98 -%
1.99 -\isadelimproof
1.100 -%
1.101 -\endisadelimproof
1.102 -%
1.103 -\isatagproof
1.104 -%
1.105 -\endisatagproof
1.106 -{\isafoldproof}%
1.107 -%
1.108 -\isadelimproof
1.109 -%
1.110 -\endisadelimproof
1.111 -%
1.112 -\isadelimproof
1.113 -%
1.114 -\endisadelimproof
1.115 -%
1.116 -\isatagproof
1.117 -%
1.118 -\endisatagproof
1.119 -{\isafoldproof}%
1.120 -%
1.121 -\isadelimproof
1.122 -%
1.123 -\endisadelimproof
1.124 -%
1.125 -\isadelimproof
1.126 -%
1.127 -\endisadelimproof
1.128 -%
1.129 -\isatagproof
1.130 -%
1.131 -\endisatagproof
1.132 -{\isafoldproof}%
1.133 -%
1.134 -\isadelimproof
1.135 -%
1.136 -\endisadelimproof
1.137 -%
1.138 -\isadelimproof
1.139 -%
1.140 -\endisadelimproof
1.141 -%
1.142 -\isatagproof
1.143 -%
1.144 -\endisatagproof
1.145 -{\isafoldproof}%
1.146 -%
1.147 -\isadelimproof
1.148 -%
1.149 -\endisadelimproof
1.150 -%
1.151 -\isadelimproof
1.152 -%
1.153 -\endisadelimproof
1.154 -%
1.155 -\isatagproof
1.156 -%
1.157 -\endisatagproof
1.158 -{\isafoldproof}%
1.159 -%
1.160 -\isadelimproof
1.161 -%
1.162 -\endisadelimproof
1.163 -%
1.164 -\isadelimproof
1.165 -%
1.166 -\endisadelimproof
1.167 -%
1.168 -\isatagproof
1.169 -%
1.170 -\endisatagproof
1.171 -{\isafoldproof}%
1.172 -%
1.173 -\isadelimproof
1.174 -%
1.175 -\endisadelimproof
1.176 -%
1.177 -\isadelimproof
1.178 -%
1.179 -\endisadelimproof
1.180 -%
1.181 -\isatagproof
1.182 -%
1.183 -\endisatagproof
1.184 -{\isafoldproof}%
1.185 -%
1.186 -\isadelimproof
1.187 -%
1.188 -\endisadelimproof
1.189 -%
1.190 -\isadelimproof
1.191 -%
1.192 -\endisadelimproof
1.193 -%
1.194 -\isatagproof
1.195 -%
1.196 -\endisatagproof
1.197 -{\isafoldproof}%
1.198 -%
1.199 -\isadelimproof
1.200 -%
1.201 -\endisadelimproof
1.202 -%
1.203 -\isadelimproof
1.204 -%
1.205 -\endisadelimproof
1.206 -%
1.207 -\isatagproof
1.208 -%
1.209 -\endisatagproof
1.210 -{\isafoldproof}%
1.211 -%
1.212 -\isadelimproof
1.213 -%
1.214 -\endisadelimproof
1.215 -%
1.216 -\isadelimproof
1.217 -%
1.218 -\endisadelimproof
1.219 -%
1.220 -\isatagproof
1.221 -%
1.222 -\endisatagproof
1.223 -{\isafoldproof}%
1.224 -%
1.225 -\isadelimproof
1.226 -%
1.227 -\endisadelimproof
1.228 -%
1.229 -\isadelimproof
1.230 -%
1.231 -\endisadelimproof
1.232 -%
1.233 -\isatagproof
1.234 -%
1.235 -\endisatagproof
1.236 -{\isafoldproof}%
1.237 -%
1.238 -\isadelimproof
1.239 -%
1.240 -\endisadelimproof
1.241 -%
1.242 -\isadelimproof
1.243 -%
1.244 -\endisadelimproof
1.245 -%
1.246 -\isatagproof
1.247 -%
1.248 -\endisatagproof
1.249 -{\isafoldproof}%
1.250 -%
1.251 -\isadelimproof
1.252 -%
1.253 -\endisadelimproof
1.254 -%
1.255 -\isadelimproof
1.256 -%
1.257 -\endisadelimproof
1.258 -%
1.259 -\isatagproof
1.260 -%
1.261 -\endisatagproof
1.262 -{\isafoldproof}%
1.263 -%
1.264 -\isadelimproof
1.265 -%
1.266 -\endisadelimproof
1.267 -%
1.268 -\isadelimproof
1.269 -%
1.270 -\endisadelimproof
1.271 -%
1.272 -\isatagproof
1.273 -%
1.274 -\endisatagproof
1.275 -{\isafoldproof}%
1.276 -%
1.277 -\isadelimproof
1.278 -%
1.279 -\endisadelimproof
1.280 -%
1.281 -\isadelimproof
1.282 -%
1.283 -\endisadelimproof
1.284 -%
1.285 -\isatagproof
1.286 -%
1.287 -\endisatagproof
1.288 -{\isafoldproof}%
1.289 -%
1.290 -\isadelimproof
1.291 -%
1.292 -\endisadelimproof
1.293 -%
1.294 -\isadelimproof
1.295 -%
1.296 -\endisadelimproof
1.297 -%
1.298 -\isatagproof
1.299 -%
1.300 -\endisatagproof
1.301 -{\isafoldproof}%
1.302 -%
1.303 -\isadelimproof
1.304 -%
1.305 -\endisadelimproof
1.306 -%
1.307 -\isadelimproof
1.308 -%
1.309 -\endisadelimproof
1.310 -%
1.311 -\isatagproof
1.312 -%
1.313 -\endisatagproof
1.314 -{\isafoldproof}%
1.315 -%
1.316 -\isadelimproof
1.317 -%
1.318 -\endisadelimproof
1.319 -%
1.320 -\isadelimproof
1.321 -%
1.322 -\endisadelimproof
1.323 -%
1.324 -\isatagproof
1.325 -%
1.326 -\endisatagproof
1.327 -{\isafoldproof}%
1.328 -%
1.329 -\isadelimproof
1.330 -%
1.331 -\endisadelimproof
1.332 -%
1.333 -\isadelimproof
1.334 -%
1.335 -\endisadelimproof
1.336 -%
1.337 -\isatagproof
1.338 -%
1.339 -\endisatagproof
1.340 -{\isafoldproof}%
1.341 -%
1.342 -\isadelimproof
1.343 -%
1.344 -\endisadelimproof
1.345 -%
1.346 -\isadelimproof
1.347 -%
1.348 -\endisadelimproof
1.349 -%
1.350 -\isatagproof
1.351 -%
1.352 -\endisatagproof
1.353 -{\isafoldproof}%
1.354 -%
1.355 -\isadelimproof
1.356 -%
1.357 -\endisadelimproof
1.358 -%
1.359 -\isadelimproof
1.360 -%
1.361 -\endisadelimproof
1.362 -%
1.363 -\isatagproof
1.364 -%
1.365 -\endisatagproof
1.366 -{\isafoldproof}%
1.367 -%
1.368 -\isadelimproof
1.369 -%
1.370 -\endisadelimproof
1.371 -%
1.372 -\isadelimproof
1.373 -%
1.374 -\endisadelimproof
1.375 -%
1.376 -\isatagproof
1.377 -%
1.378 -\endisatagproof
1.379 -{\isafoldproof}%
1.380 -%
1.381 -\isadelimproof
1.382 -%
1.383 -\endisadelimproof
1.384 -%
1.385 -\isadelimML
1.386 -%
1.387 -\endisadelimML
1.388 -%
1.389 -\isatagML
1.390 -%
1.391 -\endisatagML
1.392 -{\isafoldML}%
1.393 -%
1.394 -\isadelimML
1.395 -%
1.396 -\endisadelimML
1.397 -%
1.398 -\isadelimproof
1.399 -%
1.400 -\endisadelimproof
1.401 -%
1.402 -\isatagproof
1.403 -%
1.404 -\endisatagproof
1.405 -{\isafoldproof}%
1.406 -%
1.407 -\isadelimproof
1.408 -%
1.409 -\endisadelimproof
1.410 -%
1.411 -\isadelimproof
1.412 -%
1.413 -\endisadelimproof
1.414 -%
1.415 -\isatagproof
1.416 -%
1.417 -\endisatagproof
1.418 -{\isafoldproof}%
1.419 -%
1.420 -\isadelimproof
1.421 -%
1.422 -\endisadelimproof
1.423 -%
1.424 -\isadelimproof
1.425 -%
1.426 -\endisadelimproof
1.427 -%
1.428 -\isatagproof
1.429 -%
1.430 -\endisatagproof
1.431 -{\isafoldproof}%
1.432 -%
1.433 -\isadelimproof
1.434 -%
1.435 -\endisadelimproof
1.436 -%
1.437 -\isadelimML
1.438 -%
1.439 -\endisadelimML
1.440 -%
1.441 -\isatagML
1.442 -%
1.443 -\endisatagML
1.444 -{\isafoldML}%
1.445 -%
1.446 -\isadelimML
1.447 -%
1.448 -\endisadelimML
1.449 -%
1.450 -\isadelimML
1.451 -%
1.452 -\endisadelimML
1.453 -%
1.454 -\isatagML
1.455 -%
1.456 -\endisatagML
1.457 -{\isafoldML}%
1.458 -%
1.459 -\isadelimML
1.460 -%
1.461 -\endisadelimML
1.462 -%
1.463 -\isamarkupsection{Event Traces \label{sec:events}%
1.464 -}
1.465 -\isamarkuptrue%
1.466 -%
1.467 -\begin{isamarkuptext}%
1.468 -The system's behaviour is formalized as a set of traces of
1.469 -\emph{events}. The most important event, \isa{Says\ A\ B\ X}, expresses
1.470 -$A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$.
1.471 -A trace is simply a list, constructed in reverse
1.472 -using~\isa{{\isaliteral{23}{\isacharhash}}}. Other event types include reception of messages (when
1.473 -we want to make it explicit) and an agent's storing a fact.
1.474 -
1.475 -Sometimes the protocol requires an agent to generate a new nonce. The
1.476 -probability that a 20-byte random number has appeared before is effectively
1.477 -zero. To formalize this important property, the set \isa{used\ evs}
1.478 -denotes the set of all items mentioned in the trace~\isa{evs}.
1.479 -The function \isa{used} has a straightforward
1.480 -recursive definition. Here is the case for \isa{Says} event:
1.481 -\begin{isabelle}%
1.482 -\ \ \ \ \ used\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ parts\ {\isaliteral{7B}{\isacharbraceleft}}X{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ used\ evs%
1.483 -\end{isabelle}
1.484 -
1.485 -The function \isa{knows} formalizes an agent's knowledge. Mostly we only
1.486 -care about the spy's knowledge, and \isa{knows\ Spy\ evs} is the set of items
1.487 -available to the spy in the trace~\isa{evs}. Already in the empty trace,
1.488 -the spy starts with some secrets at his disposal, such as the private keys
1.489 -of compromised users. After each \isa{Says} event, the spy learns the
1.490 -message that was sent:
1.491 -\begin{isabelle}%
1.492 -\ \ \ \ \ knows\ Spy\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ X\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}%
1.493 -\end{isabelle}
1.494 -Combinations of functions express other important
1.495 -sets of messages derived from~\isa{evs}:
1.496 -\begin{itemize}
1.497 -\item \isa{analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}} is everything that the spy could
1.498 -learn by decryption
1.499 -\item \isa{synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is everything that the spy
1.500 -could generate
1.501 -\end{itemize}%
1.502 -\end{isamarkuptext}%
1.503 -\isamarkuptrue%
1.504 -%
1.505 -\isadelimtheory
1.506 -%
1.507 -\endisadelimtheory
1.508 -%
1.509 -\isatagtheory
1.510 -%
1.511 -\endisatagtheory
1.512 -{\isafoldtheory}%
1.513 -%
1.514 -\isadelimtheory
1.515 -%
1.516 -\endisadelimtheory
1.517 -\end{isabellebody}%
1.518 -%%% Local Variables:
1.519 -%%% mode: latex
1.520 -%%% TeX-master: "root"
1.521 -%%% End: