305 \begin{frame}[fragile,t]

   306 \frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}

   307 

   308 Bell-LaPadula access model:

   309 

   310  \begin{itemize}

   311   \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if

   312   \bl{$P$}'s security level is at least as high as \bl{$O$}'s.

   313   \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if

   314   \bl{$O$}'s security level is at least as high as \bl{$P$}'s.\medskip

   315 

   316   \item Meta-Rule: All principals in a system should have a sufficiently high security level

   317   in order to access an object.

   318   \end{itemize}\bigskip

   319 

   320 \end{frame}

   321 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

   322 

   323 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   324 \begin{frame}[fragile,t]

   325 \frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}

   326 

   327 Biba (data integrity)

   328 

   329   \begin{itemize}

   330   \item Biba: {\bf `no read down'} - {\bf `no write up'}

   331   \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if

   332   \bl{$P$}'s security level is lower or equal than \bl{$O$}'s.

   333   \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if

   334   \bl{$O$}'s security level is lower or equal than \bl{$P$}'s.

   335   \end{itemize}

   336 

   337 \end{frame}

   338 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

   339 

   340 

   341 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   342 \begin{frame}[fragile,t]

   343 \frametitle{\begin{tabular}{c}4th Lecture:\\ Protocols\end{tabular}}

   344 

   345 A mutual authentication protocol

   346 

   347 \begin{center}

   348 \begin{tabular}{ll}

   349 \bl{$A \rightarrow B$:} & \bl{$N_a$}\\  

   350 \bl{$B \rightarrow A$:} & \bl{$\{N_a, N_b\}_{K_{ab}}$}\\

   351 \bl{$A \rightarrow B$:} & \bl{$N_b$}\\

   352 \end{tabular}

   353 \end{center}

   354 

   355 

   356 \end{frame}

   357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   358 

   359 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   360 \begin{frame}[fragile,t]

   361 \frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}

   362 

   363 

   364 \begin{itemize}

   365 \item formulas

   366 \item judgements

   367 \end{itemize}\pause

   368 

   369 \begin{center}

   370   \begin{tikzpicture}[scale=1]

   371   

   372   \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);

   373   \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};

   374   \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}};

   375   \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}};

   376  

   377   \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); 

   378   \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);

   379   \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); 

   380   

   381   \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};

   382 

   383   \end{tikzpicture}

   384 \end{center}

   385 

   386 

   387 \end{frame}

   388 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   389 

   390 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   391 \begin{frame}[fragile,t]

   392 \frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}

   393 

   394 \begin{center}

   395 \begin{tikzpicture}[scale=1]

   396   

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

   398   \onslide<1->{

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

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

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

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

   403  

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

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

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

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

   408 

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

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

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

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

   413   

   414   \end{tikzpicture}

   415 \end{center}

   416 

   417 

   418 \end{frame}

   419 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   420 

   421 

   422 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   423 \mode<presentation>{

   424 \begin{frame}[c]

   425 \frametitle{\begin{tabular}{c}5th Lecture:\\ Inference Rules\end{tabular}}

   426 

   427 

   428 \begin{center}

   429 \begin{tikzpicture}[scale=1]

   430   

   431   \draw (0.0,0.0) node 

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

   433  

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

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

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

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

   438  

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

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

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

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

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

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

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

   446   \end{tikzpicture}

   447 \end{center}

   448 

   449 

   450 \end{frame}}

   451 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   452 

   453 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%