\documentclass {beamer}
\usepackage {mathpartir}
\usepackage [slide]{gastex}
%\usepackage[usenames,dvips]{color}
\usepackage{ifthen}
\usepackage{beamerthemesplit}
%\usepackage {pdfpages}
\usepackage{graphicx}
\usetheme{Pittsburgh}
\usecolortheme{seahorse}


\title{Proof carrying authorization in ML5}
\author{Romain Brenguier \\ % Internship report \\
  Supervisor : Frank Pfenning \\ Carnegie Mellon University}
\date{April - August 2008}

\begin{document}

%\newcommand{\node}{}
%\newcommand{\drawedge}{}


\newcommand{\mycomment}[1]{ }

% % % *******************

\maketitle

\begin{frame}
\tableofcontents
\end{frame}

\section*{Introduction}

\begin{frame}
\frametitle{Manifest security}
\begin{itemize}
\item building manifestly secure program
\pause
\item manifest by there type
\pause
\item according to access control and information flow policies
\pause
\item we begin with access control
\end{itemize}
\end{frame}

\section{Proof carrying authorization}

\subsection{Access control}
\begin{frame}
\begin{definition}[Access control]
to restrict access to resources to specific users
\end{definition}

\begin{example}[resources]
\begin{itemize}
\item File system ( -rw-r--r-- -rw-r----- )
\item Database
\item Door of an office
\end{itemize}
\end{example}

\end{frame}

\subsection{Authorization logic}

\begin{frame}
\frametitle{Authorization logic}
\begin{figure}[h]
$$
A ::=   P \,| \, A \supset A \, | \, \forall K \, A \, | \, K \textup{says} A
$$
\caption{Syntax of formulas, P denotes an arbitrary atomic formula}
\end{figure}

\pause

Judgments : \\
\begin{center}
\onslide<2>{$\Gamma \vdash A $}

\onslide<3->{
$\Gamma \vdash TRUE (A)$ \\
$\Gamma \vdash AFF (K,A)$
}
\end{center}

\end{frame}

\begin{frame}
$$
\inferrule* [Left=use]
{ }
{ \Gamma , \textsc{true} (A) \vdash \textsc{true} (A)}
$$

\pause

$$
\inferrule* [Left=impI]
{ \Gamma , \textsc{true} (A) \vdash \textsc{true} (B)}
{ \Gamma \vdash \textsc{true} (A \supset B)}
$$

%\pause

$$
\inferrule* [Left=impE]
  { \Gamma \vdash \textsc{true} (A \supset B) \\ \Gamma \vdash \textsc{true} (A) }
  { \Gamma \vdash \textsc{true} (B)}
$$
\end{frame}


\mycomment{
\begin{frame}
\small
  $$
  \inferrule*[Left=impE]
             { \inferrule*[Right=use]{ }
               {
                 \textsc{true} ( \textsc {s} \supset \textsc {m} 
                 (S, B)) \vdash \textsc{true} ( \textsc {s}  \supset \textsc {m})
               }
               \\
               \inferrule*[Right=use]{ }
                          { \textsc{true} ( \textsc {s} )
                            \vdash  \textsc{true} ( \textsc {s}) 
                          }
             }
             { \textsc{true} ( \textsc {s} (B, A) \supset \textsc {mr} 
                 (S, B)) , \textsc{true} ( \textsc {s} (B, A))
               \vdash 
               \textsc{true} ( \textsc {mr} (S, B) )
             }
             $$
\end{frame}
}

\newcommand{\infsaysi}
{
$$\inferrule* [Left=saysI]
{ \Gamma \vdash \textsc{aff} (K, A)}
{ \Gamma \vdash \textsc{true} ( K \textup{says} A) }
$$
}

\newcommand{\inftruaff}
{
$$\inferrule* [Left=truaff]
{ \Gamma \vdash \textsc{true} (A)}
{ \Gamma \vdash \textsc{aff} (K, A) }$$
}

\newcommand{\infsayse}
{
$$
\inferrule* [Left=saysE]
{ \Gamma \vdash \textsc{true} (K \textup{says} A) \\ \Gamma, \textsc{true} (A)
  \vdash \textsc{aff} (K,B)}
{ \Gamma \vdash \textsc{aff} (K, B) }
$$
}

\begin{frame}
\infsaysi{}
%\pause
\inftruaff{}
%\pause
\infsayse{}
\end{frame}



\mycomment{
\begin{frame} 
\inftruaff{}


$$
\inferrule* 
    [Left=truaff]
    {\textsc {mayrd} (Sheet, B) \vdash \textsc {mayrd} (S, B) }
    {\textsc {mayrd} (Sheet, B) \vdash \textsc{aff} (A, \textsc {mayrd} (S, B))}
$$
\end{frame}


%\begin{frame} \inftruaff{} \includegraphics[width=4.0in]{dessin0201} \end{frame}
%\begin{frame} \inftruaff{} \includegraphics[width=4.0in]{dessin0202} \end{frame}
%\begin{frame} \inftruaff{} \includegraphics[width=4.0in]{dessin0203} \end{frame}
%\begin{frame} \inftruaff{} \includegraphics[width=4.0in]{dessin0204} \end{frame}



\begin{frame}

$$
\inferrule* [Left=saysE]
{ \Gamma \vdash \textsc{true} (K \textup{says} A) \\ \Gamma, A \vdash \textsc{aff} (K,B)}
{ \Gamma \vdash \textsc{aff} (K, B) }
$$

$$
\inferrule*
    [Left=saysE]
    { \inferrule*[Left=use,rightskip=4em,leftskip=6em]
      { }{Alice \, \textup{says} \, \forall x  ( \textsc {student} ( x , Alice)  \supset \textsc {mayrd} (Sheet, x) ) \Gamma \vdash p3}
      \\ 
      \inferrule*[Left=trueaff,rightskip=4em,
        leftskip=6em,vdots=3em] 
                 {\Pi_2}
                 { \Gamma'' \vdash \textsc{aff} 
                   (Alice, \textsc {student} (Bob, Alice)
                   \supset \textsc {mayrd} (Sheet, Bob)) }
    }
    { \Gamma \vdash \textsc{aff} 
      (Alice, \textsc {student} (Bob, Alice) \supset
      \textsc {mayrd} (Sheet, Bob)) 
    }
    $$ 
%\includegraphics[width=20cm]{dessin0101.pdf} 

\end{frame}
}


\subsubsection*{Example}
%find a better one ?

\mycomment{
\begin{frame}

$$ p1 : Alice \, \textup{says} \, \textsc {maywt} ( Sheet, Alice ) $$
$$ p2 : Alice \, \textup{says} \, \textsc {mayrd} ( Sheet, Alice ) $$
$$ p3 : $$
$$ p4 : \textsc {student} (Bob, Alice) $$

$$\Gamma = p1, p2, p3, p2$$

we want to proove : $ \Gamma \vdash Alice \, \textup{says} \, \textsc{mayrd} (Sheet, Bob)$
\end{frame}
}

\mycomment{
\begin{frame}
\small
$\Gamma '' = \Gamma , 
\textsc{true} (\forall x  ( \textsc {student} ( x , Alice)  \supset \textsc {mayrd} (Sheet, x) )) $.

$$
\inferrule* 
    [Left=allpE]
    {\inferrule* [Left=use]{ }
      {\Gamma ''  \vdash \textsc{true} (
        \forall x  ( \textsc {student} ( x , Alice)  \supset \textsc {mayrd} (Sheet, x) )) }
    }
    { \Gamma '' \vdash \textsc{true} ( 
      \textsc {student} (Bob, Alice) \supset \textsc {mayrd} (Sheet, Bob) )}
    $$
\end{frame}
}


\mycomment{
\begin{frame}

$$
\inferrule* [Left=trueaff]
            {
              \inferrule* [Left=saysE]
                          {
                            \inferrule* [Left=saysI,rightskip=4em,leftskip=6em,vdots=3em]
                            % ,leftskip=2em,rightskip=2em,vdots=1.5em]
                                        { }
                                        { \Gamma \vdash \textsc{true} ( Alice \,\textup {says}
                                          \,\textsc {student} (Bob, Alice) \supset 
                                          \textsc {mayrd} (Sheet, Bob) ) }
                                        \\ \Pi_1
                          }
                          { \Gamma \vdash \textsc{aff} (Alice, \textsc {mayrd} (Sheet, Bob))}
            }
            {  \Gamma \vdash \textsc{true} (Alice \,\textup{says}\, \textsc {mayrd} (Sheet, Bob))}
            $$

\end{frame}
}

\subsection{Proof carrying authorization architecture}


\begin{frame}
\begin{block}{Proof carrying authorization}
\begin{itemize}
\item to find a proof = difficult problem
\pause
\item the principal is more likely to know why access should be granted him
\pause
\item a ressource monitor should only check proofs
\end{itemize}
\end{block}
\end{frame}

\section{ML5}

\subsection{IS5}

\begin{frame}
%explain why we are talking about logic
ML5 :
\begin{itemize}
\item distributed programming language
\pause
\item type system based on a modal logic called IS5
\end{itemize}

\pause 

\bigskip

\begin{tabular}{l l l l l l}

types & & & & & \\
$'a$ & $int$ & $A \rightarrow B $ & $A * B$ & $ (A , B) union$ & \\ %\union
propositions & & & & & \\
$\alpha$ & $true$ & $A \supset B $ & $A \wedge B$ & $ A \vee B $ & \\
\\
\end{tabular}
\pause

\begin{tabular}{l l l l l l}
terms & & & & & \\
$0, 1, x , ...$ & $ f (x) $ & $fun \, x  \rightarrow  y$ &
$(x,y)$ & $Inl \, x$ & $function \, Inr \, a \rightarrow y \, | \, Inl \, b \rightarrow z$ \\
proof terms & & & & & \\
\textsc{use} &
\textsc{impE} &
\textsc{impI} &
\textsc{$\wedge$I} &
\textsc{$\vee$ I$_1$} &
\textsc{$\vee$E} 
\end{tabular}

\end{frame}

\begin{frame}
\begin{figure}[h]
  $$ A , B ::=  p \, | \, A \supset B  \, | \, A \vee B \, | \,  A \wedge B \, | \,\Box A \, | \, \Diamond A \, | \,  \, A \, at \, w $$
\caption{Syntax of propositions in the IS5 logic}
\end{figure}

\begin{figure}[h]
$$ \Gamma \vdash A @ w $$
\caption{Judgments in the IS5 logic}
\end{figure}
\end{frame}




\begin{frame}
$$
\inferrule* [Left=\textsc{atI}]
{\Gamma \vdash A @ \textsc w}
{\Gamma \vdash A \, at \, \textsc w @ \textsc w'}
\hspace{4em}
\inferrule* [Left=\textsc{atE}]
{\Gamma \vdash A \, at \, \textsc w'' @ \textsc w' \\ \Gamma, A @ \textsc w'' \vdash B @ \textsc w}
{\Gamma \vdash B @ \textsc w}
$$

\mycomment{
$$
\inferrule* [Left=\textsc{ $ \Box $ I}]
{\Gamma , \omega \hspace{0.5em} world \vdash A  @ \omega}
{\Gamma \vdash \Box A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Box $ E}]
{\Gamma \vdash \Box A @ \textsc w}
{\Gamma \vdash A @ \textsc w'}
$$


$$
\inferrule* [Left=\textsc{ $ \Diamond $ I}]
{\Gamma \vdash A @ \textsc w'}
{\Gamma \vdash \Diamond A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Diamond $ E}]
{\Gamma \vdash \Diamond A @ \textsc w' \\
 \Gamma , \omega \hspace{0.5em} world , A @ \omega \vdash B @ \textsc w}
{\Gamma \vdash B @ \textsc w}
$$
}


\end{frame}

\mycomment{
\begin{frame}

$$
\inferrule* [Left=\textsc{ $ \Diamond $ I}]
{\Gamma \vdash A @ \textsc x}
{\Gamma \vdash \Diamond A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Diamond $ E}]
{\Gamma \vdash \Diamond A @ \textsc x \\
 \Gamma , \omega \hspace{0.5em} world , A @ \omega \vdash B @ \textsc w}
{\Gamma \vdash B @ \textsc w}
$$

\end{frame}
}

\subsection{Lambda 5 natural deduction}

\begin{frame}
\begin{figure}
$$
\Gamma \vdash M : A @ \textsc w
$$
\caption{Judgments in lambda 5 natural deduction}
\end{figure}
\end{frame}

\begin{frame}
\begin{figure}[h]
$$
\inferrule* [Left=\textsc{atI}]
{\Gamma \vdash M : A @ \textsc w}
{\Gamma \vdash \textbf{hold} M : A \, at \, \textsc w @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{atE}]
{\Gamma \vdash M : A \, at \, \textsc w' @ \textsc w \\ 
  \Gamma, A @ \textsc w' \vdash N : B @ \textsc w}
{\Gamma \vdash \textbf{leta} M \,in\, N : B @ \textsc w}
$$

\mycomment{
$$
\inferrule* [Left=\textsc{ $ \Box $ I}]
{\Gamma , \omega \hspace{0.5em} world \vdash M : A  @ \omega}
{\Gamma \vdash \textbf{box} M : \Box A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Box $ E}]
{\Gamma \vdash M : \Box A @ \textsc w}
{\Gamma \vdash \textbf{unbox} M : A @ \textsc w}
$$


$$
\inferrule* [Left=\textsc{ $ \Diamond $ I}]
{\Gamma \vdash M : A @ \textsc w}
{\Gamma \vdash \textbf{here} M : \Diamond A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Diamond $ E}]
{\Gamma \vdash M : \Diamond A @ \textsc w' \\
 \Gamma , \omega \hspace{0.5em} world , A @ \omega \vdash N : B @ \textsc w}
{\Gamma \vdash \textbf{letd} \omega , x = M  \,in\, N : B @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{ get }]
{A \textbf{mobile} \\
 \Gamma \vdash M : A @ \textsc w'}
{\Gamma \vdash \textbf{get} [w'] M : A @ \textsc w}
$$}

\caption{Lambda 5 natural deduction}
\label{fig:lambda5}
\end{figure} 
\end{frame}

\mycomment{
\begin{frame}
\begin{figure}[h]
$$
\inferrule{ \\ }{\Box \textbf{ mobile}}
\hspace{4em} \inferrule{ \\ }{\Diamond \textbf {mobile}}
$$

$$
\inferrule{A \textbf{ mobile} \\ B \textbf {mobile} } {A \vee B \textbf{ mobile}}
\hspace{4em}  \inferrule{A \textbf{ mobile} \\ B \textbf {mobile} } {A \wedge B \textbf{ mobile}}
$$

$$
\inferrule{ \\ }{A \, at \, \textsc w \textbf{ mobile} }
$$
\caption{The \textit{mobile} judgment }
\end{figure}
\end{frame}
}


\subsection{Example}

\newcommand{\red}[1]{{\color{red}#1}}
\newcommand{\dred}[1]{{\color{red!50}#1}}
\newcommand{\blue}[1]{{\color{blue}#1}}
\newcommand{\green}[1]{{\color{green}#1}}

\newcommand{\mlval}{\blue{val}}
\newcommand{\mlput}{\blue{put}}
\newcommand{\mlfrom}{\red{from}}
\newcommand{\mlget}{\red{get}}
\newcommand{\mllet}{\blue{let}}
\newcommand{\mlin}{\blue{in}}
\newcommand{\mlend}{\blue{end}}

\begin{frame}[fragile]
%\begin{figure}[h]
%\caption{A piece of ML5 source code}
%\label{fig:ml5code}
%\begin{verbatim}
%\begin{left}
\mlput \verb! checked_sig = ! \mlfrom \verb! server ! \mlget \verb! hold (checksig sig) ! \\
\mlval \verb! _ = ! \\
\verb!  ! \mlfrom \verb! server ! \mlget \\
\verb!    ! \mllet \verb! ! \red{leta}  \verb! cs = checked_sig!\\
\verb!    ! \mlin  \\
\verb!    ! \blue{case}  \verb! cs ! \blue{of} \\
\verb!      !  \verb!NONE => ! \mlfrom  \verb! home ! \\ 
\verb!        ! \mlget \verb! setstring ([! \dred {you are not logged in}  \verb!])! \\
\verb!      !  \verb!| (SOME log) => ! \mlfrom  \verb! home ! \\ 
\verb!        ! \mlget  \verb! setstring ([! \dred{OK} \verb!])! \\
\verb!    ! \mlend
%\end{verbatim}
%\end{left}
%\end{figure}
\end{frame}



\begin{frame}
\begin{example}
wiki application :
\begin{itemize}
\item source parsing : client side
\item database writing and reading : server side
\end{itemize}
\end{example}
% talk about the implementation of the wiki
\end{frame}

\section{PCML5}

\subsection{Architecture}
\begin{figure}[htp]
\begin{center} 
\includegraphics[width=6.0in]{dessin_architecture}
\end{center}

\label{PCML5 architecture}
\end{figure}



\subsection{Introduction}
\begin{frame}
\begin{tabular}{l l l l l l}
\onslide<6-> {kinds :} & & & & &  \\
\onslide<7->{TYPE} & \onslide<7->{PROP} & \onslide<8->{TRUE(P)} & \onslide<8-> {AFF(K,P)} & \onslide<7->{...} & \\
& & & & &  \\
\onslide<2-> {types :} & & & \onslide<4-> {propositions :} & &  \\
\onslide<3->{int} & \onslide<3->{ $'a \rightarrow 'a$ } & \onslide<3->{...} 
 & \onslide<5->{$ \textup{mayrd}(K,A)$ } & \onslide<5->{ $A \supset B$ } &
\onslide<5->{...} \\
& & & & &  \\
terms : & & & & & \\
\onslide<1-> {0 1 ... } & \onslide<1-> {fun x $\rightarrow$ y} & \onslide<1->{(f 101010)} &
\onslide<1->{ ... } & & 
\end{tabular}
\end{frame}

\mycomment{
\subsection{Authorization logic}
\begin{frame}
\begin{table}[h]
\begin{tabular}{l c l}
  $A$ & $ ::= $ & $ \textup {mayrd} (R , K) $ $|$ $ \textup{maywt} (R , K) $ \\
  & $|$ &  $\langle K \rangle A$ $|$ $A \supset A $ $|$ $\forall_p A$ $|$ $\forall_r A$ \\
\end{tabular}
  \caption{Syntax for propositions}
\end{table}
\end{frame}
}
\subsection{Syntax of the language}

\begin{frame}
\begin{table}[H]
  \begin{tabular}{l l c l}
    Kinds & $ L $ & $::= $ & $\textsc{type}$ $|$ $\textsc{world}$  \\
    & & $ | $ & $\textsc{database}$ $|$ $\textsc{principal}$ $|$ $\textsc{prop}$ \\
    & & $ | $ & $\textsc{true(A)}$ $|$ $\textsc{aff(K,A)}$ 
    % $|$ $\Pi \alpha :: K . K$ \\
  \end{tabular}
\end{table}
\end{frame}

\begin{frame}
\begin{table}[H]
  \begin{tabular}{l l c l}
    Constructors & $A$ & $ ::= $ & $\alpha$ $|$ $K$ $|$ $W$ $|$ $A \rightarrow A$ $|$ $A \wedge A$ $|$ $A \vee A $ \\
    & & $ | $ & $\Box A$ $|$ $\Diamond A $ $|$ $A @ W$ \\
   % & & $ | $ & $(N A)$ \\
    \\
    & & $ | $ & handle $(A)$ $|$ identity $(K)$ \\
    \\
    (Propositions) & & $ | $ &  mayrd$(A,K)$ $|$ maywt$(A,K)$ \\
    & & $ | $ & $ \langle K \rangle A$  $|$ $A \supset A$ $|$ $\forall_p \alpha A$ $|$ $\forall_r \alpha A$ \\
\\
    (Proof terms) & & $ | $ & truaff$(A,K,A)$ $|$ saysI$(K,A,A)$  \\
    & & $|$ & saysE$(A,A,A)$  $|$ impI$(A,A,A)$ \\
    & & $|$ & impE$(A,A)$ $|$ allpI$(A,A)$  \\
    & & $|$ & allpE$(A,A)$ \\
    & & $|$ & allrI$(A,A)$ $|$ allrE$(A,A)$ \\
\\
    & & $|$ & $\forall \alpha :: L . A$
%    \\
%    Normal constructors & $A$ & $ ::= $ & $ N$ $|$ $\forall \alpha :: L . A$
  \end{tabular}
\end{table}
\end{frame}

\begin{frame}
\begin{table}[H]
  \begin{tabular}{l l c l}
    Terms & $M$ & $::=$ & $x$ $|$ $\lambda x : A . M$ $|$ $M_1 M_2$ $|$ $\langle M_1 , M_2 \rangle$ \\
    & & $|$ & $\#_1 M $ $|$ $\#_2 M $ $|$ inl $M$ $|$ inr $M$ $|$ 
    case $M$ $ \{ x . M_1 | x . M_2 \}$ \\
    & & $|$ & hold $(M)$ $|$ leta $x$ = $M$ in $M$ $|$ box $\alpha$ . $M$ $|$ unbox $M$\\
    & & $|$ & here $(M)$ $|$ letd $x,\alpha$ = $M$ in $M$ $|$ get [$A$] $M$ \\
%    & & $|$ & read [$A$,$A$,$A$] $|$ write [$A$,$A$,$A$] ($M$) \\
    & & $|$ & $(M N)$ \\
    & & $|$ & $\textup{acquire\_cert}$ [$A$] $\{ \alpha . M  | M \}$ \\
    & & $|$ & $\textup{poly\_app}$ $M$ $\{A\}$
  \end{tabular}
\end{table}
\end{frame}


\begin{frame}[fragile]

\begin{eqnarray*}
\textup{read} : \forall d :: \textsc{database} \, \forall p :: \textsc {principal} \,
\forall t :: \textsc{true} (\textsc{mayrd} (d,p) ) \,\\ 
\textup{handle}(d)  \rightarrow \textup{identity}(p)
 \rightarrow \textup{string}
\end{eqnarray*}

\pause
\begin{verbatim}
extern val (d:database , p:principal , 
    prf : TRUE mayrd d p) read : 
      d dbhandle -> p identity -> string @ server

extern val (d:database , p:principal , 
    prf : TRUE maywt d p) write : 
     d dbhandle -> p identity -> string -> unit @ server
\end{verbatim}
\end{frame}




\begin{frame}
$$
\inferrule
{ \Delta , \alpha :: \textsc{true} (A) ; \Gamma \vdash M_1 : A' @ l \\ 
  \Delta ; \Gamma \vdash M_2 : A' @ l}
{ \Delta ; \Gamma \vdash \textup{acquire\_cert} [A] \{\alpha . M_1 | M_2\} : A' @ l }
$$
\end{frame}

\begin{frame}
$$
\inferrule
{ \Delta , \Gamma \vdash M : \forall L A' @ l \\ 
  \Delta \vdash A :: L }
{ \Delta ; \Gamma \vdash \textup{poly\_app} M \{A\} : A' @ l }
$$
\end{frame}


\section{Application}




\section*{Conclusion}

\begin{frame}
What is missing :
\begin{itemize}
\item primitives to sign certificates
\item complete the implementation
\item build some example applications
\end{itemize}
\end{frame}

\begin{frame}
Questions?
\end{frame}



\appendix



\begin{frame}
$$
\inferrule* [Left=allpI*]
{ \Gamma \vdash \textsc{true} (A)}
{\Gamma \vdash \textsc{true} (\forall x A)}
$$

* side condition : x must not occur in $\Gamma$


$$
\inferrule* [Left=allpE]
{ \Gamma \vdash \textsc{true} (\forall x A)}
{ \Gamma \vdash \textsc{true} (A[x \leftarrow K])}
$$

\end{frame}


\begin{frame}
% rules for ``and''
$$
\inferrule* [Left=\textsc{$\wedge$ I}]
{\Gamma \vdash A @ \textsc w \\ \Gamma \vdash B @ \textsc w }
{\Gamma \vdash A \wedge B @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\wedge \textsc E_1$}]
{\Gamma \vdash A \wedge B @ \textsc w }
{\Gamma \vdash A @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\wedge \textsc E_2$}]
{\Gamma \vdash A \wedge B @ \textsc w}
{\Gamma \vdash B @ \textsc w}
$$

% rules for ``or''
$$
\inferrule* [Left=\textsc{$\vee \textsc I_1$}]
{\Gamma \vdash A @ \textsc w}
{\Gamma \vdash A \vee B @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\vee \textsc I_2$}]
{\Gamma \vdash B @ \textsc w}
{\Gamma \vdash A \vee B @ \textsc w }
$$
\end{frame}

\begin{frame}
$$
\inferrule* [Left=\textsc{$\vee \textsc E$}]
{\Gamma \vdash A \vee B @ \textsc w' \\ 
  \Gamma , A @ \textsc w' \vdash  C @ \textsc w \\
  \Gamma , B @ \textsc w' \vdash C @ \textsc w}
{\Gamma \vdash C @ \textsc w}
$$
% rules for implication
$$
\inferrule* [Left=\textsc{$\supset \textsc I$}]
{\Gamma, A @ \textsc w \vdash B @ \textsc w }
{\Gamma \vdash A \supset B @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\supset \textsc E$}]
{\Gamma \vdash A \supset B @ \textsc w \\ \Gamma \vdash A @ w}
{\Gamma \vdash B @ \textsc w }
$$

$$
\inferrule* [Left=\textsc{ hyp}]
{ }
{\Gamma, A @ \textsc w, \Gamma' \vdash A @ \textsc w}
$$
\end{frame}

\begin{frame}
$$
\inferrule* [Left=\textsc{$\supset \textsc E$}]
{\Gamma \vdash A \supset B @ \textsc w \\ \Gamma \vdash A @ w}
{\Gamma \vdash B @ \textsc w }
$$
\end{frame}


\begin{frame}
\begin{figure}[h]

$$
\inferrule*
{ }
{ \Delta , x :: \textsc {true} (A) \vdash x :: \textsc {true} (A)}
$$

$$
\inferrule*
{ \Delta , x :: \textsc {true} (A) \vdash y :: \textsc {true} (B)}
{ \Delta \vdash \textsc{impI} (x, A, y) :: \textsc{true} (A \supset B)}
$$

$$
\inferrule*
  { \Delta \vdash x :: \textsc {true} (A \supset B) \\ \Delta \vdash y :: \textsc {true} (A) }
  { \Delta \vdash \textsc{impE} (x, y) :: \textsc {true} (B)}
$$
\end{figure}
\end{frame}

\begin{frame}
\begin{figure}[h]
$$
\inferrule*
{ \Delta \vdash y :: \textsc {true} (A)}
{ \Delta \vdash \textsc{allpI} (x, y) :: \textsc {true} (\forall_p x . A)}
$$

$$
\inferrule*
{ \Delta \vdash y :: \textsc {true} (\forall_p x . A) \\ \Delta \vdash K :: \textsc {principal} }
{ \Delta \vdash \textsc{allpE} (y,K) :: \textsc {true} (A[x \leftarrow_p K])}
$$



\mycomment{
$$
\inferrule*
{ \Delta \vdash y :: \textsc {true} (A) }
{ \Delta \vdash \textsc{allrI} (x, y) :: \textsc {true} (\forall_r x . A)}
\hspace {2em}
\inferrule*
{ \Delta \vdash y :: \textsc {true} (\forall_p x  . A) \\ \Delta \vdash D :: \textsc{database} }
{ \Delta \vdash \textsc{allrE} (y ,\alpha) :: \textsc {true} ( A[x \leftarrow_r D]) }
$$
}

\end{figure}
\end{frame}


\begin{frame}
\begin{figure}
$$\inferrule*
{ \Delta \vdash x :: \textsc{aff} (K, A)}
{ \Delta \vdash \textsc{saysI} (K, A, x) :: \textsc{true} ( K \textup{says} A) }
$$

$$
\inferrule*
{ \Delta \vdash x ::  \textsc{true} (A)}
{ \Delta \vdash \textsc{truaff} (A ,K, x) :: \textsc{aff} (K, A) }
$$

$$
\inferrule*
{ \Delta \vdash x :: \textsc{true} (K \textup{says} A) \\ \Delta, \alpha :: A \vdash y :: \textsc{aff} (K,B)}
{ \Delta \vdash \textsc{saysE} (\alpha, x ,y) :: \textsc{aff} (K, B) }
$$
\caption{Proof terms}
\end{figure}
\end{frame}

\mycomment{
\begin{frame}
\begin{figure}[H]
\caption{Instantiation rules}
\label{fig:instantiation}

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {database} . T \\ \Delta \vdash D :: \textsc {database} }
{ \Delta \vdash (M D) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {principal} . T \\ \Delta \vdash P :: \textsc {principal} }
{ \Delta \vdash (M P) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {proposition} . T \\ \Delta \vdash P :: \textsc {proposition} }
{ \Delta \vdash (M P) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {true}(A) . T \\ \Delta \vdash P :: \textsc {true}(A) }
{ \Delta \vdash (M P) : T }
$$

$$
\inferrule
{ \Delta \vdash M : \forall x :: \textsc {aff}(K,A) . T \\ \Delta \vdash P :: \textsc {aff}(K,A) }
{ \Delta \vdash (M P) : T }
$$
\end{figure}
\end{frame}
}



\begin{frame}
\begin{figure}[h]
\caption{Kinds}

$$
\inferrule{ } { \Delta \vdash \textsc{type} \, \textup{kind}}
\hspace{4em}
\inferrule{ } { \Delta \vdash \textsc{world} \,\textup{kind}}
$$

$$
\inferrule{ } { \Delta \vdash \textsc{database}\, \textup{kind}}
\hspace{4em}
\inferrule{ } { \Delta \vdash \textsc{principal} \,\textup{kind}}
\hspace{4em}
\inferrule{ } { \Delta \vdash \textsc{proposition} \,\textup{kind}}
$$

$$
\inferrule{  \Delta \vdash A :: \textsc{proposition} } { \Delta \vdash \textsc{true} (A) \,\textup{kind}}
\hspace{4em}
\inferrule{  \Delta \vdash A :: \textsc{proposition} \\  \Delta \vdash K :: \textsc{principal} }
          { \Delta \vdash \textsc{aff}(K,A) \, \textup{kind}}
$$
\end{figure}
\end{frame}



\begin{frame}
\begin{figure}[h]
\caption{Types}

$$
\inferrule{ \Delta \vdash P :: \textsc{principal}}
{ \Delta \vdash \textup{identity}(P) :: \textsc{type} }
\hspace{4em}
\inferrule{ \Delta \vdash D :: \textsc{database}}
{ \Delta \vdash \textup{handle}(D) :: \textsc{type} }
$$

$$
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash B :: \textsc{type}}
          {\Delta \vdash A \rightarrow B :: \textsc{type}}
$$

$$
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash B :: \textsc{type}}
          {\Delta \vdash A \wedge B :: \textsc{type}}
\hspace{4em}
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash B :: \textsc{type}}
          {\Delta \vdash A \vee B :: \textsc{type}}
$$

$$
\inferrule{\Delta \vdash A :: \textsc{type} }
          {\Delta \vdash \Box A :: \textsc{type}}
\hspace{4em}
\inferrule{\Delta \vdash A :: \textsc{type} }
          {\Delta \vdash \Diamond A :: \textsc{type}}
\hspace{4em}
\inferrule{\Delta \vdash A :: \textsc{type} \\ \Delta \vdash W :: \textsc{world}}
          {\Delta \vdash A @ W :: \textsc{type}}
$$
\end{figure}
\end{frame}


\begin{frame}
\begin{figure}[H]
\caption{Propositions}
$$
\inferrule{\Delta \vdash D :: \textsc{database} \\ \Delta \vdash K :: \textsc{principal}}
          {\Delta \vdash \textup{mayrd}(D,K) :: \textsc{proposition}}
$$

$$
\inferrule{\Delta \vdash D :: \textsc{database} \\ \Delta \vdash K :: \textsc{principal}}
          {\Delta \vdash \textup{maywt}(D,K) :: \textsc{proposition}}
$$

$$
\inferrule{\Delta \vdash K :: \textsc{principal} \\ \Delta \vdash P :: \textsc{proposition}}
          {\Delta \vdash \langle K \rangle P :: \textsc{proposition}}
$$

$$
\inferrule{\Delta \vdash A :: \textsc{proposition} \\ \Delta \vdash B :: \textsc{proposition}}
          {\Delta \vdash A \supset B :: \textsc{proposition}}
$$

$$
\inferrule{ \Delta , x :: \textsc{principal} \vdash A :: \textsc{proposition} }
          { \Delta \vdash \forall_p x \, A :: \textsc{proposition}}
\hspace{4em}
\inferrule{ \Delta , x :: \textsc{database} \vdash A :: \textsc{proposition} }
          { \Delta \vdash \forall_r x \, A :: \textsc{proposition}}
$$
\end{figure}
\end{frame}



\subsection*{Example : grade sheet}
\begin{frame}
$$ p1 : \textsc {maywt} ( gradedb , Alice ) $$
$$ p2 : \textsc {mayrd} ( gradedb , Alice ) $$
$$ p3 : \textsc {mayrd} ( gradedb , Bob ) $$
\end{frame}

\begin{frame}[fragile]
\begin{verbatim}
extern database gradedb
principal user

val cookie = webiso ()
val id = checksig {user} cookie
val gradehandle = gethandle {gradedb} ()

val _ = match (id,gradehandle) with
   (SOME id, SOME gradehandle) =>
       acquire_cert{mayrd gradedb user}
       then p1 .
           acquire_cert{maywt gradedb user}
             then p2 . edit {user,gradedb,p1,p2,id,gradehandle} ()
             else display {user,gradedb,p1,id,gradehandle} ()
       else ()
   | _ => ()
}
\end{verbatim}

\end{frame}

\begin{frame}[fragile]
\begin{verbatim}
val (u:principal,db:database,
     p1:TRUE mayrd db u, p2:TRUE maywt db u,
     id: u identity, h: db handle) edit : unit -> unit
val (u:principal,db:database,
     p1:TRUE mayrd db u,
     id: u identity, h: db handle) display : unit -> unit
\end{verbatim}

\begin{verbatim}
val grades = read {db,u,p1} h id
\end{verbatim}
\end{frame}

\end{document}
