\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->{
\begin{textblock}{6}(0.3,12)
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]
\frametitle{``Real-World'' Attacks}
EMV (Europay, MasterCard, Visa) is a standard for payments by credit cards\bigskip
It consists of three phases:
\begin{enumerate}
\item card authentication phase (the terminal reads the information; signs it with a public key
and verifies the signed information)
\item cardholder authentication (PIN; terminal sends PIN to card which verifies it; it can also verify it online
with the bank)
\item transaction authorisation (the terminal asks the card to provide an authentication code for the transaction;
the code is sent to the bank for verification)
\end{enumerate}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
A Man-in-the-middle attack
\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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: