19 \setmonofont[Scale=MatchLowercase]{Consolas}

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

   251 

   252 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   253 \mode<presentation>{

   254 \begin{frame}[c]

   255 \frametitle{Inference Rules}

   256 

   257 \begin{center}

   258 \bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\

   259 

   260 \bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_1}}

   261 \qquad

   262 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\

   263 

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

   265 

   266 \bl{\infer{\Gamma \vdash P \,\text{says}\, F_2}

   267               {\Gamma \vdash P \,\text{says}\, (F_1\Rightarrow F_2) \quad 

   268                \Gamma \vdash P \,\text{says}\, F_1}}

   269 \end{center}

   270 

   271 \end{frame}}

   272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   273 

   765 

   766 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   767 \mode<presentation>{

   768 \begin{frame}[c]

   769 \frametitle{Program}

   770 

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

   772 

   773 \begin{center}

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

   775 \end{center}

   776 

   777 \end{frame}}

   778 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   779 

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

   781 \mode<presentation>{

   782 \begin{frame}[c]

   783 

   784 \begin{center}

   785 \Large 

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

   787 \end{center}

   788 

   789 \end{frame}}

   790 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   791 

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

   793 \mode<presentation>{

   794 \begin{frame}[c]

   795 

   796 \begin{center}

   797 \Large 

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

   799 \end{center}

   800 

   801 \end{frame}}

   802 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   803 

   804 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   805 \mode<presentation>{

   806 \begin{frame}[c]

   807 

   808 \begin{center}

   809 \Large 

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

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

   812 \end{center}

   813 

   814 \end{frame}}

   815 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   816 

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

   818 \mode<presentation>{

   819 \begin{frame}[c]

   820 

   821 \begin{center}

   822 \Large 

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

   824 \end{center}

   825 

   826 \end{frame}}

   827 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   828 

   829 

   831 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   832 \mode<presentation>{

   833 \begin{frame}[t]

   834 \frametitle{Program: \texttt{prove2}}

   835 

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

   837 

   838 \begin{enumerate}

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

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

   841 \begin{center}

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

   843 \end{center}\bigskip\pause

   844 

   845 \item So I am able to try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption

   846 \bl{$F_2$}.\bigskip

   847 \begin{center}

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

   849 \end{center}

   850 \end{enumerate}

   851 

   852 \only<4>{

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

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

   855 \end{textblock}}

   856 

   857 

   858 \end{frame}}

   859 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%       

  1166 \end{document}

  1167   

  1168  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1169   \mode<presentation>{

  1170   \begin{frame}[c]

  1171   \frametitle{Encryption}

  1172 

  1173   \begin{itemize}

  1174   \item Encryption of a message\smallskip

  1175   \begin{center}

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

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

  1178   \end{center}

  1179   \end{itemize}

  1180 

  1181   \end{frame}}

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

  1183   

  1184    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1185   \mode<presentation>{

  1186   \begin{frame}[c]

  1187   \frametitle{Public/Private Keys}

  1188 

  1189   \begin{itemize}

  1190   \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip

  1191   \begin{center}

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

  1193               {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} & 

  1194                \Gamma \vdash K_{Bob}^{priv}}}}

  1195   \end{center}\bigskip\pause

  1196 

  1197   \item this is {\bf not} a derived rule! 

  1198   \end{itemize}

  1199 

  1200   \end{frame}}

  1201   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

  1202   

  1203   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1204   \mode<presentation>{

  1205   \begin{frame}[c]

  1206   \frametitle{Trusted Third Party}

  1207 

  1208   \begin{itemize}

  1209   \item Alice calls Sam for a key to communicate with Bob

  1210   \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)

  1211   \item Alice sends the message encrypted with the key and the second key it recieved

  1212   \end{itemize}\bigskip

  1213 

  1214   \begin{center}

  1215   \bl{\begin{tabular}{lcl}

  1216   $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\

  1217   $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\

  1218   $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\

  1219   $A$ sends $B$ &:& $\{m\}_{K_{AB}}$

  1220   \end{tabular}}

  1221   \end{center}

  1222 

  1223   \end{frame}}

  1224   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

  1225   

  1226   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1227   \mode<presentation>{

  1228   \begin{frame}[c]

  1229   \frametitle{Controls}

  1230   \small

  1231   

  1232   \begin{itemize}

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

  1234 

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

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

  1237 

  1238   \begin{center}

  1239   \bl{\mbox{

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

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

  1242   }}

  1243   \end{center}\pause

  1244 

  1245   \begin{center}

  1246   \bl{\mbox{

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

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

  1249   }}

  1250   \end{center}

  1251   \end{itemize}

  1252 

  1253   \end{frame}}

  1254   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1255 %

  1256 

  1257 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1258   \mode<presentation>{

  1259   \begin{frame}[c]

  1260   \frametitle{Security Levels}

  1261   \small

  1262 

  1263   \begin{itemize}

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

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

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

  1267   \end{itemize}

  1268 

  1269   \begin{center}

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

  1271   \end{center}

  1272 

  1273   \begin{itemize}

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

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

  1276   \end{itemize}

  1277 

  1278   \end{frame}}

  1279   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1280 %

  1281 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1282   \mode<presentation>{

  1283   \begin{frame}[c]

  1284   \frametitle{Reading a File}

  1285 

  1286   \bl{\begin{center}

  1287   \begin{tabular}{c}

  1288   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1296   \end{tabular}\\

  1297   \hline

  1298   Permitted $($File, read$)$

  1299   \end{tabular}

  1300   \end{center}}

  1301 

  1302   \end{frame}}

  1303   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1304 %

  1305 

  1306 

  1307 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1308   \mode<presentation>{

  1309   \begin{frame}[c]

  1310   \frametitle{Substitution Rule}

  1311   \small

  1312   

  1313   \bl{\begin{center}

  1314   \begin{tabular}{c}

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

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

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

  1318   \end{tabular}

  1319   \end{center}}\bigskip\pause

  1320 

  1321   \begin{itemize}

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

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

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

  1325   \end{itemize}

  1326 

  1327   \end{frame}}

  1328   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1329 %

  1330 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1331   \mode<presentation>{

  1332   \begin{frame}[c]

  1333   \frametitle{Reading a File}

  1334 

  1335   \bl{\begin{center}

  1336   \begin{tabular}{c}

  1337   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

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

  1346   \end{tabular}\\

  1347   \hline

  1348   Permitted $($File, read$)$

  1349   \end{tabular}

  1350   \end{center}}

  1351 

  1352   \end{frame}}

  1353   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1354 %

  1355 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1356   \mode<presentation>{

  1357   \begin{frame}[c]

  1358   \frametitle{Transitivity Rule}

  1359   \small

  1360   

  1361   \bl{\begin{center}

  1362   \begin{tabular}{c}

  1363   $\Gamma \vdash l_1 < l_2$ 

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

  1365   $\Gamma \vdash l_1 < l_3$

  1366   \end{tabular}

  1367   \end{center}}\bigskip

  1368 

  1369   \begin{itemize}

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

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

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

  1373   \end{itemize}

  1374 

  1375   \end{frame}}

  1376   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1377 %

  1378 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1379   \mode<presentation>{

  1380   \begin{frame}[c]

  1381   \frametitle{Reading Files}

  1382 

  1383   \begin{itemize}

  1384   \item Access policy for reading

  1385   \end{itemize}

  1386 

  1387   \bl{\begin{center}

  1388   \begin{tabular}{c}

  1389   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1397   \end{tabular}\\

  1398   \hline

  1399   Permitted $($File, read$)$

  1400   \end{tabular}

  1401   \end{center}}

  1402 

  1403   \end{frame}}

  1404   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1405 %

  1406 

  1407 

  1408 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1409   \mode<presentation>{

  1410   \begin{frame}[c]

  1411   \frametitle{Writing Files}

  1412 

  1413   \begin{itemize}

  1414   \item Access policy for \underline{writing}

  1415   \end{itemize}

  1416 

  1417   \bl{\begin{center}

  1418   \begin{tabular}{c}

  1419   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1427   \end{tabular}\\

  1428   \hline

  1429   Permitted $($File, write$)$

  1430   \end{tabular}

  1431   \end{center}}

  1432 

  1433   \end{frame}}

  1434   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1435 %

  1436 

  1437