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

     2 \usepackage{proof}

     3 \usepackage{beamerthemeplainculight}

     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 \usepackage{graphicx} 

    18 

    19 \isabellestyle{rm}

    20 \renewcommand{\isastyle}{\rm}%

    21 \renewcommand{\isastyleminor}{\rm}%

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

    23 \renewcommand{\isatagproof}{}

    24 \renewcommand{\endisatagproof}{}

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

    26 

    27 % Isabelle characters

    28 \renewcommand{\isacharunderscore}{\_}

    29 \renewcommand{\isacharbar}{\isamath{\mid}}

    30 \renewcommand{\isasymiota}{}

    31 \renewcommand{\isacharbraceleft}{\{}

    32 \renewcommand{\isacharbraceright}{\}}

    33 \renewcommand{\isacharless}{$\langle$}

    34 \renewcommand{\isachargreater}{$\rangle$}

    35 \renewcommand{\isasymsharp}{\isamath{\#}}

    36 \renewcommand{\isasymdots}{\isamath{...}}

    37 \renewcommand{\isasymbullet}{\act}

    38 

    39 

    40 

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

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

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

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

    45 

    46 \lstset{language=Java,

    47 	basicstyle=\ttfamily,

    48 	keywordstyle=\color{javapurple}\bfseries,

    49 	stringstyle=\color{javagreen},

    50 	commentstyle=\color{javagreen},

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

    52 	numbers=left,

    53 	numberstyle=\tiny\color{black},

    54 	stepnumber=1,

    55 	numbersep=10pt,

    56 	tabsize=2,

    57 	showspaces=false,

    58 	showstringspaces=false}

    59 

    60 \lstdefinelanguage{scala}{

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

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

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

    64     new,null,object,override,package,%

    65     private,protected,requires,return,sealed,%

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

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

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

    69   sensitive=true,

    70   morecomment=[l]{//},

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

    72   morestring=[b]",

    73   morestring=[b]',

    74   morestring=[b]"""

    75 }

    76 

    77 \lstset{language=Scala,

    78 	basicstyle=\ttfamily,

    79 	keywordstyle=\color{javapurple}\bfseries,

    80 	stringstyle=\color{javagreen},

    81 	commentstyle=\color{javagreen},

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

    83 	numbers=left,

    84 	numberstyle=\tiny\color{black},

    85 	stepnumber=1,

    86 	numbersep=10pt,

    87 	tabsize=2,

    88 	showspaces=false,

    89 	showstringspaces=false}

    90 

    91 % beamer stuff 

    92 \renewcommand{\slidecaption}{APP 05, King's College London, 23 October 2012}

    93 

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

    95 \begin{document}

    96 

    97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    98 \mode<presentation>{

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

   100 \frametitle{%

   101   \begin{tabular}{@ {}c@ {}}

   102   \\

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

   104   \LARGE Privacy Policies (5)\\[-6mm] 

   105   \end{tabular}}\bigskip\bigskip\bigskip

   106 

   107   %\begin{center}

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

   109   %\end{center}

   110 

   111 \normalsize

   112   \begin{center}

   113   \begin{tabular}{ll}

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

   115   Of$\!$fice: & S1.27 (1st floor Strand Building)\\

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

   117   \end{tabular}

   118   \end{center}

   119 

   120 

   121 \end{frame}}

   122  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   123 

   124 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   125 \mode<presentation>{

   126 \begin{frame}[c]

   127 \frametitle{Satan's Computer}

   128 

   129 Ross Anderson and Roger Needham wrote:\bigskip

   130 

   131 \begin{quote}

   132 In effect, our task is to program a computer which gives 

   133 answers which are subtly and maliciously wrong at the most 

   134 inconvenient possible moment\ldots{} we hope that the lessons 

   135 learned from programming Satan's computer may be helpful 

   136 in tackling the more common problem of programming Murphy's.

   137 \end{quote}

   138 

   139 

   140 \end{frame}}

   141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   142 

   143 

   144 

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

   146 \mode<presentation>{

   147 \begin{frame}[c]

   148 \frametitle{Protocol Specifications}

   149 

   150 The Needham-Schroeder Protocol:

   151 

   152 \begin{center}

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

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

   155 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\

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

   157 Message 4 & \bl{$B \rightarrow A :$} & \bl{$\{N_B\}_{K_{AB}}$}\\

   158 Message 5 & \bl{$A \rightarrow B :$} & \bl{$\{N_B-1\}_{K_{AB}}$}\\

   159 \end{tabular}

   160 \end{center}

   161 

   162 \end{frame}}

   163 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   164 

   165 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   166 \mode<presentation>{

   167 \begin{frame}[c]

   168 \frametitle{Cryptographic Protocol Failures}

   169 

   170 Again Ross Anderson and Roger Needham wrote:\bigskip

   171 

   172 \begin{quote}

   173 \textcolor{gray}{

   174 A lot of the recorded frauds were the result of this kind of blunder, or from 

   175 management negligence pure and simple.} However, there have been a 

   176 significant number of cases where the designers protected the right things, 

   177 used cryptographic algorithms which were not broken, and yet found that their 

   178 systems were still successfully attacked. 

   179 \end{quote}

   180 

   181 

   182 \end{frame}}

   183 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   184 

   185 

   186 

   187 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   188 \mode<presentation>{

   189 \begin{frame}[c]

   190 \frametitle{The Access Control Problem}

   191 

   192 

   193 \begin{center}

   194   \begin{tikzpicture}[scale=1]

   195   

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

   197   \draw (-2.7,1) node {\begin{tabular}{l}access\\request\end{tabular}};

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

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

   200  

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

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

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

   204   

   205   \draw (0.6,4) node {\begin{tabular}{l}\large some rules\\(access policy)\end{tabular}};

   206 

   207   \end{tikzpicture}

   208 \end{center}

   209 

   210 \end{frame}}

   211 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   212 

   213 

   214 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   215 \mode<presentation>{

   216 \begin{frame}[c]

   217 \frametitle{Access Control Logic}

   218 

   219 Ross Anderson about the use of Logic:\bigskip

   220 

   221 \begin{quote}

   222 Formal methods can be an excellent way of finding 

   223 bugs in security protocol designs as they force the designer 

   224 to make everything explicit and thus confront dif$\!$ficult design 

   225 choices that might otherwise be fudged. 

   226 \end{quote}

   227 

   228 \end{frame}}

   229 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   230 

   231 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   232 \mode<presentation>{

   233 \begin{frame}[c]

   234 

   235 \begin{center}

   236   \begin{tikzpicture}[scale=1]

   237   

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

   239   \draw (-2.7,1) node {\begin{tabular}{l}access\\request\end{tabular}};

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

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

   242  

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

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

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

   246   

   247   \draw (0.6,3.7) node {\begin{tabular}{l}access policy\end{tabular}};

   248 

   249   \end{tikzpicture}

   250 \end{center}

   251 

   252 Assuming one file on my computer contains a virus.\smallskip\\

   253 \only<1>{Q: Given my access policy, can this file ``infect'' my whole computer?}%

   254 \only<2>{Q: Can my access policy prevent that my whole computer gets infected.}

   255 

   256 

   257 \end{frame}}

   258 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   259 

   260  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   261   \mode<presentation>{

   262   \begin{frame}[c]

   263   \small

   264   \begin{center}

   265   \mbox{

   266   \inferrule{\mbox{\begin{tabular}{l}

   267          \ldots\\

   268          is\_at\_library (Christian)\\ 

   269          is\_student (a) $\wedge$ is\_at\_library (a) $\Rightarrow$ may\_obtain\_email (a)\\

   270          is\_staff (a) $\wedge$ is\_at\_library (a) $\Rightarrow$ may\_obtain\_email (a)\medskip\\

   271          \onslide<2->{HoD says is\_staff (a) $\Rightarrow$ is\_staff (a)}\\

   272          \onslide<2->{HoD says is\_staff (Christian)}\medskip\\

   273          \onslide<3->{may\_obtain\_email (a) $\wedge$ sending\_spam (a) $\Rightarrow$\\}

   274          \onslide<3->{\hspace{6cm}$\neg$ may\_obtain\_email (a)}

   275        \end{tabular}

   276         }}

   277         {\mbox{? may\_obtain\_email (Christian)}}}

   278   \end{center}

   279   \end{frame}}

   280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   281 

   282   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   283   \mode<presentation>{

   284   \begin{frame}[c]

   285   \frametitle{}

   286 

   287   There are two ways for tackling such problems:\medskip

   288 

   289   \begin{itemize}

   290   \item either you make up our own language in which you can describe

   291   the problem,\medskip

   292 

   293   \item or you use an existing language and represent the problem in

   294   this language.

   295   \end{itemize}

   296   

   297   \end{frame}}

   298   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   299 

   300 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   301   \mode<presentation>{

   302   \begin{frame}[t]

   303   \frametitle{\Large\begin{tabular}{@ {}c@ {}}Logic(s)\end{tabular}}

   304 

   305   \begin{itemize}

   306   \item Formulas

   307 

   308   \begin{center}\color{blue}

   309   \begin{tabular}{rcl@ {\hspace{10mm}}l}

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

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

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

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

   314             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}       & \textcolor{black}{implies}\\

   315             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F}       & \textcolor{black}{negation}\\

   316             & \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}}} & \textcolor{black}{predicates}\\

   317    & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}} & 

   318         \onslide<2->{\textcolor{black}{forall quantification}}\\

   319    & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ F}} & 

   320         \onslide<2->{\textcolor{black}{exists quantification}}\\[-7mm]

   321   \end{tabular}

   322   \end{center}

   323 

   324   \end{itemize}

   325 

   326   \begin{textblock}{12}(1,14)

   327   Terms \textcolor{blue}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{7C}{\isacharbar}}\ c\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}}

   328   \end{textblock}

   329   

   330   \end{frame}}

   331   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   332 %

   333 

   334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   335   \mode<presentation>{

   336   \begin{frame}[c]

   337 

   338 {\lstset{language=Scala}\fontsize{10}{12}\selectfont

   339 \texttt{\lstinputlisting{programs/formulas.scala}}}

   340 

   341   \end{frame}}

   342   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   343 

   344 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   345   \mode<presentation>{

   346   \begin{frame}[t]

   347   \frametitle{Judgements}

   348 

   349   \begin{center}

   350   \LARGE

   351   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}

   352   \end{center}

   353 

   354   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} is a collection of formulas, called the \alert{assumptions}\bigskip\pause

   355 

   356   \begin{itemize}

   357   \item Example\mbox{}\\[-8mm]

   358 

   359   \only<2>{\begin{center}\tiny

   360   \textcolor{blue}{

   361   \begin{tabular}{l}

   362   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\

   363   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\

   364   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\

   365   \end{tabular}\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}

   366   \end{center}}

   367   \only<3>{\small

   368   \textcolor{blue}{

   369   \begin{center}

   370   \mbox{

   371   \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}

   372   {\mbox{\begin{tabular}{@ {}l@ {}}

   373   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\

   374   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\

   375   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\

   376   \end{tabular}}

   377   }

   378   }

   379   \end{center}

   380   }}

   381   \only<4>{\small

   382   \textcolor{blue}{

   383   \begin{center}

   384   \mbox{

   385   \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}

   386   {\mbox{\begin{tabular}{@ {}l@ {}}

   387   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}\\

   388   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\

   389   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\

   390   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\

   391   \end{tabular}}

   392   }

   393   }

   394   \end{center}

   395   }}

   396 

   397   \end{itemize}

   398 

   399   \end{frame}}

   400   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   401 

   402 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   403   \mode<presentation>{

   404   \begin{frame}[c]

   405 

   406 {\lstset{language=Scala}\fontsize{10}{12}\selectfont

   407 \texttt{\lstinputlisting{programs/judgement.scala}}}

   408 

   409   \end{frame}}

   410   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   411 

   412 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   413   \mode<presentation>{

   414   \begin{frame}[t]

   415   \frametitle{Inference Rules}

   416 

   417   \textcolor{blue}{

   418   \begin{center}

   419   \Large

   420   \mbox{

   421   \infer{\mbox{\isa{conclusion}}}

   422         {\mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}} & \mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub n}}}}

   423   \end{center}}

   424 

   425   The conlusion and premises are judgements\bigskip\pause

   426 

   427   \begin{itemize}

   428   \item Examples

   429   \textcolor{blue}{

   430   \begin{center}

   431   \mbox{

   432   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}

   433         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}

   434   \end{center}}\pause

   435 

   436   \textcolor{blue}{

   437   \begin{center}

   438   \mbox{

   439   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}

   440         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}

   441   \hspace{10mm}

   442   \mbox{

   443   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}

   444         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}

   445   \end{center}}

   446   \end{itemize}

   447 

   448   \end{frame}}

   449   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   450 %

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

   452   \mode<presentation>{

   453   \begin{frame}[t]

   454   \frametitle{Implication}

   455   \Large

   456 

   457   \textcolor{blue}{

   458   \begin{center}

   459   \mbox{

   460   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}

   461         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}

   462   \end{center}}

   463 

   464   \textcolor{blue}{

   465   \begin{center}

   466   \mbox{

   467   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}

   468         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}

   469   \end{center}}

   470 

   471   \end{frame}}

   472   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   473 %

   474 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   475   \mode<presentation>{

   476   \begin{frame}[t]

   477   \frametitle{Universal Quantification}

   478   \Large

   479 

   480   \textcolor{blue}{

   481   \begin{center}

   482   \mbox{

   483   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5D}{\isacharbrackright}}}}}

   484         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}}}}

   485   \end{center}}

   486 

   487   \end{frame}}

   488   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   489 %

   490 

   491 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   492   \mode<presentation>{

   493   \begin{frame}[t]

   494   \frametitle{Start Rules / Axioms}

   495 

   496   \normalsize

   497   \alert{if \textcolor{blue}{\isa{F\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}}

   498   

   499   \textcolor{blue}{\Large

   500   \begin{center}

   501   \mbox{

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

   503   \end{center}}\bigskip\pause

   504 

   505   \normalsize

   506   Also written as:

   507   \textcolor{blue}{\Large

   508   \begin{center}

   509   \mbox{

   510   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}}

   511   \end{center}}\pause

   512 

   513   \textcolor{blue}{\Large

   514   \begin{center}

   515   \mbox{

   516   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ true}}}{}}

   517   \end{center}}

   518 

   519   \end{frame}}

   520   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   521 %

   522 

   523 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   524   \mode<presentation>{

   525   \begin{frame}[t]

   526   \frametitle{}

   527  

   528  \begin{minipage}{1.1\textwidth}

   529   Let \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\footnotesize\begin{tabular}{l}

   530   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\

   531   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\

   532   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\

   533   \end{tabular}}

   534   \end{minipage}

   535 

   536   \only<2>{

   537   \begin{textblock}{12}(4,3)\footnotesize

   538   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}\hspace{10mm}

   539   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}

   540   \end{textblock}}

   541 

   542   \only<3->{

   543   \begin{textblock}{12}(4,3)\footnotesize

   544   \mbox{\textcolor{blue}{

   545   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}

   546   {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} &\hspace{10mm}

   547    \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}

   548   }}

   549   \end{textblock}}

   550 

   551   \only<4>{

   552   \begin{textblock}{14}(0.5,6)\footnotesize

   553   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}}

   554   \end{textblock}}

   555 

   556   \only<5->{

   557   \begin{textblock}{14}(0.5,6)\footnotesize

   558   \textcolor{blue}{

   559   \infer{\mbox{\begin{tabular}{l}\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ 

   560            \hspace{40mm}\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\end{tabular}}}

   561         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}}}}

   562   \end{textblock}}

   563 

   564   \only<6->{

   565   \begin{textblock}{14}(5,10)\footnotesize

   566   \textcolor{blue}{

   567   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}

   568         {\vdots & \hspace{30mm} \vdots}}

   569   \end{textblock}}

   570 

   571   \end{frame}}

   572   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   573 %

   574 

   575 

   576 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   577   \mode<presentation>{

   578   \begin{frame}[t]

   579   \frametitle{Access Control}

   580   \Large

   581 

   582   \textcolor{blue}{

   583   \begin{center}

   584   \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}

   585   \end{center}}\bigskip

   586 

   587   \normalsize

   588   \begin{itemize}

   589   \item If there is a proof \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} yes (granted)

   590   \item If there isn't \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} no (denied)

   591   \end{itemize}\bigskip\pause

   592 

   593 \begin{minipage}{1.1\textwidth}	

   594   \small

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

   596   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\

   597   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\

   598   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\

   599   \end{tabular}}\medskip

   600   

   601   \textcolor{blue}{

   602   \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} $\not\vdash$ \isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}

   603 \end{minipage}

   604   \end{frame}}

   605   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   606 %

   607 

   608 

   609 

   610 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   611 \mode<presentation>{

   612 \begin{frame}[c]

   613 \frametitle{The Access Control Problem}

   614 

   615 

   616 \begin{center}

   617   \begin{tikzpicture}[scale=1]

   618   

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

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

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

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

   623  

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

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

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

   627   

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

   629 

   630   \end{tikzpicture}

   631 \end{center}

   632 

   633 \end{frame}}

   634 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   635 

   636 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   637   \mode<presentation>{

   638   \begin{frame}[c]

   639   \frametitle{Bad News}

   640   

   641   \begin{itemize}

   642   \item We introduced (roughly) first-order logic. \bigskip\pause

   643 

   644   \item Judgements

   645   \begin{center}

   646   \textcolor{blue}

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

   648   \end{center}

   649 

   650   are in general \alert{undecidable}.\pause\medskip\\ 

   651  

   652   The problem is \alert{semi-decidable}.

   653  

   654   \end{itemize}

   655 

   656 

   657   \end{frame}}

   658   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   659 %

   660 

   661 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   662   \mode<presentation>{

   663   \begin{frame}[t]

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

   665   

   666   \begin{itemize}

   667   \item[]

   668   

   669   \begin{center}\color{blue}

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

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

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

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

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

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

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

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

   678   \end{tabular}

   679   \end{center}

   680 

   681   where \textcolor{blue}{\isa{P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ Alice{\isaliteral{2C}{\isacharcomma}}\ Bob{\isaliteral{2C}{\isacharcomma}}\ Christian{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}} (principals)\bigskip\pause

   682   

   683   \item \textcolor{blue}{\isa{HoD\ says\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}

   684   \end{itemize}

   685   

   686 

   687   

   688   \end{frame}}

   689   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   690 %

   691 

   692 

   693 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   694   \mode<presentation>{

   695   \begin{frame}[c]

   696 

   697 {\lstset{language=Scala}\fontsize{10}{12}\selectfont

   698 \texttt{\lstinputlisting{programs/formulas1.scala}}}

   699 

   700   \end{frame}}

   701   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   702 

   703 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   704   \mode<presentation>{

   705   \begin{frame}[t]

   706   \frametitle{Rules about Says}

   707 

   708   \textcolor{blue}{

   709   \begin{center}

   710   \mbox{

   711   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}

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

   713   \end{center}}

   714 

   715   \textcolor{blue}{

   716   \begin{center}

   717   \mbox{

   718   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}

   719         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{10mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}

   720   \end{center}}

   721 

   722   \textcolor{blue}{

   723   \begin{center}

   724   \mbox{

   725   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}

   726         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}}}}}

   727   \end{center}}

   728 

   729   \end{frame}}

   730   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   731 %

   732 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   733   \mode<presentation>{

   734   \begin{frame}[c]

   735   \frametitle{}

   736 

   737   Consider the following scenario:

   738 

   739   \begin{itemize}

   740   \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} 

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

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

   743   \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted.

   744   \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}.

   745   \end{itemize}\bigskip\pause

   746 

   747   \small

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

   749   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\

   750   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\

   751   \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\

   752   \end{tabular}}\medskip\pause

   753 

   754   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}

   755   \end{frame}}

   756   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   757 %

   758 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   759   \mode<presentation>{

   760   \begin{frame}[c]

   761   \frametitle{}

   762 

   763   \textcolor{blue}{

   764   \begin{center}

   765   \mbox{

   766   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}

   767         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}\\\bigskip

   768   \mbox{

   769   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}

   770         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{5mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}

   771   \end{center}}\bigskip

   772 

   773   \small

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

   775   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\

   776   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\

   777   \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\

   778   \end{tabular}}\medskip

   779 

   780   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}

   781   \end{frame}}

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

   783 %

   784 

   785 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   786   \mode<presentation>{

   787   \begin{frame}[t]

   788   \frametitle{}

   789   \small

   790 

   791   \textcolor{blue}{

   792   \begin{center}

   793   \only<1>{$ \underbrace{

   794   \mbox{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file)}}

   795   {\infer{\Gamma \vdash \mbox{Bob says del\_file}}{}}}}_{X}$}

   796   \end{center}}

   797 

   798   \textcolor{blue}{

   799   \begin{center}

   800   \only<1>{

   801   $ \underbrace{

   802   \mbox{\infer{\Gamma \vdash \mbox{Admin says del\_file}}

   803   {\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file)}}{}

   804    &

   805    \deduce[$\vdots$]{X}{}

   806   }}}_{Y}$}

   807   \end{center}}

   808 

   809   \textcolor{blue}{

   810   \begin{center}

   811   \only<1>{\mbox{\infer{\Gamma \vdash \mbox{del\_file}}

   812   {\infer{\Gamma \vdash \mbox{(Admin says del\_file) \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file}}{}

   813    &

   814    \deduce[$\vdots$]{Y}{}

   815   }}}

   816   \end{center}}

   817 

   818   \end{frame}}

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

   820 %

   821 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   822   \mode<presentation>{

   823   \begin{frame}[c]

   824   \frametitle{Controls}

   825   \small

   826   

   827   \begin{itemize}

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

   829 

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

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

   832 

   833   \begin{center}

   834   \bl{\mbox{

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

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

   837   }}

   838   \end{center}\pause

   839 

   840   \begin{center}

   841   \bl{\mbox{

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

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

   844   }}

   845   \end{center}

   846   \end{itemize}

   847 

   848   \end{frame}}

   849   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   850 %

   851 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   852   \mode<presentation>{

   853   \begin{frame}[c]

   854   \frametitle{Speaks For}

   855   \small

   856   

   857   \begin{itemize}

   858   \item \bl{\isa{P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}F{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ says\ F{\isaliteral{29}{\isacharparenright}}}}

   859 

   860   \item its meaning ``\bl{P} speaks for \bl{Q}''

   861   

   862 

   863   \begin{center}

   864   \bl{\mbox{

   865   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}}

   866         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}

   867   }}

   868   \end{center}\pause

   869 

   870   \begin{center}

   871   \bl{\mbox{

   872   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}}}

   873         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ controls\ F}}}

   874   }}

   875   \end{center}

   876 

   877   \begin{center}

   878   \bl{\mbox{

   879   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}}

   880         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}}

   881   }}

   882   \end{center}

   883   \end{itemize}

   884 

   885   \end{frame}}

   886   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   887 %

   888 

   889 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   890   \mode<presentation>{

   891   \begin{frame}[c]

   892   \frametitle{Tickets}

   893   

   894   \begin{itemize}

   895   \item Tickets control access to restricted objects.\bigskip

   896   \end{itemize}

   897   \small

   898 

   899   Example: \bl{Permitted (Bob, enter\_flight)} ? \bigskip

   900   

   901   \begin{minipage}{1.1\textwidth}

   902   \begin{itemize}

   903   \item \bl{Bob says Permitted (Bob, enter\_flight)}\\ (access request)

   904   \item \bl{Ticket says (Bob controls Permitted (Bob, enter\_flight))}

   905   \item \bl{Airline controls (Bob controls Permitted (Bob, enter\_flight))} (access policy)\pause

   906   \item \bl{\isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Airline}}\\ 

   907   (trust assumption)

   908   \end{itemize}

   909   \end{minipage}

   910 

   911   \end{frame}}

   912   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   913 %

   914 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   915   \mode<presentation>{

   916   \begin{frame}[c]

   917   \frametitle{Tickets}

   918   \small

   919 

   920   \begin{minipage}{1.1\textwidth}

   921   \begin{enumerate}

   922   \item \bl{Bob says Permitted (Bob, enter\_flight)}

   923   \item \bl{Ticket says (Bob controls Permitted (Bob, enter\_flight))}

   924   \item \bl{Airline controls (Bob controls Permitted (Bob, enter\_flight))}

   925   \item \bl{\isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Airline}}

   926   \end{enumerate}

   927   \end{minipage}\bigskip\bigskip

   928 

   929   Is  \bl{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Permitted\ {\isaliteral{28}{\isacharparenleft}}Bob{\isaliteral{2C}{\isacharcomma}}\ enter{\isaliteral{5F}{\isacharunderscore}}flight{\isaliteral{29}{\isacharparenright}}}} derivable ? \bigskip

   930 

   931 

   932   \small

   933   \begin{minipage}{1.1\textwidth}

   934   \begin{center}

   935   \bl{\mbox{

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

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

   938   }}

   939   \bl{\mbox{\hspace{6mm}

   940   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}}

   941         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}

   942   }}

   943   \end{center}

   944   \end{minipage}

   945 

   946   \end{frame}}

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

   948 %

   949 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   950   \mode<presentation>{

   951   \begin{frame}[c]

   952   \frametitle{Tickets}

   953   \small

   954   

   955   \begin{minipage}{1.1\textwidth}

   956   \begin{itemize}

   957   \item Access Request:

   958   \begin{center}

   959   \bl{Person says Object}

   960   \end{center}

   961 

   962   \item Ticket:

   963   \begin{center}

   964   \bl{Ticket says (Person controls Object)}

   965   \end{center}

   966 

   967   \item Access policy:

   968   \begin{center}

   969   \bl{Authority controls (Person controls Object)}

   970   \end{center}

   971 

   972   \item Trust assumption:

   973   \begin{center}

   974   \bl{\isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Authority}}

   975   \end{center}

   976   \end{itemize}

   977   \end{minipage}

   978 

   979 

   980   \end{frame}}

   981   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   982 %

   983 

   984 

   985 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   986   \mode<presentation>{

   987   \begin{frame}[t]

   988   \frametitle{\LARGE Derived Rule for Tickets}

   989   \small

   990   \mbox{}\\[2cm]

   991   

   992   \begin{center}

   993   \bl{\mbox{\infer{\mbox{F}}

   994      {\mbox{\begin{tabular}{l}

   995       Authority controls (Person controls F)\\

   996       Ticket says (Person controls F)\\

   997       \isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Authority}\\

   998       Person says F

   999       \end{tabular}}

  1000      }}}

  1001   \end{center}

  1002   \mbox{}\\[1cm]

  1003 

  1004  

  1005   \small

  1006   \begin{minipage}{1.1\textwidth}

  1007   \begin{center}

  1008   \bl{\mbox{

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

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

  1011   }}

  1012   \bl{\mbox{\hspace{6mm}

  1013   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}}

  1014         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}

  1015   }}

  1016   \end{center}

  1017   \end{minipage}

  1018 

  1019   \end{frame}}

  1020   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1021 %

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

  1023 

  1024 

  1025 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1026   \mode<presentation>{

  1027   \begin{frame}[c]

  1028   \frametitle{Security Levels}

  1029   \small

  1030 

  1031   \begin{itemize}

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

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

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

  1035   \end{itemize}

  1036 

  1037   \begin{center}

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

  1039   \end{center}

  1040 

  1041   \begin{itemize}

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

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

  1044   \end{itemize}

  1045 

  1046   \end{frame}}

  1047   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1048 %

  1049 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1050   \mode<presentation>{

  1051   \begin{frame}[c]

  1052   \frametitle{Reading a File}

  1053 

  1054   \bl{\begin{center}

  1055   \begin{tabular}{c}

  1056   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1064   \end{tabular}\\

  1065   \hline

  1066   Permitted $($File, read$)$

  1067   \end{tabular}

  1068   \end{center}}

  1069 

  1070   \end{frame}}

  1071   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1072 %

  1073 

  1074 

  1075 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1076   \mode<presentation>{

  1077   \begin{frame}[c]

  1078   \frametitle{Substitution Rule}

  1079   \small

  1080   

  1081   \bl{\begin{center}

  1082   \begin{tabular}{c}

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

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

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

  1086   \end{tabular}

  1087   \end{center}}\bigskip\pause

  1088 

  1089   \begin{itemize}

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

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

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

  1093   \end{itemize}

  1094 

  1095   \end{frame}}

  1096   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1097 %

  1098 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1099   \mode<presentation>{

  1100   \begin{frame}[c]

  1101   \frametitle{Reading a File}

  1102 

  1103   \bl{\begin{center}

  1104   \begin{tabular}{c}

  1105   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

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

  1114   \end{tabular}\\

  1115   \hline

  1116   Permitted $($File, read$)$

  1117   \end{tabular}

  1118   \end{center}}

  1119 

  1120   \end{frame}}

  1121   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1122 %

  1123 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1124   \mode<presentation>{

  1125   \begin{frame}[c]

  1126   \frametitle{Transitivity Rule}

  1127   \small

  1128   

  1129   \bl{\begin{center}

  1130   \begin{tabular}{c}

  1131   $\Gamma \vdash l_1 < l_2$ 

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

  1133   $\Gamma \vdash l_1 < l_3$

  1134   \end{tabular}