175   

   176 

   177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   178 \mode<presentation>{

   179 \begin{frame}[c]

   180 \frametitle{Judgements}

   181 

   182 \begin{center}

   183 \begin{tikzpicture}[scale=1]

   184   

   185   \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};

   186   \onslide<2->{

   187   \draw (-1,-0.3) node (X) {};

   188   \draw (-2.0,-2.0) node (Y) {};

   189   \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}};

   190   \draw[red, ->, line width = 2mm] (Y) -- (X);

   191  

   192   \draw (1.2,-0.1) node (X1) {};

   193   \draw (2.8,-0.1) node (Y1) {};

   194   \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}};

   195   \draw[red, ->, line width = 2mm] (Y1) -- (X1);

   196 

   197   \draw (-0.1,0.1) node (X2) {};

   198   \draw (0.5,1.5) node (Y2) {};

   199   \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}};

   200   \draw[red, ->, line width = 2mm] (Y2) -- (X2);}

   201   

   202   \end{tikzpicture}

   203 \end{center}

   204 

   205 \end{frame}}

   206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   207   

   208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   209 \mode<presentation>{

   210 \begin{frame}[c]

   211 \frametitle{Inference Rules}

   212 

   213 \begin{center}

   214 \begin{tikzpicture}[scale=1]

   215   

   216   \draw (0.0,0.0) node 

   217   {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}};

   218  

   219   \draw (-0.1,-0.7) node (X) {};

   220   \draw (-0.1,-1.9) node (Y) {};

   221   \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}};

   222   \draw[red, ->, line width = 2mm] (Y) -- (X);

   223  

   224   \draw (-1,0.6) node (X2) {};

   225   \draw (0.0,1.6) node (Y2) {};

   226   \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}};

   227   \draw[red, ->, line width = 2mm] (Y2) -- (X2);

   228    \draw (1,0.6) node (X3) {};

   229   \draw (0.0,1.6) node (Y3) {};

   230   \draw[red, ->, line width = 2mm] (Y3) -- (X3);

   231   \end{tikzpicture}

   232 \end{center}

   233 

   234 \only<2>{

   235 \begin{textblock}{11}(1,13)

   236 \small

   237 \bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}

   238 \end{textblock}}

   239 \only<3>{

   240 \begin{textblock}{11}(1,13)

   241 \small

   242 \bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge

   243         \underbrace{P \,\text{says}\, G}_{F_2} $}

   244 \end{textblock}}

   245 

   246 \end{frame}}

   247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   248 

   249 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   250   \mode<presentation>{

   251   \begin{frame}[c]

   252   \frametitle{Sending Messages}

   253 

   254   \begin{itemize}

   255   \item Alice sends a message \bl{$m$}

   256   \begin{center}

   257   \bl{Alice says $m$}

   258   \end{center}\medskip\pause

   259 

   260   \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$})

   261   \begin{center}

   262   \bl{Alice says $\{m\}_K$}

   263   \end{center}\medskip\pause

   264 

   265   \item Decryption of Alice's message\smallskip

   266   \begin{center}

   267   \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}

   268               {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}

   269   \end{center}

   270   \end{itemize}

   271 

   272   \end{frame}}

   273   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   296 

   317 

   318 

   639 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   640 \mode<presentation>{

   641 \begin{frame}[c]

   642 \frametitle{Example Proof}

   643 

   644 \begin{center}

   645 \bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1}

   646          {\raisebox{2mm}{\text{\LARGE $?$}}}}

   647 \end{center}

   648 

   649 

   650 \end{frame}}

   651 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   652 

   653 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   654 \mode<presentation>{

   655 \begin{frame}[c]

   656 \frametitle{Example Proof}

   657 

   658 \begin{tabular}{@{\hspace{-6mm}}l}

   659 \begin{minipage}{1.1\textwidth}

   660 We have (by axiom)

   661 

   662 \begin{center}

   663 \begin{tabular}{@{}ll@{}}

   664 (1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$}

   665 \end{tabular}

   666 \end{center}

   667 

   668 From (1) we get

   669 

   670 \begin{center}

   671 \begin{tabular}{@{}ll@{}}

   672 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\

   673 (3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\

   674 \end{tabular}

   675 \end{center}

   676 

   677 From (3) and (2) we get

   678 

   679 \begin{center}

   680 \begin{tabular}{@{}ll@{}}

   681 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}

   682 \end{tabular}

   683 \end{center}

   684 

   685 Done.

   686 \end{minipage}

   687 \end{tabular}

   688 

   689 \end{frame}}

   690 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   691 

   692 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   693 \mode<presentation>{

   694 \begin{frame}[c]

   695 \frametitle{Other Direction}

   696 

   697 \begin{tabular}{@{\hspace{-6mm}}l}

   698 \begin{minipage}{1.1\textwidth}

   699 We want to prove

   700 

   701 \begin{center}

   702 \begin{tabular}{@{}ll@{}}

   703 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}

   704 \end{tabular}

   705 \end{center}

   706 

   707 We are better be able to prove:

   708 

   709 \begin{center}

   710 \begin{tabular}{@{}ll@{}}

   711 (1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\

   712 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\

   713 \end{tabular}

   714 \end{center}

   715 

   716 For (1): If we can prove

   717 

   718 \begin{center}

   719 \begin{tabular}{@{}ll@{}}

   720 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}

   721 \end{tabular}

   722 \end{center}

   723 

   724 then (1) is fine. Similarly for (2).

   725 \end{minipage}

   726 \end{tabular}

   727 

   728 \end{frame}}

   729 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

   730      

   731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   732   \mode<presentation>{

   733   \begin{frame}[c]

   734   \frametitle{}

   735 

   736   Recall the following scenario:

   737 

   738   \begin{itemize}

   739   \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}} 

   740   should be deleted, then this file must be deleted.

   741   \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether 

   742   \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted.

   743   \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}.

   744   \end{itemize}\bigskip

   745 

   746   \small

   747   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}

   748   \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}{}},\\

   749   \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}}},\\

   750   \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\

   751   \end{tabular}}\medskip

   752 

   753   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}

   754   \end{frame}}

   755   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   756 

   757 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   758 \mode<presentation>{

   759 \begin{frame}[c]

   760 

   761 How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip

   762 

   763 \begin{center}

   764 \Large \bl{\infer{\Gamma, F\vdash F}{}}

   765 \end{center}

   766 

   767 \end{frame}}

   768 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   769 

   770 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   771 \mode<presentation>{

   772 \begin{frame}[c]

   773 

   774 \begin{center}

   775 \Large 

   776 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}

   777 \end{center}

   778 

   779 \end{frame}}

   780 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   781 

   782 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   783 \mode<presentation>{

   784 \begin{frame}[c]

   785 

   786 \begin{center}

   787 \Large 

   788 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}

   789 \end{center}

   790 

   791 \end{frame}}

   792 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   793 

   794 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   795 \mode<presentation>{

   796 \begin{frame}[c]

   797 

   798 \begin{center}

   799 \Large 

   800 \bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad

   801 \bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\

   802 \end{center}

   803 

   804 \end{frame}}

   805 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   806 

   807 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   808 \mode<presentation>{

   809 \begin{frame}[c]

   810 

   811 \begin{center}

   812 \Large 

   813 \bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}}

   814 \end{center}

   815 

   816 \end{frame}}

   817 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   818 

   819 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   820 \mode<presentation>{

   821 \begin{frame}[t]

   822 

   823 I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause

   824 

   825 \begin{enumerate}

   826 \item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause

   827 \item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove

   828 \begin{center}

   829 \bl{$\Gamma \vdash F_2$}

   830 \end{center}\bigskip\pause

   831 

   832 \item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption

   833 \bl{$F_2$}.\bigskip

   834 \begin{center}

   835 \bl{$F_2, \Gamma \vdash \text{Pred}$}

   836 \end{center}

   837 \end{enumerate}

   838 

   839 \only<4>{

   840 \begin{textblock}{11}(1,10.5)

   841 \bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}}

   842 \end{textblock}}

   843 

   844 

   845 \end{frame}}

   846 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   847 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions

   848 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   849 \mode<presentation>{

   850 \begin{frame}[c]

   851 

   852 \begin{itemize}

   853 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ 

   854 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip

   855 

   856 \begin{center}

   857 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}

   858 \end{center}

   859 

   860 \item \bl{$P$} speaks for \bl{$Q$}\smallskip\\

   861 \bl{$P \mapsto Q \,\dn\, \forall F. (P\,\text{says}\, F) \Rightarrow (Q \,\text{says}\,F)$}\medskip

   862 

   863 \begin{center}

   864 \bl{\infer{\Gamma \vdash Q\,\text{says}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash P\,\text{says}\,F}}

   865 \medskip\\

   866 \bl{\infer{\Gamma \vdash P\,\text{controls}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash Q\,\text{controls}\,F}}\\

   867 

   868 \end{center}

   869 \end{itemize}

   870 

   871 \end{frame}}

   872 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   873 

   874 

   999   

  1000   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1001   \mode<presentation>{

  1002   \begin{frame}[c]

  1003   \frametitle{Controls}

  1004   \small

  1005   

  1006   \begin{itemize}

  1007   \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}}

  1008 

  1009   \item its meaning ``\bl{P} is entitled to do \bl{F}''

  1010   \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause

  1011 

  1012   \begin{center}

  1013   \bl{\mbox{

  1014   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}

  1015         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}

  1016   }}

  1017   \end{center}\pause

  1018 

  1019   \begin{center}

  1020   \bl{\mbox{

  1021   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}

  1022         {\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}}}

  1023   }}

  1024   \end{center}

  1025   \end{itemize}

  1026 

  1027   \end{frame}}

  1028   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1029 %

  1030 

  1031 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1032   \mode<presentation>{

  1033   \begin{frame}[c]

  1034   \frametitle{Security Levels}

  1035   \small

  1036 

  1037   \begin{itemize}

  1038   \item Top secret (\bl{$T\!S$})

  1039   \item Secret (\bl{$S$})

  1040   \item Public (\bl{$P$})

  1041   \end{itemize}

  1042 

  1043   \begin{center}

  1044   \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause

  1045   \end{center}

  1046 

  1047   \begin{itemize}

  1048   \item Bob has a clearance for ``secret''

  1049   \item Bob can read documents that are public or sectret, but not top secret

  1050   \end{itemize}

  1051 

  1052   \end{frame}}

  1053   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1054 %

  1055 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1056   \mode<presentation>{

  1057   \begin{frame}[c]

  1058   \frametitle{Reading a File}

  1059 

  1060   \bl{\begin{center}

  1061   \begin{tabular}{c}

  1062   \begin{tabular}{@ {}l@ {}}

  1063   \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\ 

  1064   \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\

  1065   Bob says Permitted $($File, read$)$\only<2->{\\}

  1066   \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%

  1067   \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%

  1068   \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%

  1069   \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%

  1070   \end{tabular}\\

  1071   \hline

  1072   Permitted $($File, read$)$

  1073   \end{tabular}

  1074   \end{center}}

  1075 

  1076   \end{frame}}

  1077   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1078 %

  1079 

  1080 

  1081 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1082   \mode<presentation>{

  1083   \begin{frame}[c]

  1084   \frametitle{Substitution Rule}

  1085   \small

  1086   

  1087   \bl{\begin{center}

  1088   \begin{tabular}{c}

  1089   $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$

  1090   \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline

  1091   $\Gamma \vdash slev(P) < slev(Q)$

  1092   \end{tabular}

  1093   \end{center}}\bigskip\pause

  1094 

  1095   \begin{itemize}

  1096   \item \bl{$slev($Bob$)$ $=$ $S$}

  1097   \item \bl{$slev($File$)$ $=$ $P$}

  1098   \item \bl{$slev(P) < slev(S)$}

  1099   \end{itemize}

  1100 

  1101   \end{frame}}

  1102   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1103 %

  1104 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1105   \mode<presentation>{

  1106   \begin{frame}[c]

  1107   \frametitle{Reading a File}

  1108 

  1109   \bl{\begin{center}

  1110   \begin{tabular}{c}

  1111   \begin{tabular}{@ {}l@ {}}

  1112   $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\ 

  1113   \hspace{3cm}Bob controls Permitted $($File, read$)$\\

  1114   Bob says Permitted $($File, read$)$\\

  1115   $slev($File$)$ $=$ $P$\\

  1116   $slev($Bob$)$ $=$ $T\!S$\\

  1117   \only<1>{\textcolor{red}{$?$}}%

  1118   \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%

  1119   \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%

  1120   \end{tabular}\\

  1121   \hline

  1122   Permitted $($File, read$)$

  1123   \end{tabular}

  1124   \end{center}}

  1125 

  1126   \end{frame}}

  1127   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1128 %

  1129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1130   \mode<presentation>{

  1131   \begin{frame}[c]

  1132   \frametitle{Transitivity Rule}

  1133   \small

  1134   

  1135   \bl{\begin{center}

  1136   \begin{tabular}{c}

  1137   $\Gamma \vdash l_1 < l_2$ 

  1138   \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline

  1139   $\Gamma \vdash l_1 < l_3$

  1140   \end{tabular}

  1141   \end{center}}\bigskip

  1142 

  1143   \begin{itemize}

  1144   \item \bl{$slev(P) < slev (S)$}

  1145   \item \bl{$slev(S) < slev (T\!S)$}

  1146   \item[] \bl{$slev(P) < slev (T\!S)$}

  1147   \end{itemize}

  1148 

  1149   \end{frame}}

  1150   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1151 %

  1152 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1153   \mode<presentation>{

  1154   \begin{frame}[c]

  1155   \frametitle{Reading Files}

  1156 

  1157   \begin{itemize}

  1158   \item Access policy for reading

  1159   \end{itemize}

  1160 

  1161   \bl{\begin{center}

  1162   \begin{tabular}{c}

  1163   \begin{tabular}{@ {}l@ {}}

  1164   $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\ 

  1165   \hspace{3cm}Bob controls Permitted $(f$, read$)$\\

  1166   Bob says Permitted $($File, read$)$\\

  1167   $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\

  1168   $slev($Bob$)$ $=$ $T\!S$\\

  1169   $slev(P) < slev(S)$\\

  1170   $slev(S) < slev(T\!S)$

  1171   \end{tabular}\\

  1172   \hline

  1173   Permitted $($File, read$)$

  1174   \end{tabular}

  1175   \end{center}}

  1176 

  1177   \end{frame}}

  1178   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1179 %

  1180 

  1181 

  1182 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1183   \mode<presentation>{

  1184   \begin{frame}[c]

  1185   \frametitle{Writing Files}

  1186 

  1187   \begin{itemize}

  1188   \item Access policy for \underline{writing}

  1189   \end{itemize}

  1190 

  1191   \bl{\begin{center}

  1192   \begin{tabular}{c}

  1193   \begin{tabular}{@ {}l@ {}}

  1194   $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\ 

  1195   \hspace{3cm}Bob controls Permitted $(f$, write$)$\\

  1196   Bob says Permitted $($File, write$)$\\

  1197   $slev($File$)$ $=$ $T\!S$\\

  1198   $slev($Bob$)$ $=$ $S$\\

  1199   $slev(P) < slev(S)$\\

  1200   $slev(S) < slev(T\!S)$

  1201   \end{tabular}\\

  1202   \hline

  1203   Permitted $($File, write$)$

  1204   \end{tabular}

  1205   \end{center}}

  1206 

  1207   \end{frame}}

  1208   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1209 %

  1210