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 

   163 \end{frame}}

   164 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   165 

   166 

   167 

   168 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   169 \mode<presentation>{

   170 \begin{frame}[c]

   171 \frametitle{The Access Control Problem}

   172 

   173 

   174 \begin{center}

   175   \begin{tikzpicture}[scale=1]

   176   

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

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

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

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

   181  

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

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

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

   185   

   186   \draw (0.6,4) node {\begin{tabular}{l}\large Some Rules\\(access policy)\end{tabular}};

   187 

   188   \end{tikzpicture}

   189 \end{center}

   190 

   191 \end{frame}}

   192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   193 

   194 

   195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   196 \mode<presentation>{

   197 \begin{frame}[c]

   198 \frametitle{Access Control Logic}

   199 

   200 Ross Anderson about the use of Logic:\bigskip

   201 

   202 \begin{quote}

   203 Formal methods can be an excellent way of finding 

   204 bugs in security protocol designs as they force the designer 

   205 to make everything explicit and thus confront difficult design 

   206 choices that might otherwise be fudged. 

   207 \end{quote}

   208 

   209 \end{frame}}

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

   211 

   212 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   213 \mode<presentation>{

   214 \begin{frame}[c]

   215 

   216 \begin{center}

   217   \begin{tikzpicture}[scale=1]

   218   

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

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

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

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

   223  

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

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

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

   227   

   228   \draw (0.6,3.7) node {\begin{tabular}{l}Access Policy\end{tabular}};

   229 

   230   \end{tikzpicture}

   231 \end{center}

   232 

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

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

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

   236 

   237 

   238 \end{frame}}

   239 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   240 

   241  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   242   \mode<presentation>{

   243   \begin{frame}[c]

   244   \small

   245   \begin{center}

   246   \mbox{

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

   248          \ldots\\

   249          is\_at\_library (Christian)\\ 

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

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

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

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

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

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

   256        \end{tabular}

   257         }}

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

   259   \end{center}

   260   \end{frame}}

   261 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   262 

   263   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   264   \mode<presentation>{

   265   \begin{frame}[c]

   266   \frametitle{}

   267 

   268   There are two solutions for the problem:\medskip

   269 

   270   \begin{itemize}

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

   272   the problem,\medskip

   273 

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

   275   this language.

   276   \end{itemize}

   277   

   278   \end{frame}}

   279   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   280 

   281 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   282   \mode<presentation>{

   283   \begin{frame}[t]

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

   285 

   286   \begin{itemize}

   287   \item Formulas

   288 

   289   \begin{center}\color{blue}

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

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

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

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

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

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

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

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

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

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

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

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

   302   \end{tabular}

   303   \end{center}

   304 

   305   \end{itemize}

   306 

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

   308   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}}}}

   309   \end{textblock}

   310   

   311   \end{frame}}

   312   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   313 %

   314 

   315 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   316   \mode<presentation>{

   317   \begin{frame}[c]

   318 

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

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

   321 

   322   \end{frame}}

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

   324 

   325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   326   \mode<presentation>{

   327   \begin{frame}[t]

   328   \frametitle{Judgements}

   329 

   330   \begin{center}

   331   \LARGE

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

   333   \end{center}

   334 

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

   336 

   337   \begin{itemize}

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

   339 

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

   341   \textcolor{blue}{

   342   \begin{tabular}{l}

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

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

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

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

   347   \end{center}}

   348   \only<3>{\small

   349   \textcolor{blue}{

   350   \begin{center}

   351   \mbox{

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

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

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

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

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

   357   \end{tabular}}

   358   }

   359   }

   360   \end{center}

   361   }}

   362   \only<4>{\small

   363   \textcolor{blue}{

   364   \begin{center}

   365   \mbox{

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

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

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

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

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

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

   372   \end{tabular}}

   373   }

   374   }

   375   \end{center}

   376   }}

   377 

   378   \end{itemize}

   379 

   380   \end{frame}}

   381   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   382 

   383 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   384   \mode<presentation>{

   385   \begin{frame}[c]

   386 

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

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

   389 

   390   \end{frame}}

   391   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   392 

   393 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   394   \mode<presentation>{

   395   \begin{frame}[t]

   396   \frametitle{Inference Rules}

   397 

   398   \textcolor{blue}{

   399   \begin{center}

   400   \Large

   401   \mbox{

   402   \infer{\mbox{\isa{conclusion}}}

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

   404   \end{center}}

   405 

   406   The conlusion and premises are judgements\bigskip\pause

   407 

   408   \begin{itemize}

   409   \item Examples

   410   \textcolor{blue}{

   411   \begin{center}

   412   \mbox{

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

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

   415   \end{center}}\pause

   416 

   417   \textcolor{blue}{

   418   \begin{center}

   419   \mbox{

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

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

   422   \hspace{10mm}

   423   \mbox{

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

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

   426   \end{center}}

   427   \end{itemize}

   428 

   429   \end{frame}}

   430   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   431 %

   432 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   433   \mode<presentation>{

   434   \begin{frame}[t]

   435   \frametitle{Implication}

   436   \Large

   437 

   438   \textcolor{blue}{

   439   \begin{center}

   440   \mbox{

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

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

   443   \end{center}}

   444 

   445   \textcolor{blue}{

   446   \begin{center}

   447   \mbox{

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

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

   450   \end{center}}

   451 

   452   \end{frame}}

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

   454 %

   455 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   456   \mode<presentation>{

   457   \begin{frame}[t]

   458   \frametitle{Universal Quantification}

   459   \Large

   460 

   461   \textcolor{blue}{

   462   \begin{center}

   463   \mbox{

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

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

   466   \end{center}}

   467 

   468   \end{frame}}

   469   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   470 %

   471 

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

   473   \mode<presentation>{

   474   \begin{frame}[t]

   475   \frametitle{Start Rules / Axioms}

   476 

   477   \normalsize

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

   479   

   480   \textcolor{blue}{\Large

   481   \begin{center}

   482   \mbox{

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

   484   \end{center}}\bigskip\pause

   485 

   486   \normalsize

   487   Also written as:

   488   \textcolor{blue}{\Large

   489   \begin{center}

   490   \mbox{

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

   492   \end{center}}\pause

   493 

   494   \textcolor{blue}{\Large

   495   \begin{center}

   496   \mbox{

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

   498   \end{center}}

   499 

   500   \end{frame}}

   501   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   502 %

   503 

   504 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   505   \mode<presentation>{

   506   \begin{frame}[t]

   507   \frametitle{}

   508   

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

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

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

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

   513   \end{tabular}}

   514 

   515   \only<2>{

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

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

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

   519   \end{textblock}}

   520 

   521   \only<3->{

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

   523   \mbox{\textcolor{blue}{

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

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

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

   527   }}

   528   \end{textblock}}

   529 

   530   \only<4>{

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

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

   533   \end{textblock}}

   534 

   535   \only<5->{

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

   537   \textcolor{blue}{

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

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

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

   541   \end{textblock}}

   542 

   543   \only<6->{

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

   545   \textcolor{blue}{

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

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

   548   \end{textblock}}

   549 

   550   \end{frame}}

   551   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   552 %

   553 

   554 

   555 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   556   \mode<presentation>{

   557   \begin{frame}[t]

   558   \frametitle{Access Control}

   559   \Large

   560 

   561   \textcolor{blue}{

   562   \begin{center}

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

   564   \end{center}}\bigskip

   565 

   566   \normalsize

   567   \begin{itemize}

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

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

   570   \end{itemize}\bigskip\pause

   571 

   572   \small

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

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

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

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

   577   \end{tabular}}\medskip

   578   

   579   \textcolor{blue}{

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

   581 

   582   \end{frame}}

   583   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   584 %

   585 

   586 

   587 

   588 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   589 \mode<presentation>{

   590 \begin{frame}[c]

   591 \frametitle{The Access Control Problem}

   592 

   593 

   594 \begin{center}

   595   \begin{tikzpicture}[scale=1]

   596   

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

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

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

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

   601  

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

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

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

   605   

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

   607 

   608   \end{tikzpicture}

   609 \end{center}

   610 

   611 \end{frame}}

   612 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   613 

   614 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   615   \mode<presentation>{

   616   \begin{frame}[c]

   617   \frametitle{Bad News}

   618   

   619   \begin{itemize}

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

   621 

   622   \item Judgements

   623   \begin{center}

   624   \textcolor{blue}

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

   626   \end{center}

   627 

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

   629  

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

   631  

   632   \end{itemize}

   633 

   634 

   635   \end{frame}}

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

   637 %

   638 

   639 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   640   \mode<presentation>{

   641   \begin{frame}[t]

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

   643   

   644   \begin{itemize}

   645   \item[]

   646   

   647   \begin{center}\color{blue}

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

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

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

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

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

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

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

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

   656   \end{tabular}

   657   \end{center}

   658 

   659   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

   660   

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

   662   \end{itemize}

   663   

   664 

   665   

   666   \end{frame}}

   667   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   668 %

   669 

   670 

   671 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   672   \mode<presentation>{

   673   \begin{frame}[t]

   674   \frametitle{Rules about Says}

   675 

   676   \textcolor{blue}{

   677   \begin{center}

   678   \mbox{

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

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

   681   \end{center}}

   682 

   683   \textcolor{blue}{

   684   \begin{center}

   685   \mbox{

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

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

   688   \end{center}}

   689 

   690   \textcolor{blue}{

   691   \begin{center}

   692   \mbox{

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

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

   695   \end{center}}

   696 

   697   \end{frame}}

   698   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   699 %

   700 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   701   \mode<presentation>{

   702   \begin{frame}[c]

   703   \frametitle{}

   704 

   705   Consider the following scenario:

   706 

   707   \begin{itemize}

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

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

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

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

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

   713   \end{itemize}\bigskip\pause

   714 

   715   \small

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

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

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

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

   720   \end{tabular}}\medskip\pause

   721 

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

   723   \end{frame}}

   724   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   725 %

   726 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   727   \mode<presentation>{

   728   \begin{frame}[c]

   729   \frametitle{}

   730 

   731   \textcolor{blue}{

   732   \begin{center}

   733   \mbox{

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

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

   736   \mbox{

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

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

   739   \end{center}}\bigskip

   740 

   741   \small

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

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

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

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

   746   \end{tabular}}\medskip

   747 

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

   749   \end{frame}}

   750   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   751 %

   752 

   753 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   754   \mode<presentation>{

   755   \begin{frame}[t]

   756   \frametitle{}

   757   \small

   758 

   759   \textcolor{blue}{

   760   \begin{center}

   761   \only<1>{$ \underbrace{

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

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

   764   \end{center}}

   765 

   766   \textcolor{blue}{

   767   \begin{center}

   768   \only<1>{

   769   $ \underbrace{

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

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

   772    &

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

   774   }}}_{Y}$}

   775   \end{center}}

   776 

   777   \textcolor{blue}{

   778   \begin{center}

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

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

   781    &

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

   783   }}}

   784   \end{center}}

   785 

   786   \end{frame}}

   787   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   788 %

   789 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   790   \mode<presentation>{

   791   \begin{frame}[c]

   792   \frametitle{Controls}

   793   \small

   794   

   795   \begin{itemize}

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

   797 

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

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

   800 

   801   \begin{center}

   802   \bl{\mbox{

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

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

   805   }}

   806   \end{center}\pause

   807 

   808   \begin{center}

   809   \bl{\mbox{

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

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

   812   }}

   813   \end{center}

   814   \end{itemize}

   815 

   816   \end{frame}}

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

   818 %

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

   820   \mode<presentation>{

   821   \begin{frame}[c]

   822   \frametitle{Speaks For}

   823   \small

   824   

   825   \begin{itemize}

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

   827 

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

   829   

   830 

   831   \begin{center}

   832   \bl{\mbox{

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

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

   835   }}

   836   \end{center}\pause

   837 

   838   \begin{center}

   839   \bl{\mbox{

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

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

   842   }}

   843   \end{center}

   844 

   845   \begin{center}

   846   \bl{\mbox{

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

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

   849   }}

   850   \end{center}

   851   \end{itemize}

   852 

   853   \end{frame}}

   854   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   855 %

   856 

   857 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   858   \mode<presentation>{

   859   \begin{frame}[c]

   860   \frametitle{Tickets}

   861   

   862   \begin{itemize}

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

   864   \end{itemize}

   865   \small

   866 

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

   868   

   869   \begin{minipage}{1.1\textwidth}

   870   \begin{itemize}

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

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

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

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

   875   (trust assumption)

   876   \end{itemize}

   877   \end{minipage}

   878 

   879   \end{frame}}

   880   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   881 %

   882 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   883   \mode<presentation>{

   884   \begin{frame}[c]

   885   \frametitle{Tickets}

   886   \small

   887 

   888   \begin{minipage}{1.1\textwidth}

   889   \begin{enumerate}

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

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

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

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

   894   \end{enumerate}

   895   \end{minipage}\bigskip\bigskip

   896 

   897   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

   898 

   899 

   900   \footnotesize

   901   \begin{center}

   902   \bl{\mbox{

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

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

   905   }}

   906   \bl{\mbox{\hspace{10mm}

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

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

   909   }}

   910   \end{center}

   911 

   912   \end{frame}}

   913   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   914 %

   915 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   916   \mode<presentation>{

   917   \begin{frame}[c]

   918   \frametitle{Tickets}

   919   \small

   920   

   921   \begin{minipage}{1.1\textwidth}

   922   \begin{itemize}

   923   \item Access Request:

   924   \begin{center}

   925   \bl{Person says Object}

   926   \end{center}

   927 

   928   \item Ticket:

   929   \begin{center}

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

   931   \end{center}

   932 

   933   \item Access policy:

   934   \begin{center}

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

   936   \end{center}

   937 

   938   \item Trust assumption:

   939   \begin{center}

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

   941   \end{center}

   942   \end{itemize}

   943   \end{minipage}

   944 

   945 

   946   \end{frame}}

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

   948 %

   949 

   950 

   951 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   952   \mode<presentation>{

   953   \begin{frame}[t]

   954   \frametitle{\LARGE Derived Rule for Tickets}

   955   \small

   956   \mbox{}\\[2cm]

   957   

   958   \begin{center}

   959   \bl{\mbox{\infer{\mbox{F}}

   960      {\mbox{\begin{tabular}{l}

   961       Authority controls (Person controls F)\\

   962       Ticket says (Person controls F)\\

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

   964       Person says F

   965       \end{tabular}}

   966      }}}

   967   \end{center}

   968   \mbox{}\\[1cm]

   969 

   970 

   971   \footnotesize

   972   \begin{center}

   973   \bl{\mbox{

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

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

   976   }}

   977   \bl{\mbox{\hspace{10mm}

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

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

   980   }}

   981   \end{center}

   982 

   983   \end{frame}}

   984   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   985 %

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

   987 

   988 

   989 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   990   \mode<presentation>{

   991   \begin{frame}[c]

   992   \frametitle{Security Levels}

   993   \small

   994 

   995   \begin{itemize}

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

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

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

   999   \end{itemize}

  1000 

  1001   \begin{center}

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

  1003   \end{center}

  1004 

  1005   \begin{itemize}

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

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

  1008   \end{itemize}

  1009 

  1010   \end{frame}}

  1011   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1012 %

  1013 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1014   \mode<presentation>{

  1015   \begin{frame}[c]

  1016   \frametitle{Reading a File}

  1017 

  1018   \bl{\begin{center}

  1019   \begin{tabular}{c}

  1020   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1028   \end{tabular}\\

  1029   \hline

  1030   Permitted $($File, read$)$

  1031   \end{tabular}

  1032   \end{center}}

  1033 

  1034   \end{frame}}

  1035   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1036 %

  1037 

  1038 

  1039 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1040   \mode<presentation>{

  1041   \begin{frame}[c]

  1042   \frametitle{Substitution Rule}

  1043   \small

  1044   

  1045   \bl{\begin{center}

  1046   \begin{tabular}{c}

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

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

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

  1050   \end{tabular}

  1051   \end{center}}\bigskip\pause

  1052 

  1053   \begin{itemize}

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

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

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

  1057   \end{itemize}

  1058 

  1059   \end{frame}}

  1060   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1061 %

  1062 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1063   \mode<presentation>{

  1064   \begin{frame}[c]

  1065   \frametitle{Reading a File}

  1066 

  1067   \bl{\begin{center}

  1068   \begin{tabular}{c}

  1069   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

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

  1078   \end{tabular}\\

  1079   \hline

  1080   Permitted $($File, read$)$

  1081   \end{tabular}

  1082   \end{center}}

  1083 

  1084   \end{frame}}

  1085   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1086 %

  1087 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1088   \mode<presentation>{

  1089   \begin{frame}[c]

  1090   \frametitle{Transitivity Rule}

  1091   \small

  1092   

  1093   \bl{\begin{center}

  1094   \begin{tabular}{c}

  1095   $\Gamma \vdash l_1 < l_2$ 

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

  1097   $\Gamma \vdash l_1 < l_3$

  1098   \end{tabular}

  1099   \end{center}}\bigskip

  1100 

  1101   \begin{itemize}

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

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

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

  1105   \end{itemize}

  1106 

  1107   \end{frame}}

  1108   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1109 %

  1110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1111   \mode<presentation>{

  1112   \begin{frame}[c]

  1113   \frametitle{Reading Files}

  1114 

  1115   \begin{itemize}

  1116   \item Access policy for reading

  1117   \end{itemize}

  1118 

  1119   \bl{\begin{center}

  1120   \begin{tabular}{c}

  1121   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1129   \end{tabular}\\

  1130   \hline

  1131   Permitted $($File, read$)$

  1132   \end{tabular}

  1133   \end{center}}

  1134 

  1135   \end{frame}}