\documentclass[dvipsnames,14pt,t]{beamer}

\usepackage{proof}

\usepackage{beamerthemeplaincu}

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

\setmonofont{Consolas}

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

\newcommand{\isaliteral}[1]{}

\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}

\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

\makeatletter

\lst@CCPutMacro\lst@ProcessOther {"2D}{\lst@ttfamily{-{}}{-{}}}

\@empty\z@\@empty

\makeatother

\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]"""

}

\lstdefinelanguage{while}{

  morekeywords={while, if, then. else, read, write},

  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 05, King's College London, 29 October 2013}

\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 (5)\\[-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\\

  Office: & S1.27 (1st floor Strand Building)\\

  Slides: & KEATS (also homework is there)\\

  \end{tabular}

  \end{center}

\end{frame}}

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

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

  \mode<presentation>{

  \begin{frame}[t]

  \frametitle{Last Week}

\mbox{} 

\begin{tabular}{l}

{\Large \bl{$A\;\rightarrow\; B : \ldots$}}\\

\onslide<1->{\Large \bl{$B\;\rightarrow\; A : \ldots$}}\\

\onslide<1->{\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

\item indicates one ``protocol run'', or session,  which specifies an 

order in the communication

\item there can be several sessions in parallel (think of wifi routers) 

\item nonces (randomly generated numbers) used only once 

\end{itemize} 

  \end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Cryptographic Protocol Failures}

Ross Anderson and Roger Needham wrote:\bigskip

\begin{quote}

\textcolor{gray}{

A lot of the recorded frauds were the result of this kind of blunder, or from 

management negligence pure and simple.} However, there have been a 

significant number of cases where the designers protected the right things, 

used cryptographic algorithms which were not broken, and yet found that their 

systems were still successfully attacked. 

\end{quote}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Protocols}

Examples where ``over-the-air'' protocols are used

\begin{itemize}

\item wifi

\item card readers (you cannot trust the terminals)

\item RFI (passports)

\end{itemize}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\begin{center}

\includegraphics[scale=0.5]{pics/dogs.jpg}

\end{center}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}Chip-and-PIN\end{tabular}}

\begin{itemize}

\item A ``tamperesitant'' terminal playing Tetris on 

\textcolor{blue}{\href{http://www.youtube.com/watch?v=wWTzkD9M0sU}{youtube}}.\\

\textcolor{lightgray}{\footnotesize(\url{http://www.youtube.com/watch?v=wWTzkD9M0sU})}

\end{itemize}

\includegraphics[scale=0.2]{pics/tetris.jpg}

\end{frame}}

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

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

  \mode<presentation>{

  \begin{frame}<1-3>[c]

  \frametitle{Oyster Cards}

  \includegraphics[scale=0.4]{pics/oysterc.jpg}

  \begin{itemize}

  \item good example of a bad protocol\\ (security by obscurity)\bigskip

  \item<3->  ``Breaching security on Oyster cards should not 

  allow unauthorised use for more than a day, as TfL promises to turn 

  off any cloned cards within 24 hours\ldots''

  \end{itemize}

  \only<2>{

  \begin{textblock}{12}(0.5,0.5)

  \begin{tikzpicture}

  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

  {\color{darkgray}

  \begin{minipage}{11cm}\raggedright\footnotesize

  {\bf Wirelessly Pickpocketing a Mifare Classic Card}\medskip

  The Mifare Classic is the most widely used contactless smartcard on the

  market. The stream cipher CRYPTO1 used by the Classic has recently been

  reverse engineered and serious attacks have been proposed. The most serious

  of them retrieves a secret key in under a second. In order to clone a card,

  previously proposed attacks require that the adversary either has access to

  an eavesdropped communication session or executes a message-by-message

  man-in-the-middle attack between the victim and a legitimate

  reader. Although this is already disastrous from a cryptographic point of

  view, system integrators maintain that these attacks cannot be performed

  undetected.\smallskip

  This paper proposes four attacks that can be executed by an adversary having

  only wireless access to just a card (and not to a legitimate reader). The

  most serious of them recovers a secret key in less than a second on ordinary

  hardware. Besides the cryptographic weaknesses, we exploit other weaknesses

  in the protocol stack. A vulnerability in the computation of parity bits

  allows an adversary to establish a side channel. Another vulnerability

  regarding nested authentications provides enough plaintext for a speedy

  known-plaintext attack.

  \end{minipage}};

  \end{tikzpicture}

  \end{textblock}}

  \end{frame}}

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

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

  \mode<presentation>{

  \begin{frame}<1->[t]

  \frametitle{Another Example}

In an email from Ross Anderson\bigskip\small	

\begin{tabular}{l}

From: Ross Anderson <Ross.Anderson@cl.cam.ac.uk>\\

Sender: cl-security-research-bounces@lists.cam.ac.uk\\

To: cl-security-research@lists.cam.ac.uk\\

Subject: Birmingham case\\

Date: Tue, 13 Aug 2013 15:13:17 +0100\\

\end{tabular}

  \only<2>{

  \begin{textblock}{12}(0.5,0.5)

  \begin{tikzpicture}

  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

  {\color{darkgray}

  \begin{minipage}{11cm}\raggedright\footnotesize

As you may know, Volkswagen got an injunction against the University of

Birmingham suppressing the publication of the design of a weak cipher

used in the remote key entry systems in its recent-model cars. The paper

is being given today at Usenix, minus the cipher design.\medskip

I've been contacted by Birmingham University's lawyers who seek to prove

that the cipher can be easily obtained anyway. They are looking for a

student who will download the firmware from any newish VW, disassemble

it and look for the cipher. They'd prefer this to be done by a student

rather than by a professor to emphasise how easy it is.\medskip

Volkswagen's argument was that the Birmingham people had reversed a

locksmithing tool produced by a company in Vietnam, and since their key

fob chip is claimed to be tamper-resistant, this must have involved a

corrupt insider at VW or at its supplier Thales. Birmingham's argument

is that this is nonsense as the cipher is easy to get hold of. Their

lawyers feel this argument would come better from an independent

outsider.\medskip

Let me know if you're interested in having a go, and I'll put you in

touch

Ross

  \end{minipage}};

  \end{tikzpicture}

  \end{textblock}}

  \end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Authentication Protocols}

Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip

Passwords:

\begin{center}

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

\end{center}\pause\bigskip

Problems: Eavesdropper can capture the secret and replay it; \bl{$A$} cannot confirm the

identity of \bl{$B$}  

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Authentication Protocols}

Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip

Simple Challenge Response:

\begin{center}

\begin{tabular}{ll}

\bl{$A \rightarrow B:$} & \bl{$N$}\\

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

\end{tabular} 

\end{center}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Authentication Protocols}

Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip

Mutual Challenge Response:

\begin{center}

\begin{tabular}{ll}

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

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

\bl{$A \rightarrow B:$} & \bl{$N_B$}\\

\end{tabular} 

\end{center}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{One Time Passwords}

\begin{center}

\bl{$B \rightarrow A: C, C_{K_{AB}}$} 

\end{center}\bigskip

A counter \bl{$C$} increases with each transmission; \bl{$A$} will not accept a 

\bl{$C$}  which has already been accepted (used in car key fob).

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Person-in-the-Middle}

``Normal'' protocol run:\bigskip

\begin{itemize}

\item \bl{$A$} sends public key  to \bl{$B$}

\item \bl{$B$} sends public key  to \bl{$A$}

\item \bl{$A$} sends message encrypted with \bl{$B$}'s public key, \bl{$B$} decrypts it

with its private key

\item \bl{$B$} sends message encrypted with \bl{$A$}'s public key, \bl{$A$} decrypts it

with its private key

\end{itemize}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Person-in-the-Middle}

Attack:

\begin{itemize}

\item \bl{$A$} sends public key  to \bl{$B$}  --- \bl{$C$} intercepts this message and send his own public key

\item \bl{$B$} sends public key  to \bl{$A$} --- \bl{$C$} intercepts this message and send his own public key

\item \bl{$A$} sends message encrypted with \bl{$C$}'s public key, \bl{$C$} decrypts it

with its private key, re-encrypts with \bl{$B$}'s public key 

\item similar

\end{itemize}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Person-in-the-Middle}

Prevention:

\begin{itemize}

\item \bl{$A$} sends public key  to \bl{$B$}

\item \bl{$B$} sends public key  to \bl{$A$}

\item \bl{$A$} encrypts message with \bl{$B$}'s public key, send's {\bf half} of the message

\item \bl{$B$} encrypts message with \bl{$A$}'s public key, send's {\bf half} of the message

\item \bl{$A$} sends other half, \bl{$B$} can now decrypt entire message

\item \bl{$B$} sends other half, \bl{$A$} can now decrypt entire message

\end{itemize}\pause

\bl{$C$} would have to invent a totally new message

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Motivation}

The ISO/IEC 9798 specifies authentication mechanisms which use security 

techniques. These mechanisms are used to corroborate that an entity is the one 

that is claimed. An entity to be authenticated proves its identity by showing its 

knowledge of a secret. The mechanisms are defined as exchanges of information 

between entities and, where required, exchanges with a trusted third party.

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Motivation}

But\ldots\bigskip 

The ISO/IEC 9798 standard neither specifies a threat model nor defines the security properties that the protocols should satisfy.\pause\bigskip 

Unfortunately, there are no general precise definitions for the goals of protocols.

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Best Practices}

{\bf Principle 1:} Every message should say what it means: the interpretation of 

a message should not depend on the context.\bigskip\pause

{\bf Principle 2:} If the identity of a principal is essential to the meaning of a message, it is prudent 

to mention the principal’s name explicitly in the message (though difficult).\bigskip

\end{frame}}

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

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

\mode<presentation>{