320 \frametitle{} |
329 \frametitle{} |
321 |
330 |
322 Recall the following scenario: |
331 Recall the following scenario: |
323 |
332 |
324 \begin{itemize} |
333 \begin{itemize} |
325 \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
334 \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}} |
326 should be deleted, then this file must be deleted. |
335 should be deleted, then this file must be deleted. |
327 \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether |
336 \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether |
328 \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted. |
337 \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted. |
329 \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}. |
338 \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}. |
330 \end{itemize}\bigskip |
339 \end{itemize}\bigskip |
331 |
340 |
332 \small |
341 \small |
333 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
342 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
334 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\ |
343 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\ |
335 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\ |
344 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\ |
336 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\ |
345 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\ |
337 \end{tabular}}\medskip |
346 \end{tabular}}\medskip |
338 |
347 |
339 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
348 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}} |
340 \end{frame}} |
349 \end{frame}} |
341 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
342 |
351 |
343 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
352 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
344 \mode<presentation>{ |
353 \mode<presentation>{ |
418 \item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption |
427 \item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption |
419 \bl{$F_2$}.\bigskip |
428 \bl{$F_2$}.\bigskip |
420 \begin{center} |
429 \begin{center} |
421 \bl{$F_2, \Gamma \vdash \text{Pred}$} |
430 \bl{$F_2, \Gamma \vdash \text{Pred}$} |
422 \end{center} |
431 \end{center} |
423 |
|
424 \end{enumerate} |
432 \end{enumerate} |
425 |
433 |
|
434 \only<4>{ |
|
435 \begin{textblock}{11}(1,10.5) |
|
436 \bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}} |
|
437 \end{textblock}} |
|
438 |
|
439 |
426 \end{frame}} |
440 \end{frame}} |
427 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
441 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
428 |
442 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions |
|
443 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
444 \mode<presentation>{ |
|
445 \begin{frame}[c] |
|
446 |
|
447 \begin{itemize} |
|
448 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ |
|
449 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip |
|
450 |
|
451 \begin{center} |
|
452 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}} |
|
453 \end{center} |
|
454 |
|
455 \item \bl{$P$} speaks for \bl{$Q$}\smallskip\\ |
|
456 \bl{$P \mapsto Q \,\dn\, \forall F. (P\,\text{says}\, F) \Rightarrow (Q \,\text{says}\,F)$}\medskip |
|
457 |
|
458 \begin{center} |
|
459 \bl{\infer{\Gamma \vdash Q\,\text{says}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash P\,\text{says}\,F}} |
|
460 \medskip\\ |
|
461 \bl{\infer{\Gamma \vdash P\,\text{controls}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash Q\,\text{controls}\,F}}\\ |
|
462 |
|
463 \end{center} |
|
464 \end{itemize} |
|
465 |
|
466 \end{frame}} |
|
467 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
468 |
|
469 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
470 \mode<presentation>{ |
|
471 \begin{frame}[c] |
|
472 \frametitle{Protocol Specifications} |
|
473 |
|
474 The Needham-Schroeder Protocol: |
|
475 |
|
476 \begin{center} |
|
477 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
478 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B, N_A$}\\ |
|
479 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\ |
|
480 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}, A\}_{K_{BS}} $}\\ |
|
481 Message 4 & \bl{$B \rightarrow A :$} & \bl{$\{N_B\}_{K_{AB}}$}\\ |
|
482 Message 5 & \bl{$A \rightarrow B :$} & \bl{$\{N_B-1\}_{K_{AB}}$}\\ |
|
483 \end{tabular} |
|
484 \end{center} |
|
485 |
|
486 \end{frame}} |
|
487 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
488 |
|
489 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
490 \mode<presentation>{ |
|
491 \begin{frame}[c] |
|
492 \frametitle{Trusted Third Party} |
|
493 |
|
494 Simple protocol for establishing a secure connection via a mutually |
|
495 trusted 3rd party (server): |
|
496 |
|
497 \begin{center} |
|
498 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
499 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\ |
|
500 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\ |
|
501 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\ |
|
502 Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\ |
|
503 \end{tabular} |
|
504 \end{center} |
|
505 |
|
506 \end{frame}} |
|
507 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
508 |
|
509 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
510 \mode<presentation>{ |
|
511 \begin{frame}[c] |
|
512 \frametitle{Sending Messages} |
|
513 |
|
514 \begin{itemize} |
|
515 \item Alice sends a message \bl{$m$} |
|
516 \begin{center} |
|
517 \bl{Alice says $m$} |
|
518 \end{center}\medskip\pause |
|
519 |
|
520 \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$}) |
|
521 \begin{center} |
|
522 \bl{Alice says $\{m\}_K$} |
|
523 \end{center}\medskip\pause |
|
524 |
|
525 \item Decryption of Alice's message\smallskip |
|
526 \begin{center} |
|
527 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
528 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash K}}} |
|
529 \end{center} |
|
530 \end{itemize} |
|
531 |
|
532 \end{frame}} |
|
533 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
534 |
|
535 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
536 \mode<presentation>{ |
|
537 \begin{frame}[c] |
|
538 \frametitle{Encryption} |
|
539 |
|
540 \begin{itemize} |
|
541 \item Encryption of a message\smallskip |
|
542 \begin{center} |
|
543 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
|
544 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash K}}} |
|
545 \end{center} |
|
546 \end{itemize} |
|
547 |
|
548 \end{frame}} |
|
549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
550 |
429 \end{document} |
551 \end{document} |
430 |
552 |
431 %%% Local Variables: |
553 %%% Local Variables: |
432 %%% mode: latex |
554 %%% mode: latex |
433 %%% TeX-master: t |
555 %%% TeX-master: t |