diff -r be35ff24cccc -r d1d07f05325a slides05.tex --- a/slides05.tex Sun Dec 09 13:00:33 2012 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1296 +0,0 @@ -\documentclass[dvipsnames,14pt,t]{beamer} -\usepackage{proof} -\usepackage{beamerthemeplainculight} -\usepackage[T1]{fontenc} -\usepackage[latin1]{inputenc} -\usepackage{mathpartir} -\usepackage{isabelle} -\usepackage{isabellesym} -\usepackage[absolute,overlay]{textpos} -\usepackage{ifthen} -\usepackage{tikz} -\usepackage{courier} -\usepackage{listings} -\usetikzlibrary{arrows} -\usetikzlibrary{positioning} -\usetikzlibrary{calc} -\usepackage{graphicx} - -\isabellestyle{rm} -\renewcommand{\isastyle}{\rm}% -\renewcommand{\isastyleminor}{\rm}% -\renewcommand{\isastylescript}{\footnotesize\rm\slshape}% -\renewcommand{\isatagproof}{} -\renewcommand{\endisatagproof}{} -\renewcommand{\isamarkupcmt}[1]{#1} - -% Isabelle characters -\renewcommand{\isacharunderscore}{\_} -\renewcommand{\isacharbar}{\isamath{\mid}} -\renewcommand{\isasymiota}{} -\renewcommand{\isacharbraceleft}{\{} -\renewcommand{\isacharbraceright}{\}} -\renewcommand{\isacharless}{$\langle$} -\renewcommand{\isachargreater}{$\rangle$} -\renewcommand{\isasymsharp}{\isamath{\#}} -\renewcommand{\isasymdots}{\isamath{...}} -\renewcommand{\isasymbullet}{\act} - - - -\definecolor{javared}{rgb}{0.6,0,0} % for strings -\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments -\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords -\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc - -\lstset{language=Java, - basicstyle=\ttfamily, - keywordstyle=\color{javapurple}\bfseries, - stringstyle=\color{javagreen}, - commentstyle=\color{javagreen}, - morecomment=[s][\color{javadocblue}]{/**}{*/}, - numbers=left, - numberstyle=\tiny\color{black}, - stepnumber=1, - numbersep=10pt, - tabsize=2, - showspaces=false, - showstringspaces=false} - -\lstdefinelanguage{scala}{ - morekeywords={abstract,case,catch,class,def,% - do,else,extends,false,final,finally,% - for,if,implicit,import,match,mixin,% - new,null,object,override,package,% - private,protected,requires,return,sealed,% - super,this,throw,trait,true,try,% - type,val,var,while,with,yield}, - otherkeywords={=>,<-,<\%,<:,>:,\#,@}, - sensitive=true, - morecomment=[l]{//}, - morecomment=[n]{/*}{*/}, - morestring=[b]", - morestring=[b]', - morestring=[b]""" -} - -\lstset{language=Scala, - basicstyle=\ttfamily, - keywordstyle=\color{javapurple}\bfseries, - stringstyle=\color{javagreen}, - commentstyle=\color{javagreen}, - morecomment=[s][\color{javadocblue}]{/**}{*/}, - numbers=left, - numberstyle=\tiny\color{black}, - stepnumber=1, - numbersep=10pt, - tabsize=2, - showspaces=false, - showstringspaces=false} - -% beamer stuff -\renewcommand{\slidecaption}{APP 05, King's College London, 23 October 2012} - -\newcommand{\bl}[1]{\textcolor{blue}{#1}} -\begin{document} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}<1>[t] -\frametitle{% - \begin{tabular}{@ {}c@ {}} - \\ - \LARGE Access Control and \\[-3mm] - \LARGE Privacy Policies (5)\\[-6mm] - \end{tabular}}\bigskip\bigskip\bigskip - - %\begin{center} - %\includegraphics[scale=1.3]{pics/barrier.jpg} - %\end{center} - -\normalsize - \begin{center} - \begin{tabular}{ll} - Email: & christian.urban at kcl.ac.uk\\ - Of$\!$fice: & S1.27 (1st floor Strand Building)\\ - Slides: & KEATS (also homework is there)\\ - \end{tabular} - \end{center} - - -\end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Satan's Computer} - -Ross Anderson and Roger Needham wrote:\bigskip - -\begin{quote} -In effect, our task is to program a computer which gives -answers which are subtly and maliciously wrong at the most -inconvenient possible moment\ldots{} we hope that the lessons -learned from programming Satan's computer may be helpful -in tackling the more common problem of programming Murphy's. -\end{quote} - - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Protocol Specifications} - -The Needham-Schroeder Protocol: - -\begin{center} -\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} -Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B, N_A$}\\ -Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\ -Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}, A\}_{K_{BS}} $}\\ -Message 4 & \bl{$B \rightarrow A :$} & \bl{$\{N_B\}_{K_{AB}}$}\\ -Message 5 & \bl{$A \rightarrow B :$} & \bl{$\{N_B-1\}_{K_{AB}}$}\\ -\end{tabular} -\end{center} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Cryptographic Protocol Failures} - -Again Ross Anderson and Roger Needham wrote:\bigskip - -\begin{quote} -\textcolor{gray}{ -A lot of the recorded frauds were the result of this kind of blunder, or from -management negligence pure and simple.} However, there have been a -significant number of cases where the designers protected the right things, -used cryptographic algorithms which were not broken, and yet found that their -systems were still successfully attacked. -\end{quote} - - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{The Access Control Problem} - - -\begin{center} - \begin{tikzpicture}[scale=1] - - \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); - \draw (-2.7,1) node {\begin{tabular}{l}access\\request\end{tabular}}; - \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}}; - \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}}; - - \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); - \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); - \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); - - \draw (0.6,4) node {\begin{tabular}{l}\large some rules\\(access policy)\end{tabular}}; - - \end{tikzpicture} -\end{center} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Access Control Logic} - -Ross Anderson about the use of Logic:\bigskip - -\begin{quote} -Formal methods can be an excellent way of finding -bugs in security protocol designs as they force the designer -to make everything explicit and thus confront dif$\!$ficult design -choices that might otherwise be fudged. -\end{quote} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] - -\begin{center} - \begin{tikzpicture}[scale=1] - - \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); - \draw (-2.7,1) node {\begin{tabular}{l}access\\request\end{tabular}}; - \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}}; - \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}}; - - \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); - \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); - \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); - - \draw (0.6,3.7) node {\begin{tabular}{l}access policy\end{tabular}}; - - \end{tikzpicture} -\end{center} - -Assuming one file on my computer contains a virus.\smallskip\\ -\only<1>{Q: Given my access policy, can this file ``infect'' my whole computer?}% -\only<2>{Q: Can my access policy prevent that my whole computer gets infected.} - - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \small - \begin{center} - \mbox{ - \inferrule{\mbox{\begin{tabular}{l} - \ldots\\ - is\_at\_library (Christian)\\ - is\_student (a) $\wedge$ is\_at\_library (a) $\Rightarrow$ may\_obtain\_email (a)\\ - is\_staff (a) $\wedge$ is\_at\_library (a) $\Rightarrow$ may\_obtain\_email (a)\medskip\\ - \onslide<2->{HoD says is\_staff (a) $\Rightarrow$ is\_staff (a)}\\ - \onslide<2->{HoD says is\_staff (Christian)}\medskip\\ - \onslide<3->{may\_obtain\_email (a) $\wedge$ sending\_spam (a) $\Rightarrow$\\} - \onslide<3->{\hspace{6cm}$\neg$ may\_obtain\_email (a)} - \end{tabular} - }} - {\mbox{? may\_obtain\_email (Christian)}}} - \end{center} - \end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{} - - There are two ways for tackling such problems:\medskip - - \begin{itemize} - \item either you make up our own language in which you can describe - the problem,\medskip - - \item or you use an existing language and represent the problem in - this language. - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{\Large\begin{tabular}{@ {}c@ {}}Logic(s)\end{tabular}} - - \begin{itemize} - \item Formulas - - \begin{center}\color{blue} - \begin{tabular}{rcl@ {\hspace{10mm}}l} - \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F} & \textcolor{black}{implies}\\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F} & \textcolor{black}{negation}\\ - & \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}\\ - & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}} & - \onslide<2->{\textcolor{black}{forall quantification}}\\ - & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ F}} & - \onslide<2->{\textcolor{black}{exists quantification}}\\[-7mm] - \end{tabular} - \end{center} - - \end{itemize} - - \begin{textblock}{12}(1,14) - 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}}}} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - -{\lstset{language=Scala}\fontsize{10}{12}\selectfont -\texttt{\lstinputlisting{programs/formulas.scala}}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Judgements} - - \begin{center} - \LARGE - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}} - \end{center} - - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} is a collection of formulas, called the \alert{assumptions}\bigskip\pause - - \begin{itemize} - \item Example\mbox{}\\[-8mm] - - \only<2>{\begin{center}\tiny - \textcolor{blue}{ - \begin{tabular}{l} - \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ - \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ - \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}}}\\ - \end{tabular}\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} - \end{center}} - \only<3>{\small - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} - {\mbox{\begin{tabular}{@ {}l@ {}} - \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ - \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ - \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}}}\\ - \end{tabular}} - } - } - \end{center} - }} - \only<4>{\small - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}} - {\mbox{\begin{tabular}{@ {}l@ {}} - \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}\\ - \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ - \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ - \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}}}\\ - \end{tabular}} - } - } - \end{center} - }} - - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - -{\lstset{language=Scala}\fontsize{10}{12}\selectfont -\texttt{\lstinputlisting{programs/judgement.scala}}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Inference Rules} - - \textcolor{blue}{ - \begin{center} - \Large - \mbox{ - \infer{\mbox{\isa{conclusion}}} - {\mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}} & \mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub n}}}} - \end{center}} - - The conlusion and premises are judgements\bigskip\pause - - \begin{itemize} - \item Examples - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} - {\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}}}}}} - \end{center}}\pause - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} - \hspace{10mm} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} - \end{center}} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Implication} - \Large - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\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{2C}{\isacharcomma}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} - \end{center}} - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} - {\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}}}}}} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Universal Quantification} - \Large - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5D}{\isacharbrackright}}}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}}}} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Start Rules / Axioms} - - \normalsize - \alert{if \textcolor{blue}{\isa{F\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}} - - \textcolor{blue}{\Large - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}} - \end{center}}\bigskip\pause - - \normalsize - Also written as: - \textcolor{blue}{\Large - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}} - \end{center}}\pause - - \textcolor{blue}{\Large - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ true}}}{}} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{} - - \begin{minipage}{1.1\textwidth} - Let \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\footnotesize\begin{tabular}{l} - \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ - \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ - \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}}}\\ - \end{tabular}} - \end{minipage} - - \only<2>{ - \begin{textblock}{12}(4,3)\footnotesize - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}\hspace{10mm} - \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}}}} - \end{textblock}} - - \only<3->{ - \begin{textblock}{12}(4,3)\footnotesize - \mbox{\textcolor{blue}{ - \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}}}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} &\hspace{10mm} - \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} - }} - \end{textblock}} - - \only<4>{ - \begin{textblock}{14}(0.5,6)\footnotesize - \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}}}} - \end{textblock}} - - \only<5->{ - \begin{textblock}{14}(0.5,6)\footnotesize - \textcolor{blue}{ - \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}}}\\ - \hspace{40mm}\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\end{tabular}}} - {\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}}}}}} - \end{textblock}} - - \only<6->{ - \begin{textblock}{14}(5,10)\footnotesize - \textcolor{blue}{ - \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}}}}} - {\vdots & \hspace{30mm} \vdots}} - \end{textblock}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Access Control} - \Large - - \textcolor{blue}{ - \begin{center} - \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F} - \end{center}}\bigskip - - \normalsize - \begin{itemize} - \item If there is a proof \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} yes (granted) - \item If there isn't \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} no (denied) - \end{itemize}\bigskip\pause - -\begin{minipage}{1.1\textwidth} - \small - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} - \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ - \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ - \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}}}\\ - \end{tabular}}\medskip - - \textcolor{blue}{ - \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} $\not\vdash$ \isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}} -\end{minipage} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{The Access Control Problem} - - -\begin{center} - \begin{tikzpicture}[scale=1] - - \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); - \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; - \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}}; - \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}}; - - \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); - \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); - \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); - - \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}}; - - \end{tikzpicture} -\end{center} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Bad News} - - \begin{itemize} - \item We introduced (roughly) first-order logic. \bigskip\pause - - \item Judgements - \begin{center} - \textcolor{blue} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} - \end{center} - - are in general \alert{undecidable}.\pause\medskip\\ - - The problem is \alert{semi-decidable}. - - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}} - - \begin{itemize} - \item[] - - \begin{center}\color{blue} - \begin{tabular}[t]{rcl@ {\hspace{10mm}}l} - \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\ - & \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}}} \\ - & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\ - \end{tabular} - \end{center} - - 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 - - \item \textcolor{blue}{\isa{HoD\ says\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} - \end{itemize} - - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - -{\lstset{language=Scala}\fontsize{10}{12}\selectfont -\texttt{\lstinputlisting{programs/formulas1.scala}}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Rules about Says} - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}} - \end{center}} - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} - {\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}}}}}} - \end{center}} - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}}}}} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{} - - Consider the following scenario: - - \begin{itemize} - \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} - should be deleted, then this file must be deleted. - \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether - \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted. - \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}. - \end{itemize}\bigskip\pause - - \small - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} - \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}}},\\ - \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}}},\\ - \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\ - \end{tabular}}\medskip\pause - - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{} - - \textcolor{blue}{ - \begin{center} - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}\\\bigskip - \mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} - {\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}}}}}} - \end{center}}\bigskip - - \small - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} - \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}}},\\ - \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}}},\\ - \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\ - \end{tabular}}\medskip - - \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{} - \small - - \textcolor{blue}{ - \begin{center} - \only<1>{$ \underbrace{ - \mbox{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file)}} - {\infer{\Gamma \vdash \mbox{Bob says del\_file}}{}}}}_{X}$} - \end{center}} - - \textcolor{blue}{ - \begin{center} - \only<1>{ - $ \underbrace{ - \mbox{\infer{\Gamma \vdash \mbox{Admin says del\_file}} - {\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file)}}{} - & - \deduce[$\vdots$]{X}{} - }}}_{Y}$} - \end{center}} - - \textcolor{blue}{ - \begin{center} - \only<1>{\mbox{\infer{\Gamma \vdash \mbox{del\_file}} - {\infer{\Gamma \vdash \mbox{(Admin says del\_file) \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file}}{} - & - \deduce[$\vdots$]{Y}{} - }}} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Controls} - \small - - \begin{itemize} - \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} - - \item its meaning ``\bl{P} is entitled to do \bl{F}'' - \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause - - \begin{center} - \bl{\mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - }} - \end{center}\pause - - \begin{center} - \bl{\mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} - {\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}}} - }} - \end{center} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Speaks For} - \small - - \begin{itemize} - \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}}}} - - \item its meaning ``\bl{P} speaks for \bl{Q}'' - - - \begin{center} - \bl{\mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - }} - \end{center}\pause - - \begin{center} - \bl{\mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ controls\ F}}} - }} - \end{center} - - \begin{center} - \bl{\mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}} - {\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}}} - }} - \end{center} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Tickets} - - \begin{itemize} - \item Tickets control access to restricted objects.\bigskip - \end{itemize} - \small - - Example: \bl{Permitted (Bob, enter\_flight)} ? \bigskip - - \begin{minipage}{1.1\textwidth} - \begin{itemize} - \item \bl{Bob says Permitted (Bob, enter\_flight)}\\ (access request) - \item \bl{Ticket says (Bob controls Permitted (Bob, enter\_flight))} - \item \bl{Airline controls (Bob controls Permitted (Bob, enter\_flight))} (access policy)\pause - \item \bl{\isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Airline}}\\ - (trust assumption) - \end{itemize} - \end{minipage} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Tickets} - \small - - \begin{minipage}{1.1\textwidth} - \begin{enumerate} - \item \bl{Bob says Permitted (Bob, enter\_flight)} - \item \bl{Ticket says (Bob controls Permitted (Bob, enter\_flight))} - \item \bl{Airline controls (Bob controls Permitted (Bob, enter\_flight))} - \item \bl{\isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Airline}} - \end{enumerate} - \end{minipage}\bigskip\bigskip - - 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 - - - \small - \begin{minipage}{1.1\textwidth} - \begin{center} - \bl{\mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - }} - \bl{\mbox{\hspace{6mm} - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - }} - \end{center} - \end{minipage} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Tickets} - \small - - \begin{minipage}{1.1\textwidth} - \begin{itemize} - \item Access Request: - \begin{center} - \bl{Person says Object} - \end{center} - - \item Ticket: - \begin{center} - \bl{Ticket says (Person controls Object)} - \end{center} - - \item Access policy: - \begin{center} - \bl{Authority controls (Person controls Object)} - \end{center} - - \item Trust assumption: - \begin{center} - \bl{\isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Authority}} - \end{center} - \end{itemize} - \end{minipage} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{\LARGE Derived Rule for Tickets} - \small - \mbox{}\\[2cm] - - \begin{center} - \bl{\mbox{\infer{\mbox{F}} - {\mbox{\begin{tabular}{l} - Authority controls (Person controls F)\\ - Ticket says (Person controls F)\\ - \isa{Ticket\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Authority}\\ - Person says F - \end{tabular}} - }}} - \end{center} - \mbox{}\\[1cm] - - - \small - \begin{minipage}{1.1\textwidth} - \begin{center} - \bl{\mbox{ - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - }} - \bl{\mbox{\hspace{6mm} - \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}} - {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} - }} - \end{center} - \end{minipage} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Security Levels} - \small - - \begin{itemize} - \item Top secret (\bl{$T\!S$}) - \item Secret (\bl{$S$}) - \item Public (\bl{$P$}) - \end{itemize} - - \begin{center} - \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause - \end{center} - - \begin{itemize} - \item Bob has a clearance for ``secret'' - \item Bob can read documents that are public or sectret, but not top secret - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Reading a File} - - \bl{\begin{center} - \begin{tabular}{c} - \begin{tabular}{@ {}l@ {}} - \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\ - \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\ - Bob says Permitted $($File, read$)$\only<2->{\\} - \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}% - \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}% - \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}% - \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}% - \end{tabular}\\ - \hline - Permitted $($File, read$)$ - \end{tabular} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Substitution Rule} - \small - - \bl{\begin{center} - \begin{tabular}{c} - $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$ - \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline - $\Gamma \vdash slev(P) < slev(Q)$ - \end{tabular} - \end{center}}\bigskip\pause - - \begin{itemize} - \item \bl{$slev($Bob$)$ $=$ $S$} - \item \bl{$slev($File$)$ $=$ $P$} - \item \bl{$slev(P) < slev(S)$} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Reading a File} - - \bl{\begin{center} - \begin{tabular}{c} - \begin{tabular}{@ {}l@ {}} - $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\ - \hspace{3cm}Bob controls Permitted $($File, read$)$\\ - Bob says Permitted $($File, read$)$\\ - $slev($File$)$ $=$ $P$\\ - $slev($Bob$)$ $=$ $T\!S$\\ - \only<1>{\textcolor{red}{$?$}}% - \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}% - \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}% - \end{tabular}\\ - \hline - Permitted $($File, read$)$ - \end{tabular} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Transitivity Rule} - \small - - \bl{\begin{center} - \begin{tabular}{c} - $\Gamma \vdash l_1 < l_2$ - \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline - $\Gamma \vdash l_1 < l_3$ - \end{tabular} - \end{center}}\bigskip - - \begin{itemize} - \item \bl{$slev(P) < slev (S)$} - \item \bl{$slev(S) < slev (T\!S)$} - \item[] \bl{$slev(P) < slev (T\!S)$} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Reading Files} - - \begin{itemize} - \item Access policy for reading - \end{itemize} - - \bl{\begin{center} - \begin{tabular}{c} - \begin{tabular}{@ {}l@ {}} - $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\ - \hspace{3cm}Bob controls Permitted $(f$, read$)$\\ - Bob says Permitted $($File, read$)$\\ - $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\ - $slev($Bob$)$ $=$ $T\!S$\\ - $slev(P) < slev(S)$\\ - $slev(S) < slev(T\!S)$ - \end{tabular}\\ - \hline - Permitted $($File, read$)$ - \end{tabular} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Writing Files} - - \begin{itemize} - \item Access policy for \underline{writing} - \end{itemize} - - \bl{\begin{center} - \begin{tabular}{c} - \begin{tabular}{@ {}l@ {}} - $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\ - \hspace{3cm}Bob controls Permitted $(f$, write$)$\\ - Bob says Permitted $($File, write$)$\\ - $slev($File$)$ $=$ $T\!S$\\ - $slev($Bob$)$ $=$ $S$\\ - $slev(P) < slev(S)$\\ - $slev(S) < slev(T\!S)$ - \end{tabular}\\ - \hline - Permitted $($File, write$)$ - \end{tabular} - \end{center}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Bell-LaPadula} - \small - - \begin{itemize} - \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if - \bl{$P$}'s security level is at least as high as \bl{$O$}'s. - \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if - \bl{$O$}'s security level is at least as high as \bl{$P$}'s.\medskip - - \item Meta-Rule: All principals in a system should have a sufficiently high security level - in order to access an object. - \end{itemize}\bigskip - - This restricts information flow $\Rightarrow$ military\bigskip\bigskip\pause - - Bell-LaPadula: {\bf `no read up'} - {\bf `no write down'} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\begin{tabular}{c}Principle of\\[-2mm] Least Privilege\end{tabular}} - - \begin{tikzpicture} - \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\normalsize\color{darkgray} - \begin{minipage}{10cm}\raggedright - A principal should have as few privileges as possible to access a resource. - \end{minipage}}; - \end{tikzpicture}\bigskip\bigskip - \small - - \begin{itemize} - \item Bob ($T\!S$) and Alice ($S$) want to communicate - \item[] $\Rightarrow$ Bob should lower his security level - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Biba Policy} - \small - - Data Integrity (rather than data confidentiality) - - \begin{itemize} - \item Biba: {\bf `no read down'} - {\bf `no write up'} - \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if - \bl{$P$}'s security level is lower or equal than \bl{$O$}'s. - \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if - \bl{$O$}'s security level is lower or equal than \bl{$P$}'s. - \end{itemize}\bigskip\bigskip\pause - - E.g.~Generals write orders to officers; officers write oders to solidiers\\ - Firewall: you can read from inside the firewall, but not from outside\\ - Phishing: you can look at an approved PDF, but not one from a random email\\ - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Point to Take Home} - -\begin{itemize} -\item Formal methods can be an excellent way of finding -bugs as they force the designer -to make everything explicit and thus confront dif$\!$ficult design -choices that might otherwise be fudged. -\end{itemize} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -\end{document} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: -