--- a/slides/slides06.tex Tue Nov 12 02:13:22 2013 +0000
+++ b/slides/slides06.tex Tue Nov 12 08:03:16 2013 +0000
@@ -172,6 +172,105 @@
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Judgements}
+
+\begin{center}
+\begin{tikzpicture}[scale=1]
+
+ \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
+ \onslide<2->{
+ \draw (-1,-0.3) node (X) {};
+ \draw (-2.0,-2.0) node (Y) {};
+ \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y) -- (X);
+
+ \draw (1.2,-0.1) node (X1) {};
+ \draw (2.8,-0.1) node (Y1) {};
+ \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y1) -- (X1);
+
+ \draw (-0.1,0.1) node (X2) {};
+ \draw (0.5,1.5) node (Y2) {};
+ \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y2) -- (X2);}
+
+ \end{tikzpicture}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Inference Rules}
+
+\begin{center}
+\begin{tikzpicture}[scale=1]
+
+ \draw (0.0,0.0) node
+ {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}};
+
+ \draw (-0.1,-0.7) node (X) {};
+ \draw (-0.1,-1.9) node (Y) {};
+ \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y) -- (X);
+
+ \draw (-1,0.6) node (X2) {};
+ \draw (0.0,1.6) node (Y2) {};
+ \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}};
+ \draw[red, ->, line width = 2mm] (Y2) -- (X2);
+ \draw (1,0.6) node (X3) {};
+ \draw (0.0,1.6) node (Y3) {};
+ \draw[red, ->, line width = 2mm] (Y3) -- (X3);
+ \end{tikzpicture}
+\end{center}
+
+\only<2>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}
+\end{textblock}}
+\only<3>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge
+ \underbrace{P \,\text{says}\, G}_{F_2} $}
+\end{textblock}}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Sending Messages}
+
+ \begin{itemize}
+ \item Alice sends a message \bl{$m$}
+ \begin{center}
+ \bl{Alice says $m$}
+ \end{center}\medskip\pause
+
+ \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$})
+ \begin{center}
+ \bl{Alice says $\{m\}_K$}
+ \end{center}\medskip\pause
+
+ \item Decryption of Alice's message\smallskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -195,6 +294,7 @@
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
@@ -214,6 +314,8 @@
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
@@ -239,149 +341,36 @@
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{}
- Recall the following scenario:
-
- \begin{itemize}
- \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}}
- should be deleted, then this file must be deleted.
- \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
- \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted.
- \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}.
- \end{itemize}\bigskip
-
- \small
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
- \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}{}},\\
- \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}}},\\
- \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
- \end{tabular}}\medskip
-
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip
-
-\begin{center}
-\Large \bl{\infer{\Gamma, F\vdash F}{}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
+\frametitle{Proofs}
\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad
-\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\
+\includegraphics[scale=0.4]{pics/river-stones.jpg}
\end{center}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{textblock}{5}(11.7,5)
+goal
+\end{textblock}
+
+\begin{textblock}{5}(11.7,14)
+start
+\end{textblock}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
+\begin{textblock}{5}(0,7)
\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}}
+\bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]
+\bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]
+\bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}
\end{center}
+\end{textblock}
\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[t]
-
-I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause
-
-\begin{enumerate}
-\item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause
-\item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove
-\begin{center}
-\bl{$\Gamma \vdash F_2$}
-\end{center}\bigskip\pause
-
-\item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption
-\bl{$F_2$}.\bigskip
-\begin{center}
-\bl{$F_2, \Gamma \vdash \text{Pred}$}
-\end{center}
-\end{enumerate}
-
-\only<4>{
-\begin{textblock}{11}(1,10.5)
-\bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}}
-\end{textblock}}
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{itemize}
-\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\
-\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
-
-\begin{center}
-\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
-\end{center}
-
-\item \bl{$P$} speaks for \bl{$Q$}\smallskip\\
-\bl{$P \mapsto Q \,\dn\, \forall F. (P\,\text{says}\, F) \Rightarrow (Q \,\text{says}\,F)$}\medskip
-
-\begin{center}
-\bl{\infer{\Gamma \vdash Q\,\text{says}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash P\,\text{says}\,F}}
-\medskip\\
-\bl{\infer{\Gamma \vdash P\,\text{controls}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash Q\,\text{controls}\,F}}\\
-
-\end{center}
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -647,6 +636,242 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Example Proof}
+
+\begin{center}
+\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}
+ {\raisebox{2mm}{\text{\LARGE $?$}}}}
+\end{center}
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Example Proof}
+
+\begin{tabular}{@{\hspace{-6mm}}l}
+\begin{minipage}{1.1\textwidth}
+We have (by axiom)
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(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$}
+\end{tabular}
+\end{center}
+
+From (1) we get
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
+(3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+\end{tabular}
+\end{center}
+
+From (3) and (2) we get
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
+\end{tabular}
+\end{center}
+
+Done.
+\end{minipage}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Other Direction}
+
+\begin{tabular}{@{\hspace{-6mm}}l}
+\begin{minipage}{1.1\textwidth}
+We want to prove
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
+\end{tabular}
+\end{center}
+
+We are better be able to prove:
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
+(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+\end{tabular}
+\end{center}
+
+For (1): If we can prove
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
+\end{tabular}
+\end{center}
+
+then (1) is fine. Similarly for (2).
+\end{minipage}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+
+ Recall the following scenario:
+
+ \begin{itemize}
+ \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}}
+ should be deleted, then this file must be deleted.
+ \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
+ \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted.
+ \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}.
+ \end{itemize}\bigskip
+
+ \small
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
+ \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}{}},\\
+ \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}}},\\
+ \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
+ \end{tabular}}\medskip
+
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip
+
+\begin{center}
+\Large \bl{\infer{\Gamma, F\vdash F}{}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad
+\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+
+I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause
+
+\begin{enumerate}
+\item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause
+\item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove
+\begin{center}
+\bl{$\Gamma \vdash F_2$}
+\end{center}\bigskip\pause
+
+\item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption
+\bl{$F_2$}.\bigskip
+\begin{center}
+\bl{$F_2, \Gamma \vdash \text{Pred}$}
+\end{center}
+\end{enumerate}
+
+\only<4>{
+\begin{textblock}{11}(1,10.5)
+\bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}}
+\end{textblock}}
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{itemize}
+\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\
+\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
+
+\begin{center}
+\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
+\end{center}
+
+\item \bl{$P$} speaks for \bl{$Q$}\smallskip\\
+\bl{$P \mapsto Q \,\dn\, \forall F. (P\,\text{says}\, F) \Rightarrow (Q \,\text{says}\,F)$}\medskip
+
+\begin{center}
+\bl{\infer{\Gamma \vdash Q\,\text{says}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash P\,\text{says}\,F}}
+\medskip\\
+\bl{\infer{\Gamma \vdash P\,\text{controls}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash Q\,\text{controls}\,F}}\\
+
+\end{center}
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -772,6 +997,218 @@
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Controls}
+ \small
+
+ \begin{itemize}
+ \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}}
+
+ \item its meaning ``\bl{P} is entitled to do \bl{F}''
+ \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause
+
+ \begin{center}
+ \bl{\mbox{
+ \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
+ {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
+ }}
+ \end{center}\pause
+
+ \begin{center}
+ \bl{\mbox{
+ \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
+ {\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}}}
+ }}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Security Levels}
+ \small
+
+ \begin{itemize}
+ \item Top secret (\bl{$T\!S$})
+ \item Secret (\bl{$S$})
+ \item Public (\bl{$P$})
+ \end{itemize}
+
+ \begin{center}
+ \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
+ \end{center}
+
+ \begin{itemize}
+ \item Bob has a clearance for ``secret''
+ \item Bob can read documents that are public or sectret, but not top secret
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
+ \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\only<2->{\\}
+ \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
+ \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
+ \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
+ \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Substitution Rule}
+ \small
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
+ \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
+ $\Gamma \vdash slev(P) < slev(Q)$
+ \end{tabular}
+ \end{center}}\bigskip\pause
+
+ \begin{itemize}
+ \item \bl{$slev($Bob$)$ $=$ $S$}
+ \item \bl{$slev($File$)$ $=$ $P$}
+ \item \bl{$slev(P) < slev(S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ $P$\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ \only<1>{\textcolor{red}{$?$}}%
+ \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
+ \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Transitivity Rule}
+ \small
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ $\Gamma \vdash l_1 < l_2$
+ \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
+ $\Gamma \vdash l_1 < l_3$
+ \end{tabular}
+ \end{center}}\bigskip
+
+ \begin{itemize}
+ \item \bl{$slev(P) < slev (S)$}
+ \item \bl{$slev(S) < slev (T\!S)$}
+ \item[] \bl{$slev(P) < slev (T\!S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading Files}
+
+ \begin{itemize}
+ \item Access policy for reading
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Writing Files}
+
+ \begin{itemize}
+ \item Access policy for \underline{writing}
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
+ Bob says Permitted $($File, write$)$\\
+ $slev($File$)$ $=$ $T\!S$\\
+ $slev($Bob$)$ $=$ $S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, write$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]