1 \documentclass[dvipsnames,14pt,t]{beamer}

     2 \usepackage{proof}

     3 \usepackage{beamerthemeplaincu}

     4 %\usepackage[T1]{fontenc}

     5 %\usepackage[latin1]{inputenc}

     6 \usepackage{mathpartir}

     7 \usepackage{isabelle}

     8 \usepackage{isabellesym}

     9 \usepackage[absolute,overlay]{textpos}

    10 \usepackage{ifthen}

    11 \usepackage{tikz}

    12 \usepackage{courier}

    13 \usepackage{listings}

    14 \usetikzlibrary{arrows}

    15 \usetikzlibrary{positioning}

    16 \usetikzlibrary{calc}

    17 \usetikzlibrary{shapes}

    18 \usepackage{graphicx} 

    19 \setmonofont[Scale=MatchLowercase]{Consolas}

    20 

    21 \isabellestyle{rm}

    22 \renewcommand{\isastyle}{\rm}%

    23 \renewcommand{\isastyleminor}{\rm}%

    24 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}%

    25 \renewcommand{\isatagproof}{}

    26 \renewcommand{\endisatagproof}{}

    27 \renewcommand{\isamarkupcmt}[1]{#1}

    28 

    29 % Isabelle characters

    30 \renewcommand{\isacharunderscore}{\_}

    31 \renewcommand{\isacharbar}{\isamath{\mid}}

    32 \renewcommand{\isasymiota}{}

    33 \renewcommand{\isacharbraceleft}{\{}

    34 \renewcommand{\isacharbraceright}{\}}

    35 \renewcommand{\isacharless}{$\langle$}

    36 \renewcommand{\isachargreater}{$\rangle$}

    37 \renewcommand{\isasymsharp}{\isamath{\#}}

    38 \renewcommand{\isasymdots}{\isamath{...}}

    39 \renewcommand{\isasymbullet}{\act}

    40 \newcommand{\isaliteral}[1]{}

    41 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}

    42 

    43 

    44 

    45 \definecolor{javared}{rgb}{0.6,0,0} % for strings

    46 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments

    47 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords

    48 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc

    49 

    50 \lstset{language=Java,

    51 	basicstyle=\ttfamily,

    52 	keywordstyle=\color{javapurple}\bfseries,

    53 	stringstyle=\color{javagreen},

    54 	commentstyle=\color{javagreen},

    55 	morecomment=[s][\color{javadocblue}]{/**}{*/},

    56 	numbers=left,

    57 	numberstyle=\tiny\color{black},

    58 	stepnumber=1,

    59 	numbersep=10pt,

    60 	tabsize=2,

    61 	showspaces=false,

    62 	showstringspaces=false}

    63 

    64 \lstdefinelanguage{scala}{

    65   morekeywords={abstract,case,catch,class,def,%

    66     do,else,extends,false,final,finally,%

    67     for,if,implicit,import,match,mixin,%

    68     new,null,object,override,package,%

    69     private,protected,requires,return,sealed,%

    70     super,this,throw,trait,true,try,%

    71     type,val,var,while,with,yield},

    72   otherkeywords={=>,<-,<\%,<:,>:,\#,@},

    73   sensitive=true,

    74   morecomment=[l]{//},

    75   morecomment=[n]{/*}{*/},

    76   morestring=[b]",

    77   morestring=[b]',

    78   morestring=[b]"""

    79 }

    80 

    81 \lstset{language=Scala,

    82 	basicstyle=\ttfamily,

    83 	keywordstyle=\color{javapurple}\bfseries,

    84 	stringstyle=\color{javagreen},

    85 	commentstyle=\color{javagreen},

    86 	morecomment=[s][\color{javadocblue}]{/**}{*/},

    87 	numbers=left,

    88 	numberstyle=\tiny\color{black},

    89 	stepnumber=1,

    90 	numbersep=10pt,

    91 	tabsize=2,

    92 	showspaces=false,

    93 	showstringspaces=false}

    94 

    95 %sudoku

    96 \newcounter{row}

    97 \newcounter{col}

    98 

    99 \newcommand\setrow[9]{

   100         \setcounter{col}{1}

   101         \foreach \n in {#1, #2, #3, #4, #5, #6, #7, #8, #9} {

   102             \edef\x{\value{col} - 0.5}

   103             \edef\y{9.5 - \value{row}}

   104             \node[anchor=center] at (\x, \y) {\n};

   105             \stepcounter{col}

   106         }

   107         \stepcounter{row}

   108 }

   109 

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

   111 

   112 % beamer stuff 

   113 \renewcommand{\slidecaption}{APP 06, King's College London, 12 November 2013}

   114 

   115 \newcommand{\bl}[1]{\textcolor{blue}{#1}}

   116 \begin{document}

   117 

   118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   119 \mode<presentation>{

   120 \begin{frame}<1>[t]

   121 \frametitle{%

   122   \begin{tabular}{@ {}c@ {}}

   123   \\

   124   \LARGE Access Control and \\[-3mm] 

   125   \LARGE Privacy Policies (6)\\[-6mm] 

   126   \end{tabular}}\bigskip\bigskip\bigskip

   127 

   128   %\begin{center}

   129   %\includegraphics[scale=1.3]{pics/barrier.jpg}

   130   %\end{center}

   131 

   132 \normalsize

   133   \begin{center}

   134   \begin{tabular}{ll}

   135   Email:  & christian.urban at kcl.ac.uk\\

   136   Office: & N7.07 (North Wing, Bush House)\\

   137   Slides: & KEATS (also homework is there)\\

   138   \end{tabular}

   139   \end{center}

   140 

   141 

   142 \end{frame}}

   143  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   144 

   145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   146   \mode<presentation>{

   147   \begin{frame}[t]

   148   \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}

   149   

   150   Formulas

   151   

   152   \begin{itemize}

   153   \item[]

   154   

   155   \begin{center}\color{blue}

   156   \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}

   157   \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\

   158             & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\

   159             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\

   160             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\

   161             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\

   162             & \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}}} \\  

   163             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\ 

   164   \end{tabular}

   165   \end{center}

   166   

   167   \end{itemize}

   168   

   169 Judgements

   170 

   171 \begin{itemize}

   172 \item[] \mbox{\hspace{9mm}}\bl{$\Gamma \vdash \text{F}$}

   173 \end{itemize}

   174   

   175   \end{frame}}

   176   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   177   

   178 

   179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   180 \mode<presentation>{

   181 \begin{frame}[c]

   182 \frametitle{Judgements}

   183 

   184 \begin{center}

   185 \begin{tikzpicture}[scale=1]

   186   

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

   188   \onslide<2->{

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

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

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

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

   193  

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

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

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

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

   198 

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

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

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

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

   203   

   204   \end{tikzpicture}

   205 \end{center}

   206 

   207 \end{frame}}

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

   209   

   210 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   211 \mode<presentation>{

   212 \begin{frame}[c]

   213 \frametitle{Inference Rules}

   214 

   215 \begin{center}

   216 \begin{tikzpicture}[scale=1]

   217   

   218   \draw (0.0,0.0) node 

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

   220  

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

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

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

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

   225  

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

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

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

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

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

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

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

   233   \end{tikzpicture}

   234 \end{center}

   235 

   236 \only<2>{

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

   238 \small

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

   240 \end{textblock}}

   241 \only<3>{

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

   243 \small

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

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

   246 \end{textblock}}

   247 

   248 \end{frame}}

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

   250 

   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 

   274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   275   \mode<presentation>{

   276   \begin{frame}[c]

   277   \frametitle{Sending Messages}

   278 

   279   \begin{itemize}

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

   281   \begin{center}

   282   \bl{Alice says $m$}

   283   \end{center}\medskip\pause

   284 

   285   \item Alice sends an encrypted message \bl{$m$} with key \bl{$K$} 

   286   (\bl{$\{m\}_K \dn K \Rightarrow m$})

   287   \begin{center}

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

   289   \end{center}\medskip\pause

   290 

   291   \item Decryption of Alice's message\smallskip

   292   \begin{center}

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

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

   295   \end{center}

   296   \end{itemize}

   297 

   298   \end{frame}}

   299   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   300 

   301 

   302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   303 \mode<presentation>{

   304 \begin{frame}[c]

   305 \frametitle{Proofs}

   306 

   307 \begin{center}

   308 \bl{

   309 \infer{\Gamma \vdash F}

   310          {\infer{\hspace{1cm}:\hspace{1cm}}

   311              {\infer{\hspace{1cm}:\hspace{1cm}}{:}

   312                &

   313               \infer{\hspace{1cm}:\hspace{1cm}}{:\quad :}

   314            }}

   315 }

   316 \end{center}

   317 

   318 \end{frame}}

   319 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   320 

   321 

   322 

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

   324 \mode<presentation>{

   325 \begin{frame}[c]

   326 \frametitle{The Access Control Problem}

   327 

   328 

   329 \begin{center}

   330   \begin{tikzpicture}[scale=1]

   331   

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

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

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

   335   \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\end{tabular}};

   336  

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

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

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

   340   

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

   342 

   343   \end{tikzpicture}

   344 \end{center}

   345 

   346 \end{frame}}

   347 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   348 

   349 

   350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   351 \mode<presentation>{

   352 \begin{frame}[c]

   353 \frametitle{Proofs}

   354 

   355 \begin{center}

   356 \includegraphics[scale=0.4]{pics/river-stones.jpg}

   357 \end{center}

   358 

   359 \begin{textblock}{5}(11.7,5)

   360 goal

   361 \end{textblock}

   362 

   363 \begin{textblock}{5}(11.7,14)

   364 start

   365 \end{textblock}

   366 

   367 \begin{textblock}{5}(0,7)

   368 \begin{center}

   369 \bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]

   370 \bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]

   371 \bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}

   372 \end{center}

   373 \end{textblock}

   374 

   375 \end{frame}}

   376 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   377 

   378 

   379 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   380 \mode<presentation>{

   381 \begin{frame}[c]

   382 \frametitle{Sudoku}

   383 

   384 \begin{tikzpicture}[scale=.5]

   385   \begin{scope}

   386     \draw (0, 0) grid (9, 9);

   387     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   388 

   389     \setcounter{row}{1}

   390     \setrow { }{2}{ }  {5}{ }{1}  { }{9}{ }

   391     \setrow {8}{ }{ }  {2}{ }{3}  { }{ }{6}

   392     \setrow { }{3}{ }  { }{6}{ }  { }{7}{ }

   393 

   394     \setrow { }{ }{1}  { }{ }{ }  {6}{ }{ }

   395     \setrow {5}{4}{ }  { }{ }{ }  { }{1}{9}

   396     \setrow { }{ }{2}  { }{ }{ }  {7}{ }{ }

   397 

   398     \setrow { }{9}{ }  { }{3}{ }  { }{8}{ }

   399     \setrow {2}{ }{ }  {8}{ }{4}  { }{ }{7}

   400     \setrow { }{1}{ }  {9}{ }{7}  { }{6}{ }

   401 

   402     \fill[red, fill opacity=0.4] (4,0) rectangle (5,9);

   403     \fill[red, fill opacity=0.4] (0,5) rectangle (9,6);

   404     \fill[red!50, fill opacity=0.4] (3,3) rectangle (4,5);

   405     \fill[red!50, fill opacity=0.4] (5,3) rectangle (6,5);  

   406     \node[gray, anchor=center] at (4.5, -0.5) {columns};

   407     \node[gray, rotate=90, anchor=center] at (-0.6, 4.5, -0.5) {rows};

   408     \node[gray, anchor=center] at (4.5, 4.5) {box};

   409   \end{scope}

   410   \end{tikzpicture}

   411 

   412 \small

   413 \begin{textblock}{7}(9,3)

   414 \begin{enumerate}

   415 \item {\bf Row-Column:} each cell, must contain exactly one number

   416 \item {\bf Row-Number:} each row must contain each number exactly once

   417 \item {\bf Column-Number:} each column must contain each number exactly once

   418 \item {\bf Box-Number:} each box must contain each number exactly once

   419 \end{enumerate}

   420 \end{textblock}

   421 

   422 

   423 \end{frame}}

   424 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   425 

   426 

   427 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   428 \mode<presentation>{

   429 \begin{frame}[c]

   430 \frametitle{Solving Sudokus}

   431 

   432 \begin{tikzpicture}[scale=.5]

   433   \begin{scope}

   434     \draw (0, 0) grid (9, 9);

   435     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   436 

   437     \setcounter{row}{1}

   438     \setrow { }{ }{ }  {7}{ }{ }  { }{5}{8}

   439     \setrow {}{5}{6}  {2}{1}{8}  {7}{9}{3}

   440     \setrow { }{ }{ }  { }{ }{ }  {1}{ }{ }

   441 

   442     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   443     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   444     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }

   445 

   446     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   447     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   448     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   449 

   450     \fill[red, fill opacity=0.4] (0,7) rectangle (1,8);

   451 

   452   \end{scope}

   453   \end{tikzpicture}

   454 

   455 \small

   456 \begin{textblock}{6}(9,6)

   457 {\bf single position rules}\\

   458 \begin{center}

   459 \bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}

   460 \end{center}

   461 

   462 \onslide<2->{

   463 \begin{center}

   464 \bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one column}}}\medskip\\

   465 \bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one box}}}

   466 \end{center}}

   467 \end{textblock}

   468 

   469 

   470 \end{frame}}

   471 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   472 

   473 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   474 \mode<presentation>{

   475 \begin{frame}[c]

   476 \frametitle{Solving Sudokus}

   477 

   478 \begin{tikzpicture}[scale=.5]

   479   \begin{scope}

   480     \draw (0, 0) grid (9, 9);

   481     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   482 

   483     \setcounter{row}{1}

   484     \setrow { }{ }{ }  {7}{ }{ }  {\alert{\footnotesize 2}}{5}{8}

   485     \setrow {}{5}{6}  {2}{1}{8}  {7}{9}{3}

   486     \setrow { }{ }{ }  { }{ }{ }  {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}}

   487 

   488     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   489     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   490     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }

   491 

   492     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   493     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   494     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   495 

   496   \end{scope}

   497   \end{tikzpicture}

   498 

   499 \small

   500 \begin{textblock}{6}(7.5,6)

   501 {\bf candidate rules}\\

   502 \begin{center}

   503 \bl{\infer{x\;\text{candidate in empty positions}}{X - \{x\}\;\text{in one box} & X \subseteq \{1..9\}}}

   504 \end{center}

   505 \end{textblock}

   506 

   507 \end{frame}}

   508 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   509 

   510 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   511 \mode<presentation>{

   512 \begin{frame}[c]

   513 \frametitle{Solving Sudokus}

   514 

   515 \begin{tikzpicture}[scale=.5]

   516   \begin{scope}

   517     \draw (0, 0) grid (9, 9);

   518     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   519 

   520     \setcounter{row}{1}

   521     \setrow { }{ }{ }  {7}{ }{ }  {\alert{\footnotesize 2}}{5}{8}

   522     \setrow {\alert{4}}{5}{6}  {2}{1}{8}  {7}{9}{3}

   523     \setrow { }{ }{ }  { }{ }{ }  {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}}

   524 

   525     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   526     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   527     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }

   528 

   529     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   530     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   531     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   532 

   533   \end{scope}

   534   \end{tikzpicture}

   535 

   536 \small

   537 \begin{textblock}{6}(7.5,6)

   538 \begin{center}

   539 \bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}\bigskip\\

   540 \bl{\infer{2\;\text{candidate in empty positions}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}}

   541 \end{center}

   542 \end{textblock}

   543 

   544 

   545 \begin{textblock}{3}(13.5,6.8)

   546   \begin{tikzpicture}

   547   \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}

   548   \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}

   549   \end{tikzpicture}

   550 \end{textblock}

   551 

   552 \begin{textblock}{3}(14.5,9.3)

   553   \begin{tikzpicture}

   554   \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}

   555   \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}

   556   \end{tikzpicture}

   557 \end{textblock}

   558 

   559 \end{frame}}

   560 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   561 

   562 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   563 \mode<presentation>{

   564 \begin{frame}[c]

   565 \frametitle{Solving Sudokus}

   566 

   567 \begin{tikzpicture}[scale=.5]

   568   \begin{scope}

   569     \draw (0, 0) grid (9, 9);

   570     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   571 

   572     \setcounter{row}{1}

   573     \setrow { }{ }{ }  {7}{ }{ }  { }{5}{8}

   574     \setrow { }{5}{6}  {2}{1}{8}  {7}{9}{3}

   575     \setrow { }{ }{ }  { }{ }{ }  {1}{ }{ }

   576 

   577     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   578     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   579     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ \alert{2}}

   580 

   581     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   582     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   583     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   584 

   585   \end{scope}

   586   \end{tikzpicture}

   587 

   588 \small

   589 \begin{textblock}{6}(7.5,6)

   590 \begin{center}

   591 \bl{\infer{2\;\text{candidate}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}}

   592 \end{center}

   593 \end{textblock}

   594 

   595 \begin{textblock}{3}(14.5,8.3)

   596   \begin{tikzpicture}

   597   \onslide<1>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}

   598   \end{tikzpicture}

   599 \end{textblock}

   600 

   601 \end{frame}}

   602 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   603 

   604 

   605 

   606 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   607 \mode<presentation>{

   608 \begin{frame}[c]

   609 \frametitle{BTW}

   610 

   611 Are there sudokus that cannot be solved?\pause

   612 

   613 \begin{center}

   614 \begin{tikzpicture}[scale=.5]

   615   \begin{scope}

   616     \draw (0, 0) grid (9, 9);

   617     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   618 

   619     \setcounter{row}{1}

   620     \setrow {1}{2}{3}  {4}{5}{6}  {7}{8}{ }

   621     \setrow { }{ }{ }  { }{ }{ }  { }{ }{2}

   622     \setrow { }{ }{ }  { }{ }{ }  { }{ }{3}

   623 

   624     \setrow { }{ }{ }  { }{ }{ }  { }{ }{4}

   625     \setrow { }{ }{ }  { }{ }{ }  { }{ }{5}

   626     \setrow { }{ }{ }  { }{ }{ }  { }{ }{6}

   627 

   628     \setrow { }{ }{ }  { }{ }{ }  { }{ }{7}

   629     \setrow { }{ }{ }  { }{ }{ }  { }{ }{8}

   630     \setrow { }{ }{ }  { }{ }{ }  { }{ }{9}

   631 

   632   \end{scope}

   633   \end{tikzpicture}

   634 \end{center}

   635 

   636 Sometimes no rules apply at all....unsolvable sudoku.

   637 

   638 

   639 \end{frame}}

   640 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   641 

   642 

   643 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   644 \mode<presentation>{

   645 \begin{frame}[c]

   646 \frametitle{Example Proof}

   647 

   648 \begin{center}

   649 \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}

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

   651 \end{center}

   652 

   653 

   654 \end{frame}}

   655 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   656 

   657 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   658 \mode<presentation>{

   659 \begin{frame}[c]

   660 \frametitle{Example Proof}

   661 

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

   663 \begin{minipage}{1.1\textwidth}

   664 We have (by axiom)

   665 

   666 \begin{center}

   667 \begin{tabular}{@{}ll@{}}

   668 (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$}

   669 \end{tabular}

   670 \end{center}

   671 

   672 From (1) we get

   673 

   674 \begin{center}

   675 \begin{tabular}{@{}ll@{}}

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

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

   678 \end{tabular}

   679 \end{center}

   680 

   681 From (3) and (2) we get

   682 

   683 \begin{center}

   684 \begin{tabular}{@{}ll@{}}

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

   686 \end{tabular}

   687 \end{center}

   688 

   689 Done.

   690 \end{minipage}

   691 \end{tabular}

   692 

   693 \end{frame}}

   694 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   695 

   696 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   697 \mode<presentation>{

   698 \begin{frame}[c]

   699 \frametitle{Other Direction}

   700 

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

   702 \begin{minipage}{1.1\textwidth}

   703 We want to prove

   704 

   705 \begin{center}

   706 \begin{tabular}{@{}ll@{}}

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

   708 \end{tabular}

   709 \end{center}

   710 

   711 We better be able to prove:

   712 

   713 \begin{center}

   714 \begin{tabular}{@{}ll@{}}

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

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

   717 \end{tabular}

   718 \end{center}

   719 

   720 For (1): If we can prove

   721 

   722 \begin{center}

   723 \begin{tabular}{@{}ll@{}}

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

   725 \end{tabular}

   726 \end{center}

   727 

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

   729 \end{minipage}

   730 \end{tabular}

   731 

   732 \end{frame}}

   733 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

   734      

   735 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   736 \mode<presentation>{

   737 \begin{frame}[t]

   738 

   739 I want to prove

   740 

   741 \begin{center}

   742 \bl{$\Gamma \vdash \text{del\_file}$}

   743 \end{center}\pause

   744 

   745 There is an inference rule

   746 

   747 \begin{center}

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

   749 \end{center}\pause

   750 

   751 So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause

   752 

   753 \bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\

   754 So I can use the rule

   755 

   756 \begin{center}

   757 \bl{\infer{\Gamma, F \vdash F}{}}

   758 \end{center}

   759 

   760 \onslide<5>{\bf\alert{What is wrong with this?}}

   761 \hfill{\bf Done. Qed.}

   762 

   763 \end{frame}}

   764 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%        

   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 

   830      

   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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%       

   860      

   861 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   862   \mode<presentation>{

   863   \begin{frame}[c]

   864   \frametitle{}

   865 

   866   Recall the following scenario:

   867 

   868   \begin{itemize}

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

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

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

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

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

   874   \end{itemize}\bigskip

   875 

   876   \small

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

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

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

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

   881   \end{tabular}}\medskip

   882 

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

   884   \end{frame}}

   885   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   886 

   887 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   888 \mode<presentation>{

   889 \begin{frame}[c]

   890 

   891 \begin{itemize}

   892 \item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or

   893 can make a statement \bl{$F$}\bigskip

   894 

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

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

   897 

   898 \begin{center}

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

   900 \end{center}

   901 

   902 

   903 \end{itemize}

   904 

   905 \end{frame}}

   906 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   907 

   908 

   909 

   910 

   911 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   912 \mode<presentation>{

   913 \begin{frame}[c]

   914 \frametitle{Trusted Third Party}

   915 

   916 Simple protocol for establishing a secure connection via a mutually

   917 trusted 3rd party (server):

   918 

   919 \begin{center}

   920 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}

   921 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\

   922 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\

   923 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\

   924 Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\

   925 \end{tabular}

   926 \end{center}

   927 

   928 \end{frame}}

   929 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   930 

   931    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   932   \mode<presentation>{

   933   \begin{frame}[c]

   934   \frametitle{Sending Rule}

   935 

   936   \bl{\begin{center}

   937   \mbox{\infer{\Gamma \vdash Q \;\text{says}\; F}

   938               {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}}

   939   \end{center}}\bigskip\pause

   940   

   941   \bl{$P \,\text{sends}\, Q : F \dn$}\\

   942   \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}

   943 

   944   \end{frame}}

   945   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   946   

   947     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   948   \mode<presentation>{

   949   \begin{frame}[c]

   950   \frametitle{Trusted Third Party}

   951 

   952   \begin{center}

   953   \bl{\begin{tabular}{l}

   954   $A$ sends $S$ : $\text{Connect}(A,B)$\\  

   955   \bl{$S \,\text{says}\, (\text{Connect}(A,B) \Rightarrow$}\\ 

   956   \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge 

   957   \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\

   958  $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\

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

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

   961   \end{tabular}}

   962   \end{center}\bigskip\pause

   963   

   964   

   965   \bl{$\Gamma \vdash B \,\text{says} \, m$}?

   966   \end{frame}}

   967   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

   968 

   969    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   970   \mode<presentation>{

   971   \begin{frame}[c]

   972   \frametitle{Public/Private Keys}

   973 

   974   \begin{itemize}

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

   976   \begin{center}

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

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

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

   980   \end{center}\bigskip\pause

   981 

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

   983   \end{itemize}

   984 

   985   \end{frame}}

   986   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

   987   

   988 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   989   \mode<presentation>{

   990   \begin{frame}[c]

   991   \frametitle{Security Levels}

   992   \small

   993 

   994   \begin{itemize}

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

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

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

   998   \end{itemize}

   999 

  1000   \begin{center}

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

  1002   \end{center}

  1003 

  1004   \begin{itemize}

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

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

  1007   \end{itemize}

  1008 

  1009   \end{frame}}

  1010   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1011 %

  1012 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1013   \mode<presentation>{

  1014   \begin{frame}[c]

  1015   \frametitle{Reading a File}

  1016 

  1017   \bl{\begin{center}

  1018   \begin{tabular}{c}

  1019   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1027   \end{tabular}\\

  1028   \hline

  1029   Permitted $($File, read$)$

  1030   \end{tabular}

  1031   \end{center}}

  1032 

  1033   \end{frame}}

  1034   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1035 %

  1036 

  1037 

  1038 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1039   \mode<presentation>{

  1040   \begin{frame}[c]

  1041   \frametitle{Substitution Rule}

  1042   \small

  1043   

  1044   \bl{\begin{center}

  1045   \begin{tabular}{c}

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

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

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

  1049   \end{tabular}

  1050   \end{center}}\bigskip\pause

  1051 

  1052   \begin{itemize}

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

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

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

  1056   \end{itemize}

  1057 

  1058   \end{frame}}

  1059   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1060 %

  1061 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1062   \mode<presentation>{

  1063   \begin{frame}[c]

  1064   \frametitle{Reading a File}

  1065 

  1066   \bl{\begin{center}

  1067   \begin{tabular}{c}

  1068   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

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

  1077   \end{tabular}\\

  1078   \hline

  1079   Permitted $($File, read$)$

  1080   \end{tabular}

  1081   \end{center}}

  1082 

  1083   \end{frame}}

  1084   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1085 %

  1086 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1087   \mode<presentation>{

  1088   \begin{frame}[c]

  1089   \frametitle{Transitivity Rule}

  1090   \small

  1091   

  1092   \bl{\begin{center}

  1093   \begin{tabular}{c}

  1094   $\Gamma \vdash l_1 < l_2$ 

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

  1096   $\Gamma \vdash l_1 < l_3$

  1097   \end{tabular}

  1098   \end{center}}\bigskip

  1099 

  1100   \begin{itemize}

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

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

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

  1104   \end{itemize}

  1105 

  1106   \end{frame}}

  1107   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1108 %

  1109 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1110   \mode<presentation>{

  1111   \begin{frame}[c]

  1112   \frametitle{Reading Files}

  1113 

  1114   \begin{itemize}

  1115   \item Access policy for reading

  1116   \end{itemize}

  1117 

  1118   \bl{\begin{center}

  1119   \begin{tabular}{c}

  1120   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1128   \end{tabular}\\

  1129   \hline

  1130   Permitted $($File, read$)$

  1131   \end{tabular}

  1132   \end{center}}

  1133 

  1134   \end{frame}}

  1135   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%