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

\usepackage{proof}

\usepackage{beamerthemeplaincu}

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

\usetikzlibrary{shapes}

\usepackage{graphicx} 

\setmonofont[Scale=MatchLowercase]{Consolas}

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

\newcommand{\isaliteral}[1]{}

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

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

%sudoku

\newcounter{row}

\newcounter{col}

\newcommand\setrow[9]{

        \setcounter{col}{1}

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

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

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

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

            \stepcounter{col}

        }

        \stepcounter{row}

}

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

% beamer stuff 

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

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

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}<1>[t]

\frametitle{%

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

  \\

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

  \LARGE Privacy Policies (6)\\[-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\\

  Office: & S1.27 (1st floor Strand Building)\\

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

  \end{tabular}

  \end{center}

\end{frame}}

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

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

  Formulas

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

  \end{itemize}

Judgements

\begin{itemize}

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

\end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Judgements}

\begin{center}

\begin{tikzpicture}[scale=1]

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

  \onslide<2->{

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

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

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

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

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

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

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

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

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

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

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

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

  \end{tikzpicture}

\end{center}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Inference Rules}

\begin{center}

\begin{tikzpicture}[scale=1]

  \draw (0.0,0.0) node 

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

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

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

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

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

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

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

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

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

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

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

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

  \end{tikzpicture}

\end{center}

\only<2>{

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

\small

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

\end{textblock}}

\only<3>{

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

\small

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

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

\end{textblock}}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Inference Rules}

\begin{center}

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

\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_1}}

\qquad

\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\

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

\bl{\infer{\Gamma \vdash P \,\text{says}\, F_2}

              {\Gamma \vdash P \,\text{says}\, (F_1\Rightarrow F_2) \quad 

               \Gamma \vdash P \,\text{says}\, F_1}}

\end{center}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Sending Messages}

  \begin{itemize}

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

  \begin{center}

  \bl{Alice says $m$}

  \end{center}\medskip\pause

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

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

  \begin{center}

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

  \end{center}\medskip\pause

  \item Decryption of Alice's message\smallskip

  \begin{center}

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

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

  \end{center}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Proofs}

\begin{center}

\bl{

\infer{\Gamma \vdash F}

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

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

               &

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

           }}

}

\end{center}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{The Access Control Problem}

\begin{center}

  \begin{tikzpicture}[scale=1]

  \draw[line width=1mm] (-.3, -0.5) 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}provable/\\not provable\end{tabular}};

  \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\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<presentation>{

\begin{frame}[c]

\frametitle{Proofs}

\begin{center}

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

\end{center}

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

goal

\end{textblock}

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

start

\end{textblock}

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

\begin{center}

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

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

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

\end{center}

\end{textblock}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Sudoku}

\begin{tikzpicture}[scale=.5]

  \begin{scope}

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

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

    \setcounter{row}{1}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  \end{scope}

  \end{tikzpicture}

\small

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

\begin{enumerate}

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

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

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

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

\end{enumerate}

\end{textblock}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Solving Sudokus}

\begin{tikzpicture}[scale=.5]

  \begin{scope}

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

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

    \setcounter{row}{1}

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

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

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

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

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

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

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

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

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

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

  \end{scope}

  \end{tikzpicture}

\small

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

{\bf single position rules}\\

\begin{center}

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

\end{center}

\onslide<2->{

\begin{center}

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

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

\end{center}}

\end{textblock}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Solving Sudokus}

\begin{tikzpicture}[scale=.5]

  \begin{scope}

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

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

    \setcounter{row}{1}

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

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

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

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

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

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

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

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

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

  \end{scope}

  \end{tikzpicture}

\small

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

{\bf candidate rules}\\

\begin{center}

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

\end{center}

\end{textblock}