diff -r be35ff24cccc -r d1d07f05325a slides/slides06.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/slides06.tex Sun Sep 22 15:22:11 2013 +0100 @@ -0,0 +1,636 @@ +\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 06, King's College London, 29 October 2012} + +\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 (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\\ + 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{1st Week} + +\begin{itemize} +\item What are hashes and salts?\bigskip\pause +\item \ldots can be use to store securely data on a client, but +you cannot make your protocol dependent on the +presence of the data\bigskip\pause +\item \ldots can be used to store and verify passwords + +\end{itemize} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{2nd Week} + +\begin{itemize} +\item Buffer overflows\bigskip +\item choice of programming language can mitigate or even eliminate this problem +\end{itemize} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{3rd Week} + +\begin{itemize} +\item defence in depth\bigskip +\item privilege separation afforded by the OS +\end{itemize} + +\begin{center} +\begin{tikzpicture}[scale=1] + + \draw[line width=1mm] (0, 1.1) rectangle (1.2,2); + \draw (4.7,1) node {Internet}; + \draw (0.6,1.7) node {\footnotesize Slave}; + \draw[line width=1mm] (0, 0) rectangle (1.2,0.9); + \draw (0.6,1.7) node {\footnotesize Slave}; + \draw (0.6,0.6) node {\footnotesize Slave}; + \draw (0.6,-0.5) node {\footnotesize \begin{tabular}{c}unprivileged\\[-1mm] processes\end{tabular}}; + \draw (-2.7,-0.4) node {\footnotesize \begin{tabular}{c}privileged\\[-1mm] process\end{tabular}}; + + \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2); + \draw (-2.9,1.7) node {\footnotesize Monitor}; + + \draw[white] (1.7,1) node (X) {}; + \draw[white] (3.7,1) node (Y) {}; + \draw[red, <->, line width = 2mm] (X) -- (Y); + + \draw[red, <->, line width = 1mm] (-0.4,1.4) -- (-1.4,1.1); + \draw[red, <->, line width = 1mm] (-0.4,0.6) -- (-1.4,0.9); + + \end{tikzpicture} +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{4th Week} + +\begin{itemize} +\item voting\ldots has security requirements that are in tension with each other +\begin{center} +integrity vs ballot secrecy\\ +authentication vs enfranchisment +\end{center}\bigskip + +\item electronic voting makes `whole sale' fraud easier as opposed to `retail attacks' +\end{itemize} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{5th Week} + +\begin{itemize} +\item access control logic\bigskip + +\item formulas +\item judgements +\item inference rules +\end{itemize} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ +\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{ +\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{ +\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{ + \begin{frame}[c] + \frametitle{} + + Recall the following scenario: + + \begin{itemize} + \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}} + should be deleted, then this file must be deleted. + \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether + \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted. + \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}. + \end{itemize}\bigskip + + \small + \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} + \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\ + \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\ + \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\ + \end{tabular}}\medskip + + \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] + +How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip + +\begin{center} +\Large \bl{\infer{\Gamma, F\vdash F}{}} +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] + +\begin{center} +\Large +\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}} +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] + +\begin{center} +\Large +\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] + +\begin{center} +\Large +\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad +\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\ +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] + +\begin{center} +\Large +\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}} +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[t] + +I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause + +\begin{enumerate} +\item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause +\item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove +\begin{center} +\bl{$\Gamma \vdash F_2$} +\end{center}\bigskip\pause + +\item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption +\bl{$F_2$}.\bigskip +\begin{center} +\bl{$F_2, \Gamma \vdash \text{Pred}$} +\end{center} +\end{enumerate} + +\only<4>{ +\begin{textblock}{11}(1,10.5) +\bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}} +\end{textblock}} + + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] + +\begin{itemize} +\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ +\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip + +\begin{center} +\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}} +\end{center} + +\item \bl{$P$} speaks for \bl{$Q$}\smallskip\\ +\bl{$P \mapsto Q \,\dn\, \forall F. (P\,\text{says}\, F) \Rightarrow (Q \,\text{says}\,F)$}\medskip + +\begin{center} +\bl{\infer{\Gamma \vdash Q\,\text{says}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash P\,\text{says}\,F}} +\medskip\\ +\bl{\infer{\Gamma \vdash P\,\text{controls}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash Q\,\text{controls}\,F}}\\ + +\end{center} +\end{itemize} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Protocol Specifications} + +The Needham-Schroeder Protocol: + +\begin{center} +\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} +Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B, N_A$}\\ +Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\ +Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}, A\}_{K_{BS}} $}\\ +Message 4 & \bl{$B \rightarrow A :$} & \bl{$\{N_B\}_{K_{AB}}$}\\ +Message 5 & \bl{$A \rightarrow B :$} & \bl{$\{N_B-1\}_{K_{AB}}$}\\ +\end{tabular} +\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{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$}) + \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{Public/Private Keys} + + \begin{itemize} + \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip + \begin{center} + \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} + {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} & + \Gamma \vdash K_{Bob}^{priv}}}} + \end{center}\bigskip\pause + + \item this is {\bf not} a derived rule! + \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}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: +