diff -r be35ff24cccc -r d1d07f05325a slides06.tex --- a/slides06.tex Sun Dec 09 13:00:33 2012 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,636 +0,0 @@ -\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: -