equal
deleted
inserted
replaced
254 \end{itemize} |
254 \end{itemize} |
255 |
255 |
256 \end{frame}} |
256 \end{frame}} |
257 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
257 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
258 |
258 |
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
260 \mode<presentation>{ |
260 \mode<presentation>{ |
261 \begin{frame}[c] |
261 \begin{frame}[c] |
262 \frametitle{Inference Rules} |
262 \frametitle{Inference Rules} |
263 |
263 |
264 \begin{center} |
264 \begin{center} |
265 \bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\ |
265 \bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\ |
266 |
266 |
267 \bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_2}} |
267 \bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_1}} |
268 \qquad |
268 \qquad |
269 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\ |
269 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\ |
270 |
270 |
271 \bl{\infer{\Gamma \vdash P\,\text{says}\, F}{\Gamma \vdash F}}\medskip\\ |
271 \bl{\infer{\Gamma \vdash P\,\text{says}\, F}{\Gamma \vdash F}}\medskip\\ |
272 |
272 |
523 \end{center}\medskip\pause |
523 \end{center}\medskip\pause |
524 |
524 |
525 \item Decryption of Alice's message\smallskip |
525 \item Decryption of Alice's message\smallskip |
526 \begin{center} |
526 \begin{center} |
527 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
527 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
528 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash K}}} |
528 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
529 \end{center} |
529 \end{center} |
530 \end{itemize} |
530 \end{itemize} |
531 |
531 |
532 \end{frame}} |
532 \end{frame}} |
533 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
533 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
539 |
539 |
540 \begin{itemize} |
540 \begin{itemize} |
541 \item Encryption of a message\smallskip |
541 \item Encryption of a message\smallskip |
542 \begin{center} |
542 \begin{center} |
543 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
543 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
544 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash K}}} |
544 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
545 \end{center} |
545 \end{center} |
546 \end{itemize} |
546 \end{itemize} |
547 |
547 |
548 \end{frame}} |
548 \end{frame}} |
549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
614 \begin{center} |
614 \begin{center} |
615 \bl{\begin{tabular}{l} |
615 \bl{\begin{tabular}{l} |
616 $A$ sends $S$ : $\textit{Connect}(A,B)$\\ |
616 $A$ sends $S$ : $\textit{Connect}(A,B)$\\ |
617 \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ |
617 \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ |
618 \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge |
618 \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge |
619 \{\{K_{AB}\}_{K_{BS}}\}\_{K_{AS}})$}\\ |
619 \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\ |
620 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
620 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
621 $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\ |
621 $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\ |
622 $A$ sends $B$ : $\{m\}_{K_{AB}}$ |
622 $A$ sends $B$ : $\{m\}_{K_{AB}}$ |
623 \end{tabular}} |
623 \end{tabular}} |
624 \end{center}\bigskip\pause |
624 \end{center}\bigskip\pause |