548 \end{quote} |
554 \end{quote} |
549 |
555 |
550 \end{frame}} |
556 \end{frame}} |
551 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
557 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
552 |
558 |
|
559 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
560 \mode<presentation>{ |
|
561 \begin{frame}[t] |
|
562 \frametitle{\Large\begin{tabular}{@ {}c@ {}}Logic(s)\end{tabular}} |
|
563 |
|
564 \begin{itemize} |
|
565 \item Formulas |
|
566 |
|
567 \begin{center}\color{blue} |
|
568 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
|
569 \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\ |
|
570 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\ |
|
571 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\ |
|
572 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\ |
|
573 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F} & \textcolor{black}{implies}\\ |
|
574 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F} & \textcolor{black}{negation}\\ |
|
575 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} & \textcolor{black}{predicates}\\ |
|
576 & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}} & |
|
577 \onslide<2->{\textcolor{black}{forall quantification}}\\ |
|
578 & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ F}} & |
|
579 \onslide<2->{\textcolor{black}{exists quantification}}\\[-7mm] |
|
580 \end{tabular} |
|
581 \end{center} |
|
582 |
|
583 \end{itemize} |
|
584 |
|
585 \begin{textblock}{12}(1,14) |
|
586 Terms \textcolor{blue}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{7C}{\isacharbar}}\ c\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}} |
|
587 \end{textblock} |
|
588 |
|
589 \end{frame}} |
|
590 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
591 % |
|
592 |
|
593 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
594 \mode<presentation>{ |
|
595 \begin{frame}[c] |
|
596 |
|
597 {\lstset{language=Scala}\fontsize{10}{12}\selectfont |
|
598 \texttt{\lstinputlisting{../programs/formulas.scala}}} |
|
599 |
|
600 \end{frame}} |
|
601 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
602 |
|
603 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
604 \mode<presentation>{ |
|
605 \begin{frame}[t] |
|
606 \frametitle{Judgements} |
|
607 |
|
608 \begin{center} |
|
609 \LARGE |
|
610 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}} |
|
611 \end{center} |
|
612 |
|
613 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} is a collection of formulas, called the \alert{assumptions}\bigskip\pause |
|
614 |
|
615 \begin{itemize} |
|
616 \item Example\mbox{}\\[-3mm] |
|
617 |
|
618 \only<2>{\begin{center}\tiny |
|
619 \textcolor{blue}{ |
|
620 \begin{tabular}{l} |
|
621 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
622 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
623 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
624 \end{tabular}\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} |
|
625 \end{center}} |
|
626 \only<3>{\small |
|
627 \textcolor{blue}{ |
|
628 \begin{center} |
|
629 \mbox{ |
|
630 \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
631 {\mbox{\begin{tabular}{@ {}l@ {}} |
|
632 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
633 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
634 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
635 \end{tabular}} |
|
636 } |
|
637 } |
|
638 \end{center} |
|
639 }} |
|
640 \only<4>{\small |
|
641 \textcolor{blue}{ |
|
642 \begin{center} |
|
643 \mbox{ |
|
644 \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}} |
|
645 {\mbox{\begin{tabular}{@ {}l@ {}} |
|
646 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}\\ |
|
647 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
648 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
649 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
650 \end{tabular}} |
|
651 } |
|
652 } |
|
653 \end{center} |
|
654 }} |
|
655 |
|
656 \end{itemize} |
|
657 |
|
658 \end{frame}} |
|
659 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
660 |
|
661 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
662 \mode<presentation>{ |
|
663 \begin{frame}[c] |
|
664 |
|
665 {\lstset{language=Scala}\fontsize{10}{12}\selectfont |
|
666 \texttt{\lstinputlisting{../programs/judgement.scala}}} |
|
667 |
|
668 \end{frame}} |
|
669 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
670 |
|
671 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
672 \mode<presentation>{ |
|
673 \begin{frame}[t] |
|
674 \frametitle{Inference Rules} |
|
675 |
|
676 \textcolor{blue}{ |
|
677 \begin{center} |
|
678 \Large |
|
679 \mbox{ |
|
680 \infer{\mbox{\isa{conclusion}}} |
|
681 {\mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}} & \mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub n}}}} |
|
682 \end{center}} |
|
683 |
|
684 The conlusion and premises are judgements\bigskip\pause |
|
685 |
|
686 \begin{itemize} |
|
687 \item Examples |
|
688 \textcolor{blue}{ |
|
689 \begin{center} |
|
690 \mbox{ |
|
691 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
692 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} |
|
693 \end{center}}\pause |
|
694 |
|
695 \textcolor{blue}{ |
|
696 \begin{center} |
|
697 \mbox{ |
|
698 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
699 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
700 \hspace{10mm} |
|
701 \mbox{ |
|
702 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
703 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} |
|
704 \end{center}} |
|
705 \end{itemize} |
|
706 |
|
707 \end{frame}} |
|
708 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
709 % |
|
710 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
711 \mode<presentation>{ |
|
712 \begin{frame}[t] |
|
713 \frametitle{Implication} |
|
714 \Large |
|
715 |
|
716 \textcolor{blue}{ |
|
717 \begin{center} |
|
718 \mbox{ |
|
719 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
720 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} |
|
721 \end{center}} |
|
722 |
|
723 \textcolor{blue}{ |
|
724 \begin{center} |
|
725 \mbox{ |
|
726 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
727 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
728 \end{center}} |
|
729 |
|
730 \end{frame}} |
|
731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
732 % |
|
733 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
734 \mode<presentation>{ |
|
735 \begin{frame}[t] |
|
736 \frametitle{Universal Quantification} |
|
737 \Large |
|
738 |
|
739 \textcolor{blue}{ |
|
740 \begin{center} |
|
741 \mbox{ |
|
742 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F{\isaliteral{5B}{$\isacharbrackleft$}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5D}{$\isacharbrackright$}}}}} |
|
743 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}}}} |
|
744 \end{center}} |
|
745 |
|
746 \end{frame}} |
|
747 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
748 % |
|
749 |
|
750 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
751 \mode<presentation>{ |
|
752 \begin{frame}[t] |
|
753 \frametitle{Start Rules / Axioms} |
|
754 |
|
755 \normalsize |
|
756 \alert{if \textcolor{blue}{\isa{F\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}} |
|
757 |
|
758 \textcolor{blue}{\Large |
|
759 \begin{center} |
|
760 \mbox{ |
|
761 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}} |
|
762 \end{center}}\bigskip\pause |
|
763 |
|
764 \normalsize |
|
765 Also written as: |
|
766 \textcolor{blue}{\Large |
|
767 \begin{center} |
|
768 \mbox{ |
|
769 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}} |
|
770 \end{center}}\pause |
|
771 |
|
772 \textcolor{blue}{\Large |
|
773 \begin{center} |
|
774 \mbox{ |
|
775 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ true}}}{}} |
|
776 \end{center}} |
|
777 |
|
778 \end{frame}} |
|
779 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
780 % |
|
781 |
|
782 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
783 \mode<presentation>{ |
|
784 \begin{frame}[t] |
|
785 \frametitle{} |
|
786 |
|
787 \begin{minipage}{1.1\textwidth} |
|
788 Let \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\footnotesize\begin{tabular}{l} |
|
789 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
790 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
791 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
792 \end{tabular}} |
|
793 \end{minipage} |
|
794 |
|
795 \only<2>{ |
|
796 \begin{textblock}{12}(4,3)\footnotesize |
|
797 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}\hspace{10mm} |
|
798 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} |
|
799 \end{textblock}} |
|
800 |
|
801 \only<3->{ |
|
802 \begin{textblock}{12}(4,3)\footnotesize |
|
803 \mbox{\textcolor{blue}{ |
|
804 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
805 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} &\hspace{10mm} |
|
806 \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
807 }} |
|
808 \end{textblock}} |
|
809 |
|
810 \only<4>{ |
|
811 \begin{textblock}{14}(0.5,6)\footnotesize |
|
812 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}} |
|
813 \end{textblock}} |
|
814 |
|
815 \only<5->{ |
|
816 \begin{textblock}{14}(0.5,6)\footnotesize |
|
817 \textcolor{blue}{ |
|
818 \infer{\mbox{\begin{tabular}{l}\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
819 \hspace{40mm}\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\end{tabular}}} |
|
820 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}}}} |
|
821 \end{textblock}} |
|
822 |
|
823 \only<6->{ |
|
824 \begin{textblock}{14}(5,10)\footnotesize |
|
825 \textcolor{blue}{ |
|
826 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
827 {\vdots & \hspace{30mm} \vdots}} |
|
828 \end{textblock}} |
|
829 |
|
830 \end{frame}} |
|
831 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
832 % |
|
833 |
|
834 |
|
835 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
836 \mode<presentation>{ |
|
837 \begin{frame}[t] |
|
838 \frametitle{Access Control} |
|
839 \Large |
|
840 |
|
841 \textcolor{blue}{ |
|
842 \begin{center} |
|
843 \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F} |
|
844 \end{center}}\bigskip |
|
845 |
|
846 \normalsize |
|
847 \begin{itemize} |
|
848 \item If there is a proof \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} yes (granted) |
|
849 \item If there isn't \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} no (denied) |
|
850 \end{itemize}\bigskip\pause |
|
851 |
|
852 \begin{minipage}{1.1\textwidth} |
|
853 \small |
|
854 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
855 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
856 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
857 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
858 \end{tabular}}\medskip |
|
859 |
|
860 \textcolor{blue}{ |
|
861 \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} $\not\vdash$ \isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}} |
|
862 \end{minipage} |
|
863 \end{frame}} |
|
864 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
865 % |
|
866 |
|
867 |
|
868 |
|
869 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
870 \mode<presentation>{ |
|
871 \begin{frame}[c] |
|
872 \frametitle{The Access Control Problem} |
|
873 |
|
874 |
|
875 \begin{center} |
|
876 \begin{tikzpicture}[scale=1] |
|
877 |
|
878 \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); |
|
879 \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; |
|
880 \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}}; |
|
881 \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}}; |
|
882 |
|
883 \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); |
|
884 \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); |
|
885 \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); |
|
886 |
|
887 \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}}; |
|
888 |
|
889 \end{tikzpicture} |
|
890 \end{center} |
|
891 |
|
892 \end{frame}} |
|
893 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
894 |
|
895 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
896 \mode<presentation>{ |
|
897 \begin{frame}[c] |
|
898 \frametitle{Bad News} |
|
899 |
|
900 \begin{itemize} |
|
901 \item We introduced (roughly) first-order logic. \bigskip\pause |
|
902 |
|
903 \item Judgements |
|
904 \begin{center} |
|
905 \textcolor{blue} |
|
906 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} |
|
907 \end{center} |
|
908 |
|
909 are in general \alert{undecidable}.\pause\medskip\\ |
|
910 |
|
911 The problem is \alert{semi-decidable}. |
|
912 |
|
913 \end{itemize} |
|
914 |
|
915 |
|
916 \end{frame}} |
|
917 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
918 % |
|
919 |
|
920 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
921 \mode<presentation>{ |
|
922 \begin{frame}[t] |
|
923 \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}} |
|
924 |
|
925 \begin{itemize} |
|
926 \item[] |
|
927 |
|
928 \begin{center}\color{blue} |
|
929 \begin{tabular}[t]{rcl@ {\hspace{10mm}}l} |
|
930 \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\ |
|
931 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\ |
|
932 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\ |
|
933 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\ |
|
934 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\ |
|
935 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} \\ |
|
936 & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\ |
|
937 \end{tabular} |
|
938 \end{center}\medskip |
|
939 |
|
940 where \textcolor{blue}{\isa{P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ Alice{\isaliteral{2C}{\isacharcomma}}\ Bob{\isaliteral{2C}{\isacharcomma}}\ Christian{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}} (principals)\bigskip\pause |
|
941 |
|
942 \item \textcolor{blue}{\isa{HoD\ says\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} |
|
943 \end{itemize} |
|
944 |
|
945 |
|
946 |
|
947 \end{frame}} |
|
948 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
949 % |
|
950 |
|
951 |
|
952 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
953 \mode<presentation>{ |
|
954 \begin{frame}[c] |
|
955 |
|
956 {\lstset{language=Scala}\fontsize{10}{12}\selectfont |
|
957 \texttt{\lstinputlisting{../programs/formulas1.scala}}} |
|
958 |
|
959 \end{frame}} |
|
960 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
961 |
|
962 |
|
963 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
964 \mode<presentation>{ |
|
965 \begin{frame}[t] |
|
966 \frametitle{Rules about Says} |
|
967 |
|
968 \textcolor{blue}{ |
|
969 \begin{center} |
|
970 \mbox{ |
|
971 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
972 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}} |
|
973 \end{center}} |
|
974 |
|
975 \textcolor{blue}{ |
|
976 \begin{center} |
|
977 \mbox{ |
|
978 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
979 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{10mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
980 \end{center}} |
|
981 |
|
982 \textcolor{blue}{ |
|
983 \begin{center} |
|
984 \mbox{ |
|
985 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
986 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}}}}} |
|
987 \end{center}} |
|
988 |
|
989 \end{frame}} |
|
990 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
991 % |
|
992 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
993 \mode<presentation>{ |
|
994 \begin{frame}[c] |
|
995 \frametitle{} |
|
996 |
|
997 Consider the following scenario: |
|
998 |
|
999 \begin{itemize} |
|
1000 \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
|
1001 should be deleted, then this file must be deleted. |
|
1002 \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether |
|
1003 \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted. |
|
1004 \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}. |
|
1005 \end{itemize}\bigskip\pause |
|
1006 |
|
1007 \small |
|
1008 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
1009 \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}}},\\ |
|
1010 \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}}},\\ |
|
1011 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\ |
|
1012 \end{tabular}}\medskip\pause |
|
1013 |
|
1014 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
|
1015 \end{frame}} |
|
1016 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1017 % |
|
1018 |
|
1019 |
|
1020 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1021 \mode<presentation>{ |
|
1022 \begin{frame}[c] |
|
1023 \frametitle{} |
|
1024 |
|
1025 \textcolor{blue}{ |
|
1026 \begin{center} |
|
1027 \mbox{ |
|
1028 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1029 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}\\\bigskip |
|
1030 \mbox{ |
|
1031 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
1032 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{5mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
1033 \end{center}}\bigskip |
|
1034 |
|
1035 \small |
|
1036 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
1037 \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}}},\\ |
|
1038 \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}}},\\ |
|
1039 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\ |
|
1040 \end{tabular}}\medskip |
|
1041 |
|
1042 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
|
1043 \end{frame}} |
|
1044 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1045 % |
|
1046 |
|
1047 |
|
1048 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1049 \mode<presentation>{ |
|
1050 \begin{frame}[t] |
|
1051 \frametitle{} |
|
1052 \small |
|
1053 |
|
1054 \textcolor{blue}{ |
|
1055 \begin{center} |
|
1056 \only<1>{$ \underbrace{ |
|
1057 \mbox{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file)}} |
|
1058 {\infer{\Gamma \vdash \mbox{Bob says del\_file}}{}}}}_{X}$} |
|
1059 \end{center}} |
|
1060 |
|
1061 \textcolor{blue}{ |
|
1062 \begin{center} |
|
1063 \only<1>{ |
|
1064 $ \underbrace{ |
|
1065 \mbox{\infer{\Gamma \vdash \mbox{Admin says del\_file}} |
|
1066 {\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file)}}{} |
|
1067 & |
|
1068 \deduce[$\vdots$]{X}{} |
|
1069 }}}_{Y}$} |
|
1070 \end{center}} |
|
1071 |
|
1072 \textcolor{blue}{ |
|
1073 \begin{center} |
|
1074 \only<1>{\mbox{\infer{\Gamma \vdash \mbox{del\_file}} |
|
1075 {\infer{\Gamma \vdash \mbox{(Admin says del\_file) \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file}}{} |
|
1076 & |
|
1077 \deduce[$\vdots$]{Y}{} |
|
1078 }}} |
|
1079 \end{center}} |
|
1080 |
|
1081 \end{frame}} |
|
1082 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1083 % |
|
1084 |
|
1085 |
|
1086 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1087 \mode<presentation>{ |
|
1088 \begin{frame}[c] |
|
1089 \frametitle{Controls} |
|
1090 \small |
|
1091 |
|
1092 \begin{itemize} |
|
1093 \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} |
|
1094 |
|
1095 \item its meaning ``\bl{P} is entitled to do \bl{F}'' |
|
1096 \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause |
|
1097 |
|
1098 \begin{center} |
|
1099 \bl{\mbox{ |
|
1100 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} |
|
1101 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1102 }} |
|
1103 \end{center}\pause |
|
1104 |
|
1105 \begin{center} |
|
1106 \bl{\mbox{ |
|
1107 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} |
|
1108 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1109 }} |
|
1110 \end{center} |
|
1111 \end{itemize} |
|
1112 |
|
1113 \end{frame}} |
|
1114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1115 % |
|
1116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1117 \mode<presentation>{ |
|
1118 \begin{frame}[c] |
|
1119 \frametitle{Speaks For} |
|
1120 \small |
|
1121 |
|
1122 \begin{itemize} |
|
1123 \item \bl{\isa{P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}F{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ says\ F{\isaliteral{29}{\isacharparenright}}}} |
|
1124 |
|
1125 \item its meaning ``\bl{P} speaks for \bl{Q}'' |
|
1126 |
|
1127 |
|
1128 \begin{center} |
|
1129 \bl{\mbox{ |
|
1130 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}} |
|
1131 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1132 }} |
|
1133 \end{center}\pause |
|
1134 |
|
1135 \begin{center} |
|
1136 \bl{\mbox{ |
|
1137 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}}} |
|
1138 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ controls\ F}}} |
|
1139 }} |
|
1140 \end{center} |
|
1141 |
|
1142 \begin{center} |
|
1143 \bl{\mbox{ |
|
1144 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}} |
|
1145 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}} |
|
1146 }} |
|
1147 \end{center} |
|
1148 \end{itemize} |
|
1149 |
|
1150 \end{frame}} |
|
1151 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1152 % |
|
1153 |
|
1154 |
|
1155 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1156 \mode<presentation>{ |
|
1157 \begin{frame}[c] |
|
1158 \frametitle{Security Levels} |
|
1159 \small |
|
1160 |
|
1161 \begin{itemize} |
|
1162 \item Top secret (\bl{$T\!S$}) |
|
1163 \item Secret (\bl{$S$}) |
|
1164 \item Public (\bl{$P$}) |
|
1165 \end{itemize} |
|
1166 |
|
1167 \begin{center} |
|
1168 \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause |
|
1169 \end{center} |
|
1170 |
|
1171 \begin{itemize} |
|
1172 \item Bob has a clearance for ``secret'' |
|
1173 \item Bob can read documents that are public or sectret, but not top secret |
|
1174 \end{itemize} |
|
1175 |
|
1176 \end{frame}} |
|
1177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1178 % |
|
1179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1180 \mode<presentation>{ |
|
1181 \begin{frame}[c] |
|
1182 \frametitle{Reading a File} |
|
1183 |
|
1184 \bl{\begin{center} |
|
1185 \begin{tabular}{c} |
|
1186 \begin{tabular}{@ {}l@ {}} |
|
1187 \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\ |
|
1188 \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\ |
|
1189 Bob says Permitted $($File, read$)$\only<2->{\\} |
|
1190 \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}% |
|
1191 \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}% |
|
1192 \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}% |
|
1193 \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}% |
|
1194 \end{tabular}\\ |
|
1195 \hline |
|
1196 Permitted $($File, read$)$ |
|
1197 \end{tabular} |
|
1198 \end{center}} |
|
1199 |
|
1200 \end{frame}} |
|
1201 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1202 % |
|
1203 |
|
1204 |
|
1205 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1206 \mode<presentation>{ |
|
1207 \begin{frame}[c] |
|
1208 \frametitle{Substitution Rule} |
|
1209 \small |
|
1210 |
|
1211 \bl{\begin{center} |
|
1212 \begin{tabular}{c} |
|
1213 $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$ |
|
1214 \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline |
|
1215 $\Gamma \vdash slev(P) < slev(Q)$ |
|
1216 \end{tabular} |
|
1217 \end{center}}\bigskip\pause |
|
1218 |
|
1219 \begin{itemize} |
|
1220 \item \bl{$slev($Bob$)$ $=$ $S$} |
|
1221 \item \bl{$slev($File$)$ $=$ $P$} |
|
1222 \item \bl{$slev(P) < slev(S)$} |
|
1223 \end{itemize} |
|
1224 |
|
1225 \end{frame}} |
|
1226 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1227 % |
|
1228 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1229 \mode<presentation>{ |
|
1230 \begin{frame}[c] |
|
1231 \frametitle{Reading a File} |
|
1232 |
|
1233 \bl{\begin{center} |
|
1234 \begin{tabular}{c} |
|
1235 \begin{tabular}{@ {}l@ {}} |
|
1236 $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\ |
|
1237 \hspace{3cm}Bob controls Permitted $($File, read$)$\\ |
|
1238 Bob says Permitted $($File, read$)$\\ |
|
1239 $slev($File$)$ $=$ $P$\\ |
|
1240 $slev($Bob$)$ $=$ $T\!S$\\ |
|
1241 \only<1>{\textcolor{red}{$?$}}% |
|
1242 \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}% |
|
1243 \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}% |
|
1244 \end{tabular}\\ |
|
1245 \hline |
|
1246 Permitted $($File, read$)$ |
|
1247 \end{tabular} |
|
1248 \end{center}} |
|
1249 |
|
1250 \end{frame}} |
|
1251 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1252 % |
|
1253 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1254 \mode<presentation>{ |
|
1255 \begin{frame}[c] |
|
1256 \frametitle{Transitivity Rule} |
|
1257 \small |
|
1258 |
|
1259 \bl{\begin{center} |
|
1260 \begin{tabular}{c} |
|
1261 $\Gamma \vdash l_1 < l_2$ |
|
1262 \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline |
|
1263 $\Gamma \vdash l_1 < l_3$ |
|
1264 \end{tabular} |
|
1265 \end{center}}\bigskip |
|
1266 |
|
1267 \begin{itemize} |
|
1268 \item \bl{$slev(P) < slev (S)$} |
|
1269 \item \bl{$slev(S) < slev (T\!S)$} |
|
1270 \item[] \bl{$slev(P) < slev (T\!S)$} |
|
1271 \end{itemize} |
|
1272 |
|
1273 \end{frame}} |
|
1274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1275 % |
|
1276 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1277 \mode<presentation>{ |
|
1278 \begin{frame}[c] |
|
1279 \frametitle{Reading Files} |
|
1280 |
|
1281 \begin{itemize} |
|
1282 \item Access policy for reading |
|
1283 \end{itemize} |
|
1284 |
|
1285 \bl{\begin{center} |
|
1286 \begin{tabular}{c} |
|
1287 \begin{tabular}{@ {}l@ {}} |
|
1288 $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\ |
|
1289 \hspace{3cm}Bob controls Permitted $(f$, read$)$\\ |
|
1290 Bob says Permitted $($File, read$)$\\ |
|
1291 $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\ |
|
1292 $slev($Bob$)$ $=$ $T\!S$\\ |
|
1293 $slev(P) < slev(S)$\\ |
|
1294 $slev(S) < slev(T\!S)$ |
|
1295 \end{tabular}\\ |
|
1296 \hline |
|
1297 Permitted $($File, read$)$ |
|
1298 \end{tabular} |
|
1299 \end{center}} |
|
1300 |
|
1301 \end{frame}} |
|
1302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1303 % |
|
1304 |
|
1305 |
|
1306 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1307 \mode<presentation>{ |
|
1308 \begin{frame}[c] |
|
1309 \frametitle{Writing Files} |
|
1310 |
|
1311 \begin{itemize} |
|
1312 \item Access policy for \underline{writing} |
|
1313 \end{itemize} |
|
1314 |
|
1315 \bl{\begin{center} |
|
1316 \begin{tabular}{c} |
|
1317 \begin{tabular}{@ {}l@ {}} |
|
1318 $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\ |
|
1319 \hspace{3cm}Bob controls Permitted $(f$, write$)$\\ |
|
1320 Bob says Permitted $($File, write$)$\\ |
|
1321 $slev($File$)$ $=$ $T\!S$\\ |
|
1322 $slev($Bob$)$ $=$ $S$\\ |
|
1323 $slev(P) < slev(S)$\\ |
|
1324 $slev(S) < slev(T\!S)$ |
|
1325 \end{tabular}\\ |
|
1326 \hline |
|
1327 Permitted $($File, write$)$ |
|
1328 \end{tabular} |
|
1329 \end{center}} |
|
1330 |
|
1331 \end{frame}} |
|
1332 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1333 % |
553 |
1334 |
554 \end{document} |
1335 \end{document} |
555 |
1336 |
556 %%% Local Variables: |
1337 %%% Local Variables: |
557 %%% mode: latex |
1338 %%% mode: latex |