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

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

}

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

\begin{center}

\end{center}

\begin{center}

\end{center}

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

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

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

\end{frame}}

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

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

\mode<presentation>{