--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides07.tex Tue Nov 13 04:50:22 2012 +0000
@@ -0,0 +1,353 @@
+\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 07, King's College London, 13 November 2012}
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\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 (7)\\[-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<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}
+
+\pause\pause
+\footnotesize Gimel (Phoenician), Gamma (Greek), C and G (Latin), Gim (Arabic),\\[-2mm] ?? (Indian), Ge (Cyrillic)
+\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}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Trusted Third Party}
+
+Simple protocol for establishing a secure connection via a mutually
+trusted 3rd party (server):
+
+\begin{center}
+\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
+Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
+Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
+Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
+Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
+\end{tabular}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Encrypted 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$})
+ \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{Encryption}
+
+ \begin{itemize}
+ \item Encryption of a message\smallskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Trusted Third Party}
+
+ \begin{itemize}
+ \item Alice calls Sam for a key to communicate with Bob
+ \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
+ \item Alice sends the message encrypted with the key and the second key it recieved
+ \end{itemize}\bigskip
+
+ \begin{center}
+ \bl{\begin{tabular}{lcl}
+ $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\
+ $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+ $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\
+ $A$ sends $B$ &:& $\{m\}_{K_{AB}}$
+ \end{tabular}}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Sending Rule}
+
+ \bl{\begin{center}
+ \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F}
+ {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}}
+ \end{center}}\bigskip\pause
+
+ \bl{$P \,\text{sends}\, Q : F \dn$}\\
+ \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Trusted Third Party}
+
+ \begin{center}
+ \bl{\begin{tabular}{l}
+ $A$ sends $S$ : $\textit{Connect}(A,B)$\\
+ \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\
+ \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
+ \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
+ $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+ $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
+ $A$ sends $B$ : $\{m\}_{K_{AB}}$
+ \end{tabular}}
+ \end{center}\bigskip\pause
+
+
+ \bl{$\Gamma \vdash B \,\text{says} \, m$}?
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Challenge-Response Protocol}
+
+ \begin{itemize}
+ \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip
+ \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip
+ \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip
+ \item if \bl{$E$} receives \bl{$\{N\}_K$} from \bl{$T$} then starts engine
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Challenge-Response Protokol}
+
+ \begin{center}
+ \bl{\begin{tabular}{l}
+ $E \;\text{says}\; N$\hfill(start)\\
+ $E \;\text{sends}\; T : N$\hfill(challenge)\\
+ $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\
+ \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\
+ $T \;\text{says}\; K$\hfill(key)\\
+ $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\
+ $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\
+ \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\
+ \end{tabular}}
+ \end{center}\bigskip
+
+ \bl{$\Gamma \vdash \text{start\_engine}(T)$}?
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+