# HG changeset patch # User Christian Urban # Date 1352782222 0 # Node ID 8d3c4efb91b3ba202adcde5090ed7e01eb0f8116 # Parent d53d7d61f37b9182937667705eaca1e2c10435aa added diff -r d53d7d61f37b -r 8d3c4efb91b3 programs/prove1.scala --- a/programs/prove1.scala Tue Nov 13 00:22:28 2012 +0000 +++ b/programs/prove1.scala Tue Nov 13 04:50:22 2012 +0000 @@ -115,4 +115,4 @@ run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email)) -// consider the cases for true and false + diff -r d53d7d61f37b -r 8d3c4efb91b3 slides07.pdf Binary file slides07.pdf has changed diff -r d53d7d61f37b -r 8d3c4efb91b3 slides07.tex --- /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{ +\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{ +\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{ +\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{ +\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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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: +