\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} 

\usetikzlibrary{shapes}

\usetikzlibrary{shadows}

\usetikzlibrary{plotmarks}

\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 08, King's College London, 20 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 (8)\\[-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{Last Week}

Andrew Secure RPC Protocol:

\bl{$A$} and \bl{$B$} share a key \bl{$K_{AB}$} and want to identify

each other\bigskip

 \begin{itemize}

 \item \bl{$A \,\text{sends}\, B :  A, N_A$} 

 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$}

 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$}

 \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

  \frametitle{Protocols}

\mbox{} 

\begin{tabular}{l}

{\Large \bl{$A\;\text{sends}\; B : \ldots$}}\\

\onslide<2->{\Large \bl{$B\;\text{sends}\; A : \ldots$}}\\

\onslide<2->{\Large \;\;\;\;\;\bl{$:$}}\bigskip

\end{tabular}  

 \begin{itemize}

 \item by convention \bl{$A$}, \bl{$B$} are named principals \bl{Alice\ldots}\\

 but most likely they are programs, which just follow some instructions\bigskip

\item<2-> indicates one ``protocol run'', or session,  which specifies some 

order in the communication

\item<2-> there can be several sessions in parallel (think of wifi routers) 

\end{itemize} 

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Last Week}

\bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify

each other\bigskip

 \begin{itemize}

 \item \bl{$A \,\text{sends}\, B :  A, N_A$} 

 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$}

 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$}

 \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Defeating Challenge-Response}

\noindent

A \alert{reflection attack}: an intruder \bl{$I$} impersonates \bl{$B$}.

\begin{center}

\begin{tabular}{@{\hspace{-7mm}}c@{\hspace{1mm}}c@{}}

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

\onslide<1->{\bl{$A \,\text{sends}\, I :  A, N_A$}}\\ 

\onslide<4->{\bl{$I \,\text{sends}\, A :  \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ 

\onslide<5->{\bl{$A \,\text{sends}\, I : \{N_A\}_{K'_{AB}}$}}\\

\end{tabular}

&

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

\onslide<2->{\bl{$I \,\text{sends}\, A :  B, N_A$}}\\ 

\onslide<3->{\bl{$A \,\text{sends}\, I :  \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ 

\onslide<6->{\bl{$I \,\text{sends}\, A : \{N_A\}_{K'_{AB}}$}}\\

\end{tabular}

\end{tabular}

\end{center}\bigskip

\onslide<7->{Sounds stupid: ``\ldots answering a question with a counter question''\medskip\\

was originally developed at CMU for terminals to connect to 

workstations (e.g.~file servers)}

  \end{frame}}

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%         

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Identify Friend or Foe}

\begin{center}

\onslide<2->{\mbox{}\hspace{3.4cm}\includegraphics[scale=0.55]{pics/MigInMiddle.jpg}}

\end{center}

\begin{textblock}{6}(0.3,2)

198?: war between Angola (supported by Cuba)

and Namibia (supported by SA)

\end{textblock}

\begin{textblock}{3}(12.5,4.6)

  \onslide<2->{

  \begin{tikzpicture}

  \node at (0,0) [single arrow, fill=red,text=white, rotate=-50, shape border rotate=180]{``bystander''};

  \end{tikzpicture}}

  \end{textblock}

\begin{textblock}{3}(10.9,10)

  \onslide<2->{

  \begin{tikzpicture}

  \node at (0,0) [single arrow, fill=red,text=white, rotate=-40, shape border rotate=180]{attacker};

  \end{tikzpicture}}

  \end{textblock}

\only<3->{

being outsmarted by Angola/Cuba

ended SA involvement

\end{textblock}}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Encryption to the Rescue?}

 \begin{itemize}

 \item \bl{$A \,\text{sends}\, B :  \{A, N_A\}_{K_{AB}}$}\hspace{1cm} encrypted\bigskip 

 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$}\bigskip

 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$}\bigskip

 \end{itemize}\pause

means you need to send a separate ``Hello'' signal (bad), or worse 

share a single key between many entities

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Protocol Attacks}

\begin{itemize}

\item replay attacks

\item reflection attacks

\item man-in-the-middle attacks

\item timing attacks

\item parallel session attacks

\item binding attacks (public key protocols)

\item changing environment / changing assumptions

\end{itemize}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Replay Attacks}

Schroeder-Needham protocol: exchange of a symmetric key with a trusted 3rd-party \bl{$S$}: 

\begin{center}

\begin{tabular}{r@ {\hspace{1mm}}l}

\bl{$A \rightarrow S :$} & \bl{$A, B, N_A$}\\

\bl{$S \rightarrow A :$} & \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\

\bl{$A \rightarrow B :$} & \bl{$\{K_{AB}, A\}_{K_{BS}} $}\\

\bl{$B \rightarrow A :$} & \bl{$\{N_B\}_{K_{AB}}$}\\

\bl{$A \rightarrow B :$} & \bl{$\{N_B-1\}_{K_{AB}}$}\\

\end{tabular}

\end{center}\bigskip\pause

at the end both \bl{$A$} and \bl{$B$} should be in the possession of the secret key

\bl{$K_{AB}$} and know that the other principal has the key

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\begin{center}

\begin{tabular}{l}

\bl{$A \rightarrow S :$} \bl{$A, B, N_A$}\\

\bl{$S \rightarrow A :$} \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\

\bl{$A \rightarrow B :$} \bl{$\{K_{AB}, A\}_{K_{BS}} $}\\

\bl{$B \rightarrow A :$} \bl{$\{N_B\}_{K_{AB}}$}\\

\bl{$A \rightarrow B :$} \bl{$\{N_B-1\}_{K_{AB}}$}\pause\\

\hspace{5cm}compromise \bl{$K_{AB}$}\pause\\

\bl{$A \rightarrow S :$} \bl{$A, B, N'_A$}\\

\bl{$S \rightarrow A :$} \bl{$\{N'_A, B, K'_{AB},\{K'_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\pause\\

\bl{$I(A) \rightarrow B :$} \bl{$\{K_{AB}, A\}_{K_{BS}} $}\hspace{0.5cm} replay of older run\pause\\

\bl{$B \rightarrow I(A) :$} \bl{$\{N'_B\}_{K_{AB}}$}\\

\bl{$I(A) \rightarrow B :$} \bl{$\{N'_B-1\}_{K_{AB}}$}\

\end{tabular}

\end{center}\pause

\bl{$B$} believes it is following the correct protocol,

intruder \bl{$I$} can form the correct response because it knows \bl{$K_{AB}$} and

talk to \bl{$B$} masquerading as \bl{$A$}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Replay Attacks}

Andrew Secure RPC protocol: exchanging a new key

between \bl{$A$} and \bl{$B$}

\begin{center}

\begin{tabular}{l}

\bl{$A \rightarrow B :$} \bl{$A, \{N_A\}_{K_{AB}}$}\\

\bl{$B \rightarrow A :$} \bl{$\{N_A+1, N_B\}_{K_{AB}}$}\\

\bl{$A \rightarrow B :$} \bl{$\{N_B+1\}_{K_{AB}}$}\\

\bl{$B \rightarrow A :$} \bl{$\{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\\

\end{tabular}

\end{center}\bigskip\pause

Assume nonces are represented as bit-sequences of the same length

\begin{center}

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

\bl{$A \rightarrow B :$} \bl{$A, \{N_A\}_{K_{AB}}$}\\

\bl{$B \rightarrow A :$} \bl{$\{N_A+1, N_B\}_{K_{AB}}$}\\

\bl{$A \rightarrow I(B) :$} \bl{$\{N_B+1\}_{K_{AB}}$}\hspace{0.5mm}intercepts\\

\bl{$I(B) \rightarrow A :$} \bl{$\{N_A+1, N_B\}_{K_{AB}}$}\hspace{0.5mm}resend 2nd msg\\

\end{tabular}

\end{center}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Binding Attacks}

with public-private keys it is important that the public key is \alert{bound} 

to the right owner (verified by a certification authority \bl{$CA$})

\begin{center}

\begin{tabular}{l}

\bl{$A \rightarrow CA :$} \bl{$A, B, N_A$}\\

\bl{$CA \rightarrow A :$} \bl{$CA, \{CA, A, N_A, K^{pub}_{B}\}_{K^{pub}_{A}}$}\\

\end{tabular}

\end{center}\bigskip

\bl{$A$} knows \bl{$K^{prig}_A$} and can verify the message came from \bl{$CA$}

in response to \bl{$A$}'s message and trusts \bl{$K^{pub}_{B}$} is \bl{$B$}'s public key

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Binding Attacks}

\begin{center}

\begin{tabular}{l}

\bl{$A \rightarrow I(CA) :$} \bl{$A, B, N_A$}\\

\bl{$I(A) \rightarrow CA :$} \bl{$A, I, N_A$}\\

\bl{$CA \rightarrow I(A) :$} \bl{$CA, \{CA, A, N_A, K^{pub}_{I}\}_{K^{pub}_{A}}$}\\

\bl{$I(CA) \rightarrow A :$} \bl{$CA, \{CA, A, N_A, K^{pub}_{I}\}_{K^{pub}_{A}}$}\\

\end{tabular}

\end{center}\pause

\bl{$A$} now encrypts messages for \bl{$B$} with the public key of \bl{$I$}

(which happily decrypts them with its private key)

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\begin{itemize}

\item the card only says yes or no to the terminal if the PIN is correct

\item trick the card in thinking transaction is verified by signature

\item trick the terminal in thinking the transaction was verified by PIN

\end{itemize}

\begin{minipage}{1.1\textwidth}

\begin{center}

\mbox{}\hspace{-6mm}\includegraphics[scale=0.5]{pics/chip-attack.png}

\includegraphics[scale=0.3]{pics/chipnpinflaw.png}

\end{center}

\end{minipage}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Problems with EMV}

\begin{itemize}

\item it is a wrapper for many protocols

\item specification by consensus (resulted unmanageable complexity)

\item its specification is 700 pages in English plus 2000+ pages for testing, additionally some 

further parts are secret

\item other attacks have been found

\item one solution might be to require always online verification of the PIN with the bank

\end{itemize}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%