2120 lines
68 KiB
TeX
2120 lines
68 KiB
TeX
\documentclass{book}
|
|
\providecommand{\draftversion}{no}
|
|
%----------------------------------------------------------------------------
|
|
\input{preamble}
|
|
%----------------------------------------------------------------------------
|
|
\usepackage[paper=a4paper]{geometry}
|
|
\usepackage{microtype}
|
|
\usepackage{cite}
|
|
\usepackage{makeidx}
|
|
\usepackage{watermark}
|
|
\usepackage{ifthen}
|
|
\usepackage{tikz}
|
|
\usepackage{environ}
|
|
\usepackage{listings}
|
|
\usetikzlibrary{fadings}
|
|
\usetikzlibrary{calc}
|
|
%----------------------------------------------------------------------------
|
|
%\usepackage{showidx} %%% NOTE: Only for DRAFT!
|
|
%----------------------------------------------------------------------------
|
|
\makeindex
|
|
%----------------------------------------------------------------------------
|
|
|
|
%----------------------------------------------------------------------------
|
|
\begin{document}
|
|
\input{macros}
|
|
\newcommand{\spdindex}[1]{\index{#1@\spd{#1}}}
|
|
%----------------------------------------------------------------------------
|
|
%
|
|
% NOTE TO FRIENDS: Please use the macro below to insert remarks at
|
|
% various points. Usage: \remark{A friend}{This is great!}
|
|
%
|
|
\ifthenelse{\equal{\draftversion}{yes}}
|
|
{
|
|
\newcommand{\remark}[2]{
|
|
|
|
{\bf Draft note (#1)} : {\em #2}
|
|
|
|
}
|
|
\newcommand{\later}{
|
|
|
|
{\em More text will be supplied at a later stage.}
|
|
|
|
}
|
|
}{
|
|
\newcommand{\remark}[2]{}
|
|
\newcommand{\later}{To be continued\ldots}
|
|
}
|
|
|
|
%----------------------------------------------------------------------------
|
|
%----------------------------------------------------------------------------
|
|
|
|
% Environments
|
|
\newenvironment{example}{}{}
|
|
|
|
\DefineVerbatimEnvironment
|
|
{screen}{Verbatim}
|
|
{fontsize=\small,frame=lines,fontfamily=courier}
|
|
\DefineVerbatimEnvironment
|
|
{ingraph}{Verbatim}
|
|
{frame=single,xleftmargin=1.0cm,xrightmargin=1.0cm}
|
|
\DefineVerbatimEnvironment
|
|
{email}{Verbatim}
|
|
{fontfamily=courier}
|
|
\DefineVerbatimEnvironment
|
|
{spdlFV}{Verbatim}
|
|
{frame=single,xleftmargin=1.0cm,xrightmargin=1.0cm}
|
|
\newcommand{\spd}[1]{{\tt #1}}
|
|
\newcommand{\scr}[1]{{\tt #1}}
|
|
\newcommand{\gra}[1]{{\tt #1}}
|
|
|
|
|
|
|
|
\lstnewenvironment{spdl}{%
|
|
\lstset{backgroundcolor=\color{verbgray},
|
|
frame=single,
|
|
framerule=0.5pt,
|
|
rulecolor=\color{verbgrayframe},
|
|
basicstyle=\small\ttfamily,
|
|
xleftmargin=10pt,
|
|
xrightmargin=10pt,
|
|
columns=fullflexible}}{}
|
|
|
|
%----------------------------------------------------------------------------
|
|
|
|
\pagestyle{headings}
|
|
|
|
%----------------------------------------------------------------------------
|
|
%
|
|
% FRONT PAGE
|
|
%
|
|
\thispagestyle{empty}
|
|
|
|
\definecolor{verbgray}{HTML}{F0F0F0} % Background of code listings
|
|
\definecolor{verbgrayframe}{HTML}{C0C0C0} % Background of code listings' frames
|
|
\definecolor{lgrey}{HTML}{C0E0FF} % Background of "new since" tabs
|
|
\definecolor{sblue}{HTML}{26546C}
|
|
\definecolor{lblue}{HTML}{E8F8FF}
|
|
\definecolor{gblue}{HTML}{6C6C6C}
|
|
\definecolor{sorange}{HTML}{E67400}
|
|
\definecolor{lorange}{HTML}{FFF8F0}
|
|
\definecolor{gorange}{HTML}{E6E6E6}
|
|
\definecolor{syellow}{HTML}{FBE115}
|
|
|
|
\begin{tikzpicture}[remember picture,overlay,
|
|
titletext/.style={text=black,inner sep=0pt,anchor=south west,font=\sf,align=left}
|
|
]
|
|
% Define coordinates
|
|
\node (a) at (current page.north west) {};
|
|
\node (b) at (current page.north east) {};
|
|
\node (e) at (current page.south west) {};
|
|
\node (f) at (current page.south east) {};
|
|
\node (c) at ($ (e) + (0mm,200mm) $) {};
|
|
\node (d) at ($ (f) + (0mm,200mm) $) {};
|
|
\node (x) at ($ (c) + (0mm, 4pt) $) {};
|
|
\node (y) at ($ (c) + (0mm,-4pt) $) {};
|
|
% Orange upper
|
|
%\fill[top color=white, bottom color=lorange]
|
|
% (a) rectangle ($ (d) + (0mm,-1mm) $);
|
|
\fill[sorange]
|
|
(x) rectangle ($ (d) + (0mm,-1mm) $);
|
|
% Bottom blue
|
|
% \fill[top color=lblue, bottom color=white]
|
|
% (c) rectangle (f);
|
|
% Blue center bar narrow
|
|
\fill[sblue]
|
|
(y) rectangle (d);
|
|
% Yellow
|
|
\fill [syellow]
|
|
(y) rectangle ($ (y) + (8mm,-32mm) $);
|
|
% Help grid
|
|
%\draw[help lines,step=10mm] (e) grid (20,30);
|
|
% Text
|
|
\node[titletext,scale=10]
|
|
at ($ (e) + (30mm,145mm) $)
|
|
{Scyther};
|
|
\node[titletext,scale=6]
|
|
at ($ (e) + (30mm,125mm) $)
|
|
{User Manual};
|
|
\node[titletext,scale=3]
|
|
at ($ (e) + (60mm,235mm) $)
|
|
{Cas Cremers};
|
|
%{Cas Cremers\\Sjouke Mauw}; %% Until now, one man effort
|
|
|
|
% Draft
|
|
\node[titletext,scale=2,anchor=south]
|
|
at ($ (e) + (105mm,30mm) $)
|
|
{Draft \today};
|
|
\end{tikzpicture}
|
|
%----------------------------------------------------------------------------
|
|
%
|
|
% Headers
|
|
%
|
|
\newcommand{\mygheaderA}{
|
|
% Define coordinates
|
|
\node (a) at ($ (current page.north west) + (0mm,-25mm) $) {};
|
|
\node (b) at ($ (current page.north east) + (0mm,-25mm) $) {};
|
|
\node (c) at ($ (a) + (0mm,-5mm) $) {};
|
|
\node (d) at ($ (b) + (0mm,-5mm) $) {};
|
|
\node (e) at ($ (c) + (0mm,-7mm) $) {};
|
|
\node (f) at ($ (d) + (0mm,-7mm) $) {};
|
|
% Orange upper
|
|
\draw[draw=none]
|
|
[fill=gorange]
|
|
(a) rectangle ($ (d) + (0mm,-1mm) $);
|
|
\draw[draw=none]
|
|
[postaction={path fading=north,fill=sorange}]
|
|
(a) rectangle ($ (d) + (0mm,-1mm) $);
|
|
% Bottom blue
|
|
% \draw[draw=none]
|
|
% [fill=gblue]
|
|
% (c) rectangle (f);
|
|
\draw[draw=none]
|
|
[postaction={path fading=south,fill=sblue}]
|
|
(c) rectangle (f);
|
|
% Yellow highlight
|
|
\tikzfading[name=fade out,
|
|
inner color=transparent!0,
|
|
outer color=transparent!100]
|
|
}
|
|
\newcommand{\mygheaderB}{
|
|
\draw[draw=none]
|
|
[postaction={path fading=north,fill=white}]
|
|
(c) rectangle (f);
|
|
}
|
|
\newsavebox{\myheaderL}
|
|
\newsavebox{\myheaderR}
|
|
\savebox{\myheaderL}{
|
|
\begin{tikzpicture}[remember picture,overlay,
|
|
titletext/.style={text=white,inner sep=0pt,anchor=south west,font=\sf,align=left}
|
|
]
|
|
\mygheaderA
|
|
\begin{scope}
|
|
\draw[draw=none,clip]
|
|
(c) rectangle (f);
|
|
\fill [syellow,path fading=fade out]
|
|
($ (d) + -1.0*(30mm,90mm) $) rectangle ($ (d) + (30mm,90mm) $);
|
|
\end{scope}
|
|
\mygheaderB
|
|
\end{tikzpicture}
|
|
}
|
|
\savebox{\myheaderR}{
|
|
\begin{tikzpicture}[remember picture,overlay,
|
|
titletext/.style={text=white,inner sep=0pt,anchor=south west,font=\sf,align=left}
|
|
]
|
|
\mygheaderA
|
|
\begin{scope}
|
|
\draw[draw=none,clip]
|
|
(c) rectangle (f);
|
|
\fill [syellow,path fading=fade out]
|
|
($ (c) + -1.0*(30mm,90mm) $) rectangle ($ (c) + (30mm,90mm) $);
|
|
\end{scope}
|
|
\mygheaderB
|
|
\end{tikzpicture}
|
|
}
|
|
%\leftwatermark{\usebox{\myheaderL}}
|
|
%\rightwatermark{\usebox{\myheaderR}}
|
|
|
|
|
|
% NOTE for use of the 'supported' macro for denoting new features.
|
|
%
|
|
% \subsection[RealTitle]{RealTitle\supported{MyVersion and YourVersion}}
|
|
%
|
|
% The square-bracket version is needed, otherwise the 'new' bar shows up
|
|
% in the table of contents.
|
|
\newcommand{\supported}[1]{
|
|
\hfill
|
|
\colorbox{lgrey}{{\text{\small New in version #1}}
|
|
}}
|
|
|
|
%----------------------------------------------------------------------------
|
|
\tableofcontents
|
|
%----------------------------------------------------------------------------
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Introduction}
|
|
%----------------------------------------------------------------------------
|
|
|
|
\begin{center}
|
|
\fbox{\parbox{0.8\textwidth}{
|
|
\sf {\bf Note:} This is a draft of the new version of the Scyther manual. The manual may therefore be
|
|
incomplete at points.
|
|
|
|
Any feedback is
|
|
welcome and can be sent to Cas Cremers by e-mail:
|
|
{\tt cas.cremers@cs.ox.ac.uk}.
|
|
}}
|
|
\end{center}
|
|
|
|
\bigskip
|
|
|
|
\noindent
|
|
This is the user manual for the Scyther security protocol verification
|
|
tool.
|
|
|
|
The purpose of this manual is to explain the
|
|
details of the Scyther input language, explain how to model basic
|
|
protocols, and how to effectively use the Scyther tool.
|
|
This manual does not detail the protocol execution model nor
|
|
the adversary model used by the tool. It is therefore highly recommended to read the
|
|
accompanying book~\cite{opsembook}. The book includes a detailed
|
|
description of Scyther's
|
|
underlying protocol model, security property specifications, and the
|
|
algorithm.
|
|
|
|
We proceed in the following way. Some background is given in
|
|
Chapter~\ref{sec:background}.
|
|
Chapter~\ref{sec:install} explains how to install the Scyther tool on
|
|
various platforms. In Chapter~\ref{sec:tutorial} we give a brief
|
|
tutorial using simple examples to show the basics of the tool.
|
|
Then we discuss things in more detail as we introduce the input language
|
|
of the tool in Chapter~\ref{sec:input}. Modeling of basic protocols is
|
|
described in Chapter~\ref{sec:modeling}, and
|
|
Chapter~\ref{sec:properties} describes how to specify security
|
|
properties. The usage of the GUI version of tool
|
|
is then explained in more detail in Section~\ref{sec:gui}. The
|
|
underlying command-line tool is described in Section~\ref{sec:cli}.
|
|
Advanced topics are discussed
|
|
in Section~\ref{sec:advanced}.
|
|
|
|
\section*{Online information}
|
|
|
|
More help can be found online on the Scyther website:
|
|
|
|
\index{Scyther website}
|
|
\index{website|see{Scyther website}}
|
|
\medskip
|
|
\url{http://users.ox.ac.uk/~coml0529/scyther/index.html}
|
|
\medskip
|
|
|
|
\noindent
|
|
Users are advised to subscribe to the Scyther mailing list,
|
|
whose details can also be found on the Scyther website.
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Background}
|
|
\label{sec:background}
|
|
%----------------------------------------------------------------------------
|
|
|
|
Scyther is a tool for the formal analysis of security protocols under the
|
|
\emph{perfect cryptography assumption}, in which it is assumed that all
|
|
cryptographic functions are perfect: the adversary learns nothing from
|
|
an encrypted message unless he knows the decryption key. The tool can be
|
|
used to find problems that arise from the way the protocol is
|
|
constructed. This problem is undecidable in general, but in practice
|
|
many protocols can be either proven correct or attacks can be found.
|
|
|
|
The full protocol model, its assumptions, the basic security properties,
|
|
and the algorithm are described in~\cite{opsembook}. This manual serves
|
|
as a companion to the book. Thus, in this manual we assume the
|
|
reader is familiar with the formal modeling of security protocols and
|
|
their properties.
|
|
|
|
% Not only is knowledge of security protocol models needed to use the
|
|
% Scyther tool, further knowledge is needed to know how to interpret the
|
|
% results that the tool produces in any useful way. In fact, the reader
|
|
% should be very cautious: security protocol models and their properties
|
|
% are intricate and it is easy to misinterpret the results.
|
|
%
|
|
% Having said that, one of the main goals of Scyther is to help with the
|
|
% analysis of a protocol in such a way that for example attacks can be
|
|
% understood well. Thus, wherever possible the tool will give useful
|
|
% information on the results.
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Installation}
|
|
\label{sec:install}
|
|
%----------------------------------------------------------------------------
|
|
|
|
Scyther can be downloaded from the following website:
|
|
|
|
\index{downloading Scyther}
|
|
\url{http://users.ox.ac.uk/~coml0529/scyther/}
|
|
|
|
\medskip
|
|
|
|
\noindent
|
|
\index{installing Scyther}
|
|
Installation instruction are included in the downloadable Scyther
|
|
archives. Scyther is available for the Windows,
|
|
Linux and Mac OS platforms.
|
|
|
|
%\section{Linux}
|
|
|
|
%\section{Windows}
|
|
|
|
%\section{MAC OS X}
|
|
|
|
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Quick start tutorial}
|
|
\label{sec:tutorial}
|
|
%----------------------------------------------------------------------------
|
|
|
|
\index{quick start tutorial}
|
|
Scyther takes as input a security protocol description that includes a
|
|
specification of intended security properties, referred to as security
|
|
claims, and evaluates these.
|
|
|
|
Start Scyther by executing the \scr{scyther-gui.py} program in the
|
|
Scyther directory. The program will launch two windows: the main window,
|
|
in which files are edited, and the \scr{about} window, which shows some
|
|
information about the tool.
|
|
|
|
As an introductory example, we will verify the Needham-Schroeder
|
|
protocol, and investigate an attack on it.
|
|
|
|
Go to the file$\rightarrow$open dialog, and open the file
|
|
\scr{ns3.spdl} in the Scyther directory. Your main window should look
|
|
like the one in Figure~\ref{protocolwindow}.
|
|
|
|
\begin{figure}[!htb]
|
|
\begin{center}
|
|
\includegraphics[height=0.90\textheight]{protocolwindow}
|
|
\end{center}
|
|
\label{protocolwindow}
|
|
\caption{Scyther main window with the file ns3.spdl opened}
|
|
\end{figure}
|
|
|
|
By
|
|
convention, protocol description files have the extension \scr{.spdl} (Security Protocol Description
|
|
Language), but it can have any name. The file used in this example is
|
|
shown in Appendix~\ref{app:ns3}.
|
|
|
|
Run the verification tool by selecting verify$\rightarrow$verify\_claims in the
|
|
menu. A new window will appear during the verification process. Once
|
|
verification is completed, the window will be
|
|
replaced by the result window, as shown in
|
|
Figure~\ref{resultwindow}.
|
|
|
|
\begin{figure}[!htb]
|
|
\begin{center}
|
|
\includegraphics[scale=0.5]{resultwindow}
|
|
\end{center}
|
|
\label{resultwindow}
|
|
\caption{Scyther result window}
|
|
\end{figure}
|
|
|
|
The result window shows a summary of the claims in the protocol, and the
|
|
verification results. Here one can find whether the protocol is correct,
|
|
or false. In the next section there will be a full explanation of the
|
|
possible outcomes of the verification process. Most importantly, if a
|
|
protocol claim is incorrect, then there exists at least one
|
|
attack on the protocol. A button is shown next to the claim: press this
|
|
button to view the attacks on the claim, as in
|
|
Figure~\ref{attackwindow}.
|
|
|
|
\begin{figure}[!htb]
|
|
\begin{center}
|
|
\includegraphics[height=0.90\textheight]{attackwindow}
|
|
\end{center}
|
|
\label{attackwindow}
|
|
\caption{Scyther attack window}
|
|
\end{figure}
|
|
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Input Language}
|
|
\label{sec:input}
|
|
%----------------------------------------------------------------------------
|
|
|
|
Scyther's input language is loosely based on a C/Java-like syntax.
|
|
The main purpose of the language is to describe protocols, which are defined by a set of
|
|
roles. Roles, in turn, are defined by a sequence of events, most of
|
|
which are events that denote the sending or receiving of terms. We describe
|
|
these elements in the following sections.
|
|
|
|
\index{comments}
|
|
Comments can start with \spd{//} or \spd{\#} (for single-line comments) or
|
|
be enclosed by \spd{/*} and \spd{*/} (for multi-line comments). Note that
|
|
multi-line comments cannot be nested.
|
|
|
|
\index{whitespace}
|
|
Any whitespace between elements is ignored. It is
|
|
therefore possible to use whitespace (spaces, tabs, newlines) to
|
|
improve readability.
|
|
|
|
\index{identifier}
|
|
A basic identifier consists of a string of characters from
|
|
the set of alphanumeric characters as well as the symbols
|
|
\spd{\^{}} and \spd{-}.
|
|
|
|
\index{case-sensitive}
|
|
The language is case-sensitive, thus \spd{NS3} is not the same
|
|
identifier as \spd{ns3}.
|
|
|
|
%............................................................................
|
|
\section{A minimal input file}
|
|
|
|
The core elements in a Scyther input file are protocol definitions. A
|
|
minimal example is the following:
|
|
\begin{spdl}
|
|
protocol ExampleProtocol(I,R) {
|
|
role I { };
|
|
role R { };
|
|
};
|
|
\end{spdl}
|
|
In the above, we have defined a protocol called ``ExampleProtocol'' that
|
|
has two roles, ``I'' and ``R'' by listing them between brackets after
|
|
the protocol name. Note that we haven't defined the
|
|
behaviour of these roles
|
|
yet: such behaviours are defined within the curly brackets after the
|
|
corresponding \spd{role I} and \spd{role R} commands.
|
|
|
|
|
|
%............................................................................
|
|
\section{Terms}
|
|
|
|
At the most basic level, Scyther manipulates terms.
|
|
|
|
\subsection{Atomic terms}
|
|
|
|
\index{atomic term}
|
|
An atomic term can be any identifier, which is usually a string of
|
|
alphanumeric characters.
|
|
|
|
Atomic terms can be combined into more complex terms by
|
|
operators such as pairing and encryption.
|
|
|
|
\subsubsection{Constants}
|
|
\index{constant}
|
|
\index{global constant}
|
|
|
|
\subsubsection{Freshly generated values}
|
|
\index{freshly generated value}
|
|
\index{nonce}
|
|
\index{random value}
|
|
|
|
Many security protocols rely on generating random values. They can be
|
|
specified by declaring them inside a role definition using the
|
|
\spd{fresh} declaration. For example, to generate a random value
|
|
\scr{Na} of
|
|
type \spd{Nonce}, we specify:
|
|
\begin{spdl}
|
|
role X(...) {
|
|
fresh Na: Nonce;
|
|
|
|
send_1(X,Y,Na);
|
|
}
|
|
\end{spdl}
|
|
|
|
\subsubsection{Variables}
|
|
\index{variable}
|
|
\index{var}
|
|
|
|
Agents can use variables to store received terms. For example, to
|
|
receive a nonce into a variable with name \spd{Na}, we specify:
|
|
\begin{spdl}
|
|
role Y(...) {
|
|
var Na: Nonce;
|
|
|
|
recv_1(X,Y,Na);
|
|
}
|
|
\end{spdl}
|
|
Local declarations, for both freshly generated values as
|
|
well as variables such as \spd{Na}, are local to the role.
|
|
Thus, one can specify a \emph{freshly generated nonce} \spd{Na} in one
|
|
role and a variable \spd{Na} in another role without any conflicts.
|
|
Variables are rigid: after the first receive event in which they occur
|
|
has been executed, they are assigned a value. This value cannot be
|
|
changed afterwards.
|
|
|
|
Variables must occur first in receive events: it is not allowed to
|
|
use uninitialized variables in send events.
|
|
|
|
\subsection{Pairing}
|
|
|
|
\index{pairing}
|
|
\index{tupling}
|
|
Any two terms can combined into a term pair: we write \spd{(x,y)} for
|
|
the pair of terms \spd{x} and \spd{y}. It is also allowed to write
|
|
n-tuples as \spd{(x,y,z)}, which is interpreted by Scyther as \spd{((x,y),z)}.
|
|
|
|
\subsection{Symmetric keys}
|
|
|
|
\index{symmetric keys}
|
|
Any term can act as a key for symmetrical encryption.
|
|
|
|
The encryption of \spd{ni} with a term \spd{kir} is written as:
|
|
\begin{spdl}
|
|
{ ni }kir
|
|
\end{spdl}
|
|
|
|
Unless \spd{kir} is explicitly defined as being part of an asymmetric
|
|
key pair (explained below), this is interpreted as symmetric encryption.
|
|
|
|
\index{k(X,Y)@\spd{k(X,Y)}}
|
|
A symmetric-key infrastructure is predefined:
|
|
\spd{k(X,Y)} denotes the long-term symmetric key shared between $X$ and $Y$.
|
|
|
|
\subsection{Asymmetric keys}
|
|
|
|
\index{asymmetric keys}
|
|
\index{sk(X)@\spd{sk(X)}}
|
|
\index{pk(X)@\spd{pk(X)}}
|
|
A public-key infrastructure (PKI) is predefined:
|
|
\spd{sk(X)} denotes the long-term private key of $X$, and \spd{pk(X)}
|
|
denotes the corresponding public key.
|
|
|
|
\begin{example}
|
|
|
|
As an example, consider the following term. It represents the encryption
|
|
of some term \spd{ni} by the term \spd{pk(I)}. Under normal conventions,
|
|
this means that the nonce of the initiator (\spd{ni}) is encrypted with
|
|
the public key of the initiator.
|
|
|
|
\begin{spdl}
|
|
{ ni }pk(I)
|
|
\end{spdl}
|
|
|
|
This term can only be decrypted by an agent who knows the secret key
|
|
\spd{sk(I)}.
|
|
|
|
\end{example}
|
|
|
|
Section~\ref{adv:asymmetric} describes how to model more than one key
|
|
pair per agent.
|
|
|
|
\subsection{Hash functions}
|
|
|
|
\index{hash functions}
|
|
\index{hashfunction@\spd{hashfunction}}
|
|
Hash functions are essentially encryptions with a function, of which the inverse is not known by anybody.
|
|
|
|
They can be used by a global declaration of an identifier to be a
|
|
hashfunction, \eg:
|
|
\begin{spdl}
|
|
hashfunction H1;
|
|
\end{spdl}
|
|
As all agents and protocols should have access to such a function, the
|
|
declaration of hashfunction is usually global, \ie, defined outside of
|
|
any protocol definition.
|
|
|
|
|
|
\begin{example}
|
|
Once declared, they can be used in protocol messages, \eg:
|
|
\begin{spdl}
|
|
H1(ni)
|
|
\end{spdl}
|
|
|
|
\end{example}
|
|
|
|
|
|
\subsection{Predefined types}
|
|
|
|
\begin{description}
|
|
|
|
\item [\spd{Agent }]
|
|
|
|
\spdindex{Agent}
|
|
Type used for agents.
|
|
|
|
\item [\spd{Function }]
|
|
|
|
\spdindex{Function}
|
|
A special type that defines a function term that can take a list
|
|
of terms as parameter. By default, it behaves like a hash
|
|
function: given the term \spd{h(x)} where \spd{h} is of type
|
|
\spd{Function}, it is impossible to derive \spd{x}.
|
|
|
|
\item [\spd{Nonce }]
|
|
|
|
\spdindex{Nonce}
|
|
A standard type that is often used and therefore defined inside
|
|
the tool.
|
|
|
|
\item [\spd{Ticket }]
|
|
|
|
\spdindex{Ticket}
|
|
A variable of type \spd{Ticket} can be substituted by any term.
|
|
|
|
\end{description}
|
|
|
|
\subsection{Usertypes}
|
|
|
|
\spdindex{usertype}
|
|
It is possible to define a new type. This can be done
|
|
using the \spd{usertype} command:
|
|
\begin{spdl}
|
|
usertype MyAtomicMessage;
|
|
|
|
protocol X(I,R) {
|
|
role I {
|
|
var y: MyAtomicMessage;
|
|
|
|
recv_1(I,R, y );
|
|
\end{spdl}
|
|
The effect of such a declaration is that variables of the new type can
|
|
only be instantiated with messages \spd{m} of that type, \ie, that have been
|
|
declared by the global declaration
|
|
\spd{const m: MyAtomicMessage}
|
|
or the freshly generated
|
|
\spd{fresh m: MyAtomicMessage} within a role.
|
|
|
|
In general, the tool can perform better if more is known about which messages might unify or not. By defining a usertype, the modeler can inform the tool that a variable can only be instantiated with terms of that type, and not with, \eg, terms of type Nonce.
|
|
Conceptually, one can always write \spd{Ticket} (which corresponds to all possible messages) for each variable type, but then one may find false attacks (in case the implementation in fact does check the type of a message) and the tool will be less likely to verify the property (for an unbounded number of runs).
|
|
|
|
\remark{CC}{Generic (local) declarations? Where is 'fresh' explained?}
|
|
|
|
\remark{CC}{TODO: reverse order: first protocol context, then roles,
|
|
then events. That way we can actually show what events can do.}
|
|
|
|
%............................................................................
|
|
\section{Events}
|
|
\index{events}
|
|
|
|
\subsection{Receive and send events}
|
|
|
|
\spdindex{send}
|
|
\index{event!send}
|
|
\index{event!recv}
|
|
\spdindex{send}
|
|
\spdindex{recv}
|
|
The \spd{recv} and \spd{send} events mark receiving and sending a
|
|
message, respectively. For example, we write:
|
|
\begin{spdl}
|
|
role MyRole(...) {
|
|
recv_Label1(OtherRole, MyRole, m1);
|
|
send_Label2(MyRole, OtherRole, m2);
|
|
}
|
|
\end{spdl}
|
|
to specify that role \spd{MyRole} first receives message \spd{m1} from
|
|
\spd{OtherRole} and then sends message \spd{m2} to \spd{OtherRole}. The
|
|
receive event is labeled with label \spd{Label1} and the send event is
|
|
labeled with \spd{Label2}.
|
|
|
|
Usually each \spd{send} event will have a corresponding \spd{recv}
|
|
event. We specify this correspondence by giving corresponding events the same
|
|
label.
|
|
\begin{spdl}
|
|
role MyRole(...) {
|
|
send_Label3(MyRole, OtherRole, m2);
|
|
}
|
|
role OtherRole(...) {
|
|
recv_Label3(MyRole, OtherRole, m2);
|
|
}
|
|
\end{spdl}
|
|
|
|
|
|
\subsubsection*{Bang prefix for labels}
|
|
|
|
For some protocols we may want to model sending or receiving to the
|
|
adversary directly, in which case we have no corresponding event.
|
|
If a \spd{send} or \spd{recv} event has no corresponding event, Scyther
|
|
will output a warning. To surpress this warning, the label can be
|
|
prefixed by a bang \spd{!}, \eg:
|
|
\index{20@{\tt "!}}
|
|
\begin{spdl}
|
|
send_!1(I,I, LeakToAdversary );
|
|
\end{spdl}
|
|
|
|
|
|
\subsection{Claim events and Security properties}
|
|
\index{event!claim}
|
|
\index{claim event}
|
|
\index{security properties}
|
|
|
|
\spdindex{claim}
|
|
Claim events are used in role specifications to model intended security properties. For
|
|
example, the following claim event models that \spd{Ni} is meant to be
|
|
secret.
|
|
\begin{spdl}
|
|
claim(I, Secret, Ni);
|
|
\end{spdl}
|
|
|
|
There are several predefined claim types.
|
|
|
|
\begin{description}
|
|
|
|
|
|
|
|
\item[\spd{Secret }]
|
|
|
|
\spdindex{Secret}
|
|
This claim requires a parameter term. Secrecy of this term is
|
|
claimed as defined in~\cite{opsembook}.
|
|
|
|
\item[\spd{SKR }]
|
|
|
|
\spdindex{SKR}
|
|
The verification condition for this claim is equivalent to the \spd{Secret} claim.
|
|
|
|
The purpose of this claim is to additionally mark the parameter term as a session-key.
|
|
The consequence is that using the \emph{session-key reveal}
|
|
adversary rule will now reveal the parameter term.
|
|
|
|
If the \emph{session-key reveal} rule is not enabled, this
|
|
claim is identical to the \spd{Secret} claim.
|
|
|
|
\item[\spd{Alive }]
|
|
|
|
\spdindex{Alive}
|
|
Aliveness (of all roles) as defined in~\cite{lowe97hierarchy}.
|
|
|
|
\item[\spd{Weakagree }]
|
|
|
|
\spdindex{Weakagree}
|
|
Weak agreement (of all roles) as defined in~\cite{lowe97hierarchy}.
|
|
|
|
\item[\spd{Commit}, \spd{Running } ]
|
|
|
|
\spdindex{Commit}
|
|
\spdindex{Running}
|
|
\index{agreement on data}
|
|
\index{data agreement}
|
|
\index{non-injective agreement}
|
|
Non-injective agreement with a role on a set of data
|
|
items~\cite{lowe97hierarchy} can be defined by
|
|
inserting the appropriate signal claims.
|
|
In this context, \spd{Commit} marks the effective claim, whose
|
|
correctness requires the existence of a corresponding
|
|
\spd{Running} signal in the trace.
|
|
|
|
These claims are used to model agreement over data, which is
|
|
explained in Section~\ref{sec:agreement}.
|
|
|
|
|
|
|
|
|
|
|
|
\item[\spd{Nisynch }]
|
|
|
|
\spdindex{Nisynch}
|
|
\index{synchronisaton}
|
|
\index{non-injective synchronisation}
|
|
Non-injective synchronisation as defined in~\cite{opsembook}.
|
|
|
|
\item[\spd{Niagree }]
|
|
|
|
\spdindex{Niagree}
|
|
\index{agreement (on messages)}
|
|
\index{message agreement}
|
|
\index{non-injective agreement}
|
|
Non-injective agreement on messages as defined in~\cite{opsembook}.
|
|
|
|
\item[\spd{Reachable }]
|
|
|
|
\spdindex{Reachable}
|
|
When this claim is verified, Scyther will check whether this
|
|
claim can be reached at all. It is true iff there exists a trace
|
|
in which this claim occurs. This can be useful to check if there
|
|
is no obvious error in the protocol specification, and is in
|
|
fact inserted when the \scr{--check} mode of Scyther is used.
|
|
|
|
\item[\spd{Empty }]
|
|
\spdindex{Empty}
|
|
This claim will not be verified, but simply ignored. It is only
|
|
useful when Scyther is used as a back-end for other verification
|
|
means. For more on this, see Section~\ref{sec:advanced}.
|
|
|
|
\end{description}
|
|
|
|
|
|
\subsection{Internal computation/pattern match events}
|
|
\index{internal computation events}
|
|
\index{pattern match events}
|
|
|
|
We extend the basic set of events from~\cite{opsembook} with two events that can be used to
|
|
model internal computations.
|
|
|
|
\subsubsection[Match event]{Match event\supported{v1.1 and Compromise-0.8}}
|
|
\index{match event}
|
|
\index{event!match}
|
|
|
|
The first new event is the \spd{match} event, that is used to specify
|
|
pattern matching, \ie,
|
|
\begin{spdl}
|
|
match(pt,m)
|
|
\end{spdl}
|
|
In operational terms, if there exists a well-typed substitution $\sigma$
|
|
such that $\sigma pt = m$, then this event can be executed. Upon
|
|
execution, the substitution is applied to the remaining events of the
|
|
role.
|
|
|
|
This event can be used to model various constructions, such as equality
|
|
tests, delayed decryption, checking commitments. They can also be used
|
|
to model internal computations to simplify specifications, \eg:
|
|
\begin{spdl}
|
|
var X: Nonce;
|
|
var Y;
|
|
|
|
recv(R,I, X);
|
|
match(Y, hash(X,I,R) );
|
|
send(I,R, Y,{ Y }sk(I) );
|
|
\end{spdl}
|
|
In the above example, we could have replaced \spd{Y} by
|
|
\spd{hash(X,I,R)} throughout the specification, but this version avoid
|
|
replication.
|
|
|
|
\subsubsection[Not match event]{Not match event\supported{v1.1 and Compromise-0.8}}
|
|
\index{not match event}
|
|
\index{event!not match}
|
|
|
|
The second new event is the \spd{not match} event, that is used to specify
|
|
pattern matching, \ie,
|
|
\begin{spdl}
|
|
not match(pt,m)
|
|
\end{spdl}
|
|
The operational interpretation is the opposite of the previous event. If
|
|
there is no substitution $\sigma$ such that $\sigma pt = m$, then the
|
|
event can be executed.
|
|
|
|
This event can be used to model, \eg, inequality constraints. For
|
|
example, the execution model allows by default agents executing
|
|
sessions with themselves. In some cases, we want to exclude such
|
|
behaviour, because the protocol disallows it. For example,
|
|
\begin{spdl}
|
|
role A {
|
|
not match(A,B);
|
|
send (A,B, m1);
|
|
}
|
|
\end{spdl}
|
|
models a role whose instances only send messages to other agents.
|
|
|
|
As a more advanced usage, \spd{match} and \spd{not match} can be used
|
|
together in two roles with a common starting sequence of events to model
|
|
\emph{if ... then ... else} constructions.
|
|
% LATER (advanced topics)
|
|
% We will return to this issue in Section~\ref{}
|
|
|
|
%............................................................................
|
|
\section{Role definitions}
|
|
|
|
\index{role definition}
|
|
Role definitions are sequences of events, \ie, declarations, send,
|
|
receive, or claim events.
|
|
|
|
\begin{spdl}
|
|
role Server {
|
|
var x,y,z: Nonce;
|
|
fresh n,m: Nonce;
|
|
|
|
send_1(Server,Init, m,n );
|
|
recv_2(Init,Server, x,y, { z }pk(Server) );
|
|
}
|
|
\end{spdl}
|
|
|
|
%............................................................................
|
|
\section{Protocol definitions}
|
|
|
|
\index{protocol definition}
|
|
A protocol definition takes as a parameter a sequence of roles, which
|
|
are then defined within its body.
|
|
|
|
\begin{spdl}
|
|
protocol MyProt(Init,Resp,Server)
|
|
{
|
|
role Init {
|
|
...
|
|
}
|
|
role Resp {
|
|
...
|
|
}
|
|
role Server {
|
|
...
|
|
}
|
|
}
|
|
\end{spdl}
|
|
|
|
\subsection*{Helper protocols}
|
|
\index{helper protocol|textbf}
|
|
\index{19@"@}
|
|
|
|
It is possible to prepend an ``@'' symbol before a protocol name. This
|
|
has no effect on the protocol model, nor on the outcome of the analysis.
|
|
The ``@'' is only used when rendering output graphs: the intent is to mark
|
|
the protocol as a
|
|
``helper protocol''. Such protocols are often used to model additional adversary
|
|
capabilities, see Section~\ref{sec:advanced} for examples.
|
|
When rendering output graphs, Scyther collapses role instances of helper
|
|
protocols into single nodes. This can make the graphs more readable.
|
|
|
|
\subsection*{Symmetric-role protocols}
|
|
\index{symmetric-role protocol|textbf}
|
|
|
|
Some adversary-compromise rules, such as $\mathit{SKR}$ and
|
|
$\mathit{LKR}_\mathit{aftercorrect}$ depend on a partnering function. For
|
|
protocols that are entirely symmetric in their roles and key
|
|
computations (such as HMQV), this is not the appropriate partnering
|
|
function. To use the correct partnering function, the protocol needs to
|
|
be annotated as a \emph{symmetric-role} protocol. This instructs Scyther
|
|
to use the appropriate partnering function.
|
|
|
|
\begin{spdl}
|
|
symmetric-role protocol MyProt(Init,Resp)
|
|
{
|
|
role Init {
|
|
...
|
|
}
|
|
role Resp {
|
|
...
|
|
}
|
|
}
|
|
\end{spdl}
|
|
|
|
|
|
%............................................................................
|
|
\section{Global declarations}
|
|
|
|
\index{global declarations}
|
|
In many applications global constants are used. These include, for
|
|
example, string constants, labels, or protocol identifiers.
|
|
|
|
\spdindex{const}
|
|
They are modeled and used in the following way:
|
|
\begin{spdl}
|
|
usertype String;
|
|
const HelloWorld: String;
|
|
|
|
protocol hello(I,R)
|
|
{
|
|
role I {
|
|
send_1(I,R, HelloWorld);
|
|
}
|
|
role R {
|
|
recv_1(I,R, HelloWorld);
|
|
}
|
|
}
|
|
\end{spdl}
|
|
|
|
|
|
%............................................................................
|
|
\section{Miscellaneous}
|
|
|
|
\subsection[Macro]{Macro\supported{v1.1 and Compromise-0.8}}
|
|
\spdindex{macro}
|
|
\index{abbreviate}
|
|
\index{define macro}
|
|
It is possible to define \emph{macros}, \ie, abbreviations for
|
|
particular term.
|
|
The syntax used to define these abbreviations is the following:
|
|
\begin{spdl}
|
|
macro MyShortCut = LargeTerm;
|
|
\end{spdl}
|
|
For example, for a protocol that contains complex
|
|
messages or repeating elements, macros can be used to simplify the
|
|
protocol specification:
|
|
\begin{spdl}
|
|
hashfunction h;
|
|
|
|
protocol macro-example-one(I,R) {
|
|
role I {
|
|
fresh nI: Nonce;
|
|
macro m1 = h(I,ni);
|
|
|
|
send_1(I,R, { m1 }pk(R) );
|
|
claim(I, Secret, m1);
|
|
}
|
|
role R {
|
|
var X: Ticket;
|
|
|
|
recv_1(I,R, { X }pk(R) );
|
|
}
|
|
}
|
|
\end{spdl}
|
|
Note that macros have \emph{global scope}, and are handled at the
|
|
\emph{syntactical} level. This also allows for global abbreviations of
|
|
protocol messages, \eg:
|
|
\begin{spdl}
|
|
hashfunction h;
|
|
macro m1 = { I,R, nI, h(nI,R) }pk(R);
|
|
|
|
protocol macro-example-two(I,R) {
|
|
role I {
|
|
fresh nI: Nonce;
|
|
|
|
send_1(I,R, m1 );
|
|
}
|
|
role R {
|
|
var nI: Nonce;
|
|
|
|
recv_1(I,R, m1 );
|
|
}
|
|
}
|
|
\end{spdl}
|
|
Note that in the above example, \spd{nI} is a freshly generated nonce in
|
|
the I role, and a variable in the R role. Because the macro definitions
|
|
are unfolded syntactically, the same macro can be used to refer to both
|
|
terms.
|
|
|
|
\subsection{Include}
|
|
It is possible to import other files in a protocol specification:
|
|
|
|
\spdindex{include}
|
|
\index{import file}
|
|
\index{input file}
|
|
\begin{spdl}
|
|
include "filename";
|
|
\end{spdl}
|
|
|
|
where {\em filename} denotes the name of the file that will be included
|
|
at this point. Using this command, it is possible to share, \eg, a set of common
|
|
definitions between files. Typically this will include definitions for
|
|
the key structures, and (untrusted) agent names. Nested use of this
|
|
command is possible.
|
|
|
|
\subsection[one-role-per-agent]{one-role-per-agent\supported{v1.1 and Compromise-0.8}}
|
|
\spdindex{one-role-per-agent}
|
|
\index{one role per agent}
|
|
\index{multiple roles per agent}
|
|
The operational semantics allow agents to perform any roles, and even
|
|
multiple different roles in parallel. This modeling choice corresponds
|
|
to the worst possible scenario, in which the adversary has the most
|
|
options to exploit. However, in many concrete settings, agents perform
|
|
only one role. For example, the set of servers may be disjoint from the
|
|
set of clients, or the set of RFID tags may be disjoint from the set of
|
|
readers. In such cases, we do not need to consider attacks that exploit
|
|
that an agent can perform multiple roles. This can be modeled by the
|
|
following statement:
|
|
\begin{spdl}
|
|
option "--one-role-per-agent"; // disallow agents in multiple roles
|
|
\end{spdl}
|
|
This causes Scyther to ignore attacks in which agents perform multiple
|
|
roles. Phrased differently, this corresponds to the situation in which
|
|
each role is performed by a dedicated set of agents.
|
|
|
|
%............................................................................
|
|
\section{Language BNF}
|
|
|
|
\index{BNF}
|
|
The full BNF grammar for the input language is given below. In the
|
|
strict language definition, there are no claim terms such as
|
|
\spd{Niagree} and \spd{Nisynch}, and neither are there any predefined
|
|
type classes such as \spd{Agent}. Instead, they are predefined constant
|
|
terms in the Scyther tool itself.
|
|
|
|
\subsection{Input file}
|
|
|
|
An input file is simply a list of spdl constructions, which are global
|
|
declarations or protocol descriptions.
|
|
|
|
\begin{grammar}
|
|
|
|
<spdlcomplete> ::= <spdl> \{ ';' <spdl> \}
|
|
|
|
<spdl> ::= <globaldeclaration>
|
|
\alt <protocol>
|
|
% Only needed for modelchecker
|
|
%\alt `run' <roleref> `(' <termlist> `)' `;'
|
|
|
|
\end{grammar}
|
|
|
|
\subsection{Protocols}
|
|
|
|
A protocol is simply a container for a set of roles. Because
|
|
we use a role-based approach to describing roles, the protocol container
|
|
in fact only affects the
|
|
naming of the roles: a role ``I'' in a protocol ``ns3'' will internally be assigned the
|
|
name ``ns3.I''. This is used to make role names globally unique.
|
|
|
|
\begin{grammar}
|
|
|
|
<protocol> ::= `protocol' <id> `(' <termlist> `)' `{' <roles> `}' [ `;' ]
|
|
|
|
\end{grammar}
|
|
|
|
\subsection{Roles}
|
|
|
|
\begin{grammar}
|
|
|
|
<roles> ::= <role> [ <roles> ]
|
|
\alt <declaration> [ <roles> ]
|
|
|
|
<role> ::= [ `singular' ] `role' <id> `{' <roledef> `}' [ `;' ]
|
|
|
|
<roledef> ::= <event> [ <roledef> ]
|
|
\alt <declaration> [ <roledef> ]
|
|
|
|
\end{grammar}
|
|
|
|
\subsection{Events}
|
|
|
|
\begin{grammar}
|
|
|
|
<event> ::= `recv' <label> `(' <from> `,' <to> `,' <termlist> `)' `;'
|
|
\alt `send' <label> `(' <from> `,' <to> `,' <termlist> `)' `;'
|
|
\alt `claim' [ <label> ] `(' <from> `,' <claim> [ `,'
|
|
<termlist> ] `)' `;'
|
|
|
|
% Only needed for modelchecker
|
|
% <roleref> ::= <id> `.' <id>
|
|
|
|
<label> ::= `_' <term>
|
|
|
|
<from> ::= <id>
|
|
|
|
<to> ::= <id>
|
|
|
|
<claim> ::= <id>
|
|
|
|
|
|
\end{grammar}
|
|
\subsection{Declarations}
|
|
\begin{grammar}
|
|
|
|
<globaldeclaration> ::= <declaration>
|
|
\alt `untrusted' <termlist> `;'
|
|
\alt `usertype' <termlist> `;'
|
|
|
|
<declaration> ::= [ `secret' ] `const' <termlist> [ `:' <type> ] `;'
|
|
\alt [ `secret' ] `fresh' <termlist> [ `:' <typelist> ] `;'
|
|
\alt [ `secret' ] `var' <termlist> [ `:' <typelist> ] `;'
|
|
\alt `secret' <termlist> [ <type> ] `;'
|
|
\alt `inversekeys' `(' <term> `,' <term> `)' `;'
|
|
\alt `compromised' <termlist> `;'
|
|
|
|
<type> ::= <id>
|
|
|
|
<typelist> ::= <type> \{ `,' <type> \}
|
|
|
|
\end{grammar}
|
|
\subsection{Terms}
|
|
\begin{grammar}
|
|
|
|
<term> ::= <id>
|
|
\alt `{' <termlist> `}' <key>
|
|
\alt `(' <termlist> `)'
|
|
\alt <id> `(' <termlist> `)'
|
|
|
|
<key> ::= <term>
|
|
|
|
<termlist> ::= <term> \{ `,' <term> \}
|
|
|
|
|
|
\end{grammar}
|
|
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Modeling security protocols}
|
|
\label{sec:modeling}
|
|
%----------------------------------------------------------------------------
|
|
|
|
\begin{figure}[!htb]
|
|
\centering
|
|
\includegraphics{msc-ns}
|
|
\caption{A message sequence chart description}
|
|
\label{msc:ns3}
|
|
\end{figure}
|
|
|
|
\section{Introduction}
|
|
|
|
The correct modeling of a security protocol for analysis in the Scyther
|
|
tool requires a basic understanding of the underlying
|
|
symbolic model. This model is explained in detail in~\cite{opsembook}.
|
|
|
|
Roughly speaking, the symbolic analysis focuses on the following
|
|
aspects:
|
|
\begin{itemize}
|
|
|
|
\item Logical message components and their intended function within the
|
|
protocol (public versus
|
|
secret, freshly generated in each run or constant)
|
|
\item Message structure (pairing, encryption, signing, hashing)
|
|
\item Message flow (order, involved agents)
|
|
|
|
\end{itemize}
|
|
Many other elements are abstracted away. For example, bit strings are
|
|
abstracted into terms, bit strings that occur with negligble probability
|
|
are abstracted away, and more complext control flow constructs such as
|
|
loops are often unfolded for a (low) finite number of times.
|
|
|
|
%The initial step of modeling a protocol typically takes the most time of
|
|
%the verification process. Most protocols are not very well documented,
|
|
%and because we work here with abstracted protocols, it is very easy to
|
|
%make a wrong abstraction in the process and miss out on a crucial
|
|
%feature. Once the protocol is modeled, the issue of deciding which
|
|
%security properties need to be included is often also unclear. Secrecy
|
|
%of some terms is fairly straightforward, but informal notions of
|
|
%authentication are potential minefields, and should be carefully
|
|
%examined.
|
|
%
|
|
%Once this difficult phase is over, and we are left with a
|
|
%suitable abstracted protocol, the tools can be used to quickly find
|
|
%attacks on the protocol model. It is often easy to check whether an
|
|
%attack on the abstract protocol constitutes an attack on the real
|
|
%protocol.
|
|
|
|
%............................................................................
|
|
\section{Example: Needham-Schroeder Public Key}
|
|
|
|
As an example, we show how to model a simple protocol.
|
|
|
|
\index{Needham-Schroeder protocol}
|
|
\index{NS|see{Needham-Schroeder protocol}}
|
|
Figure~\ref{msc:ns3} depicts the Needham-Schroeder Public Key protocol.
|
|
For simplicity, we have only displayed the claim by each role
|
|
that the initiator nonce $\nI$ is secret.
|
|
|
|
We start off the protocol description by adding a multi-line
|
|
comment that describes the protocol and other interesting details.
|
|
Multi-line comments start with \spd{/*} and end with \spd{*/}.
|
|
\begin{spdl}[numbers=left]
|
|
/*
|
|
* Needham-Schroeder protocol
|
|
*/
|
|
\end{spdl}
|
|
|
|
The protocol uses the default public/private key infrastructure: an agent
|
|
\spd{A} has
|
|
a key pair \spd{(pk(A),sk(A))}.
|
|
|
|
The protocol has two roles: the
|
|
intiator role \spd{I} and the responder role \spd{R}. We also add a
|
|
single line comment, starting with \spd{//}.
|
|
\begin{spdl}[numbers=left,firstnumber=5]
|
|
// The protocol description
|
|
|
|
protocol ns3(I,R)
|
|
{
|
|
\end{spdl}
|
|
|
|
Scyther works with a role-based description of the protocols. We first
|
|
model the initiator role. This role has two values that are local to the
|
|
role: the nonce that is created by \spd{I} and the nonce that is
|
|
received. We have to declare them both.
|
|
\begin{spdl}[numbers=left,firstnumber=9]
|
|
role I
|
|
{
|
|
fresh ni: Nonce;
|
|
var nr: Nonce;
|
|
\end{spdl}
|
|
|
|
We now model the communication behaviour of the protocol.
|
|
Needham-Schroeder has three messages, and the initiator role sends the
|
|
first and last of these. Note the labels (\eg, \spd{\_1}) at the end of
|
|
the \spd{send} and \spd{recv} keywords: these serve merely to retain the
|
|
information of the connected arrows in the message sequence chart.
|
|
|
|
\begin{spdl}[numbers=left,firstnumber=14]
|
|
send_1(I,R, {I,ni}pk(R) );
|
|
recv_2(R,I, {ni,nr}pk(I) );
|
|
send_3(I,R, {nr}pk(R) );
|
|
\end{spdl}
|
|
|
|
\remark{CC}{This should be refactored, and moved to the next chapter.}
|
|
|
|
Finally, we add the security requirements of the protocol. Without such
|
|
claims, Scyther does not know\footnote{If you are unsure about the
|
|
claims, you can also use the \scr{--auto-claims} switch to automatically
|
|
generate these at run-time.} what needs to be checked.
|
|
|
|
Here we have chosen to check for secrecy of the generated and received
|
|
nonce, and will check for non-injective agreement and synchronisation.
|
|
\begin{spdl}[numbers=left,firstnumber=18]
|
|
claim_i1(I,Secret,ni);
|
|
claim_i2(I,Secret,nr);
|
|
claim_i3(I,Niagree);
|
|
claim_i4(I,Nisynch);
|
|
}
|
|
\end{spdl}
|
|
This completes the specification of the initiator role.
|
|
|
|
For this simple protocol, the responder role is very similar to the
|
|
initiator role\footnote{In general, the transformation is not that
|
|
simple, but for many protocols this will suffice.}. In fact, there are
|
|
only a few differences:
|
|
\begin{enumerate}
|
|
|
|
\item The keywords \spd{var} and \spd{fresh} have swapped places:
|
|
\spd{ni} was created by \spd{I} and a freshly generated value there, but for the role
|
|
\spd{R} it is the received value and thus a variable.
|
|
|
|
\item The keywords \spd{send} and \spd{recv} have swapped places.
|
|
|
|
\item The claims should have unique labels, so they have changed, and
|
|
the role executing the claim is now \spd{R} instead of \spd{I}.
|
|
|
|
\end{enumerate}
|
|
|
|
The complete role description for the responder looks like this:
|
|
\begin{spdl}[numbers=left,firstnumber=24]
|
|
role R
|
|
{
|
|
var ni: Nonce;
|
|
fresh nr: Nonce;
|
|
|
|
recv_1(I,R, {I,ni}pk(R) );
|
|
send_2(R,I, {ni,nr}pk(I) );
|
|
recv_3(I,R, {nr}pk(R) );
|
|
|
|
claim_r1(R,Secret,ni);
|
|
claim_r2(R,Secret,nr);
|
|
claim_r3(R,Niagree);
|
|
claim_r4(R,Nisynch);
|
|
}
|
|
}
|
|
\end{spdl}
|
|
|
|
The full protocol description file for the {\em Needham-Schroeder}
|
|
protocol is given in Appendix~\ref{app:ns3}.
|
|
|
|
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Specifying security properties}
|
|
\label{sec:properties}
|
|
%----------------------------------------------------------------------------
|
|
|
|
%\remark{CC}{This should synch up explicitly with the book chapter, and say
|
|
%where we deviate.}
|
|
|
|
\section{Specifying secrecy}
|
|
|
|
|
|
|
|
\section{Specifying authentication properties}
|
|
|
|
\subsection{Aliveness}
|
|
|
|
\subsection{Non-injective synchronisation}
|
|
|
|
\subsection{Non-injective agreement}
|
|
|
|
\subsection{Agreement over data}
|
|
\label{sec:agreement}
|
|
\spdindex{Commit}
|
|
\spdindex{Running}
|
|
\index{agreement on data}
|
|
\index{data agreement}
|
|
\index{non-injective agreement}
|
|
|
|
In order to specify data agreement, \eg, that the role $I$ agrees with
|
|
the role $R$ on a set of terms, \eg, the nonces
|
|
$ni$ and $nr$, one inserts two claims:
|
|
\begin{enumerate}
|
|
\item At the end of the $I$ role, insert
|
|
\spd{claim(I,Commit,R,ni,nr);}
|
|
\item In the $R$, just before the last send (in case
|
|
of a protocol with multiple roles: the last
|
|
send that
|
|
causally precedes the claim in the $I$ role),
|
|
insert
|
|
\spd{claim(R,Running,I,ni,nr);}
|
|
|
|
\end{enumerate}
|
|
For an example of the use of these claims, see the ``ns3.spdl'' input file in the Scyther
|
|
distribution. For a formal definition of the signals,
|
|
see~\cite{lowe97hierarchy}.
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Using the Scyther tool GUI}
|
|
\label{sec:gui}
|
|
%----------------------------------------------------------------------------
|
|
|
|
\index{GUI}
|
|
The Scyther tool can be used in two main ways. First, through the
|
|
graphical user interface (GUI) and second, through the command-line
|
|
interface. For most users the first option is preferred.
|
|
|
|
In this section we detail the Scyther output when used through the GUI.
|
|
|
|
%............................................................................
|
|
\section{Results}
|
|
|
|
As shown before, verifying the Needham-Schroeder public key protocol yields the
|
|
following results as in Figure~\ref{resultwindowbig}.
|
|
|
|
\begin{figure}[!htb]
|
|
\begin{center}
|
|
\includegraphics[width=\linewidth]{resultwindow}
|
|
\end{center}
|
|
\label{resultwindowbig}
|
|
\caption{Scyther results for the Needham-Schroeder protocol}
|
|
\end{figure}
|
|
|
|
The interpretation is as follows: all the claims of the initiator role
|
|
\spd{ns3,I} are correct for an unbounded number of runs.
|
|
|
|
Unfortunately, all the claims of the responder role are false. Scyther
|
|
reports that it found at least one attack for each of those four claims.
|
|
We could choose to view these attacks: this will be shown in
|
|
Section~\ref{sec:graphical}.
|
|
|
|
In the result window, Scyther will output a single
|
|
line for each claim. The line is divided into several columns. The first
|
|
column shows the protocol in which the claim occurs, and the second
|
|
shows the role. In the third column a unique claim identifier is shown,
|
|
of the form \scr{p,l}, where \scr{p} is the protocol and \scr{l} is the
|
|
claim label.\footnote{This includes the protocol name, which is important when
|
|
doing multi-protocol analysis.}. The fourth column displays the claim
|
|
type and the claim parameter.
|
|
|
|
Under the header \scr{Status} we find two columns.
|
|
The fifth column gives the actual result of the verification process: it
|
|
will yield \scr{Fail} when the claim is false, and \scr{Ok} when the
|
|
claim is correct.
|
|
The sixth column refines the previous statement: in some cases, the
|
|
Scyther verification process is not complete (which will be explored in
|
|
more detail in the next section). If this column states \scr{Verified},
|
|
then the claim is provably true. If the column states \scr{Falsified},
|
|
then the claim is provably false. If the column is empty, then the
|
|
statement of fail/ok depends on the specific bounds setting.
|
|
|
|
The seventh column, \scr{Comments}, serves to explain the status of the results
|
|
further. In particular, the column contains a single sentences. We
|
|
describe the possible results below.
|
|
|
|
\begin{itemize}
|
|
|
|
\item \scr{At least X attack(s)}
|
|
|
|
\index{at least X attack(s)}
|
|
Some attacks were found in the state space: however, due
|
|
to the undecidability of the problem, or because of the
|
|
branch and bround structure of the search, we cannot be
|
|
sure that there are no other attack states.
|
|
|
|
In the default setup, Scyther will stop the
|
|
verification process after an attack is found.
|
|
|
|
\item \scr{Exactly X attack(s)}
|
|
|
|
\index{exactly X attack(s)}
|
|
Within the statespace, there are exactly this many
|
|
attacks, and no others.
|
|
|
|
\item \scr{At least X pattern(s)}
|
|
\item \scr{Exactly X pattern(s)}
|
|
|
|
\index{exactly X pattern(s)}
|
|
\index{at least X pattern(s)}
|
|
These correspond exactly to the previous two, but occur
|
|
in case of a `\spd{Reachable}' claim. Thus, the states
|
|
that are found are not really attacks but classes of reachable
|
|
states.
|
|
|
|
\item \scr{No attacks within bounds}
|
|
|
|
\index{no attacks within bounds}
|
|
No attack was found within the bounded statespace, but there can
|
|
possibly be an attack outside the bounded statespace.
|
|
|
|
\item \scr{No attacks}
|
|
|
|
\index{no attacks}
|
|
\index{verification}
|
|
No attack was found within the (bounded or unbounded) statespace, and a proof
|
|
can be constructed that there is no attack even when the
|
|
statespace is unbounded. Thus, the security property has
|
|
been succesfully verified.
|
|
|
|
Note that because of the nature of the algorithm, this
|
|
result can even be obtained when the statespace is
|
|
bounded.
|
|
|
|
\end{itemize}
|
|
|
|
%............................................................................
|
|
\section{Bounding the statespace}
|
|
|
|
During the verification process, the Scyther tool explores a proof tree
|
|
that covers all
|
|
possible protocol behaviours. The default setting is to {\em bound} the
|
|
size of this tree in some
|
|
way, ensuring that the verification procedure terminates. However,
|
|
importantly, even if the size of this proof tree is bounded, unbounded
|
|
verification may still be achieved.
|
|
|
|
In most cases, the verification procedure will terminate and return
|
|
results before ever reaching the bound. However, if the verification procedure
|
|
reaches the bound, this is reported in the result window, \eg:
|
|
|
|
\begin{screen}
|
|
No attack within bounds
|
|
\end{screen}
|
|
|
|
This should be interpreted as: Scyther did not find any attacks, but
|
|
because it reached the bound, it did not explore the full tree, and it
|
|
is possible that there are still attacks on the protocol.
|
|
|
|
The default way of bounding the {\em maximum number of runs}, or protocol
|
|
instances. This can be changed in the \scr{Settings} tab of the main
|
|
window. If the maximum number of runs is, \eg, ~5, and Scyther reports
|
|
\scr{No attack within bounds}, this means that there exist no attacks
|
|
that involve 5 runs or less. However, there might exist attacks that
|
|
involve 6 runs or more.
|
|
|
|
For some protocols, increasing the maximum number of runs can lead to
|
|
complete results (i.e.~finding an attack or being sure that there is no
|
|
attack), but for other protocols the result will always be \scr{No
|
|
attack within bounds}.
|
|
|
|
Note that the verification time usually grows exponentially with respect
|
|
to the maximum number of runs.
|
|
|
|
%............................................................................
|
|
\section{Attack graphs}
|
|
\label{sec:graphical}
|
|
|
|
\index{attack graph}
|
|
\index{attack window}
|
|
In Figure~\ref{attackwindowbig} we show an attack window in more detail.
|
|
|
|
\begin{figure}[!htb]
|
|
\begin{center}
|
|
\includegraphics[scale=0.53]{attackwindow}
|
|
\end{center}
|
|
\label{attackwindowbig}
|
|
\caption{Scyther attack window}
|
|
\end{figure}
|
|
|
|
|
|
The basic elements are arrows and several kinds of boxes. The arrows in
|
|
the graph represent ordering constraints (caused by the
|
|
prefix-closedness of events in the protocol roles, or by dependencies in
|
|
the intruder knowledge). The boxes represent creation of a run,
|
|
communication events of a run, and claim events.
|
|
|
|
\subsection{Runs}
|
|
|
|
\index{run}
|
|
Each vertical axis represents a run (an instance of a protocol role).
|
|
Thus, in this attack we see that there are two runs involved. Each run
|
|
starts with a diamond shaped box. This represents the creation of a run,
|
|
and is used to give information about the run.
|
|
|
|
For the run on the left-hand side in the attack we have this information:
|
|
|
|
\begin{ingraph}
|
|
Run #1
|
|
Agent2 in role I
|
|
I -> Agent2
|
|
R -> Agent1
|
|
\end{ingraph}
|
|
|
|
Each run is assigned a run identifier (here 1), which is an arbitrary
|
|
number that enables us to uniquely identify each run. This run executes
|
|
the \gra{R} role of the protocol. It is being executed by an agent
|
|
called \gra{Agent1}, who thinks he is talking to \gra{Agent2}. Note that
|
|
although run 2 is being executed by \gra{Agent2}, this agent does not
|
|
believe he is talking to \gra{Agent1}.
|
|
|
|
\begin{ingraph}
|
|
Run #2
|
|
Agent2 in role I
|
|
I -> Agent2
|
|
R -> Eve
|
|
\end{ingraph}
|
|
|
|
In the run on the right, we see
|
|
This run
|
|
represents an instance of the role \gra{I}. From the second line we can
|
|
see which agent is executing the run, and who he thinks he is talking
|
|
to. In this example, the run is executed by an agent called
|
|
\gra{Agent2}, who thinks the responder role is being executed by the
|
|
untrusted agent \gra{Eve}.\footnote{Because this agent is talking to the
|
|
untrusted agent, of course all information is leaked, and no guarantees
|
|
can be given.}
|
|
|
|
Additionally, the run headers contain information on the freshly
|
|
generated values
|
|
(\eg, run 1 generates \gra{nr\#1}) and information on the
|
|
instantiation of the local variables (\eg, run 1 instantiates its
|
|
variable \gra{ni} with the nonce \gra{ni\#2} or run 2.
|
|
|
|
|
|
\subsection{Communication events}
|
|
|
|
\index{communication event}
|
|
Send events denote the sending of a message. The first send
|
|
occurs in this attack is the first send event of run 2.
|
|
|
|
\begin{ingraph}
|
|
send_1(Eve, { Agent#0, ni#2 }pk(Eve) )
|
|
\end{ingraph}
|
|
|
|
Every time a message is sent, it is effectively given to the intruder.
|
|
In this case, because the intruder knows the secret key \spd{sk(Eve)} of
|
|
the agent \gra{Eve}, he can decrypt the message and learns the value of
|
|
the nonce \gra{ni\#2}.
|
|
|
|
Receive events correspond to the successful reception of a message. The
|
|
first receive event that can
|
|
occur in this attack is the first receive event of run 0.
|
|
|
|
\begin{ingraph}
|
|
recv_1(Agent#0, { Agent#0, ni#2 }pk(Agent#1) )
|
|
\end{ingraph}
|
|
|
|
This tells us that the agent executing this run, \gra{Agent\#1}, reads a
|
|
message that is apparently coming from \gra{Agent\#1}. The message that
|
|
is received is \gra{\{ Agent\#0, ni\#2 \}pk(Agent\#1)} : the name of the
|
|
agent he thinks he is communicating with and the nonce \gra{ni\#2},
|
|
encrypted with his public key.
|
|
|
|
The incoming arrow does not indicate a direct sending of the message.
|
|
Rather, it denotes an ordering constraint: this message can only be
|
|
received
|
|
{\em after} something else has happened. In this case, we see that the
|
|
message can only be received after run 2 sends his initial message. The
|
|
reason for this is the nonce \gra{ni\#2}: the intruder cannot predict
|
|
this nonce, and thus has to wait until run 2 has generated it.
|
|
|
|
\index{construct}
|
|
In the graph the connecting arrow is red and has a label ``construct''
|
|
with it: this is caused by the fact that the message sent does not
|
|
correspond to the message that is received. We know the intruder can only
|
|
construct the message to be received after the sent message, and thus it
|
|
must be the case that he uses information from the sent message to
|
|
construct the message that is received. Other possibilities include a green
|
|
and a yellow arrow. A yellow arrow indicates that a message was sent,
|
|
and received in exactly the same form: however, the agents disagree about
|
|
who was sending a message to whom. It is therefore labeled with
|
|
``redirect'' because the intruder must have redirected the message. A
|
|
green arrow (not in the picture) indicating that a message is received
|
|
exactly the same as it was sent, representing a normal message
|
|
communication between two agents.
|
|
|
|
Note that a \spd{recv} event without an incoming arrow denotes that a term is
|
|
received that can be generated from the initial knowledge of the intruder.
|
|
There is no such event in the example, but this can occur often. For
|
|
example, if a role reads a plain message containing only an agent name,
|
|
the intruder can generate the term from his initial knowledge.
|
|
|
|
\subsection{Claims}
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Using the Scyther command-line tools}
|
|
\label{sec:cli}
|
|
%----------------------------------------------------------------------------
|
|
|
|
\index{command-line tools}
|
|
\index{GUI!using Scyther without GUI}
|
|
All of the features offered by the Scyther GUI are also available
|
|
through command-line tools. Additionally, the command-line tools offer
|
|
some features that currently cannot be accessed through the GUI.
|
|
|
|
Depending on your platform, the Scyther directory contains one of the following executables:
|
|
\begin{itemize}
|
|
\item \scr{Scyther/scyther-linux}
|
|
\item \scr{Scyther/scyther-w32}
|
|
\item \scr{Scyther/scyther-mac}
|
|
\end{itemize}
|
|
In the following, we assume that the linux version is used. If you have a different version, please replace \scr{scyther-linux} in the below by the executable for your platform.
|
|
|
|
To get a list of (some) of the command-line options, run the executable with the \scr{--help} switch, e.g.:
|
|
\begin{screen}
|
|
scyther-linux --help
|
|
\end{screen}
|
|
To analyze the Needham-Schroeder protocol and generate a .dot file (the input language for the Graphviz tool) for the attacks, use
|
|
\begin{screen}
|
|
scyther-linux --dot-output --output=ns3-attacks.dot ns3.spdl
|
|
\end{screen}
|
|
The resulting output file can then be rendered by graphviz, e.g.:
|
|
\begin{screen}
|
|
dot -Tpdf -O ns3-attacks.dot
|
|
\end{screen}
|
|
This yields several PDF files \scr{ns3-attacks.dot[.N].pdf} that contain the attack graphs.
|
|
|
|
To get a more complete list of command-line options, run the executable with the \scr{--expert --help} switch, e.g.:
|
|
\begin{screen}
|
|
scyther-linux --expert --help
|
|
\end{screen}
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Advanced topics}
|
|
\label{sec:advanced}
|
|
%----------------------------------------------------------------------------
|
|
|
|
\section{Modeling more than one asymmetric key pair}
|
|
\label{adv:asymmetric}
|
|
|
|
\index{multiple asymmetric key pairs per agent}
|
|
\index{asymmetric key!multiple pairs per agent}
|
|
Asymmetric keys are typically modeled as two functions: one function that maps
|
|
the agents to their public keys, and another function that maps agents to their
|
|
secret keys.
|
|
|
|
By default, each agent $x$ has a public/private key pair
|
|
$(\spd{pk(x)},\spd{sk(x)})$.
|
|
|
|
To model other asymmetric keys, we first define the two functions, which are
|
|
for example named \spd{pk2} for the public key function, and \spd{sk2} for the secret
|
|
key function.
|
|
\begin{spdl}
|
|
const pk2: Function;
|
|
secret sk2: Function;
|
|
\end{spdl}
|
|
|
|
We also declare that these functions represent asymmetric key pairs:
|
|
\begin{spdl}
|
|
inversekeys (pk2,sk2);
|
|
\end{spdl}
|
|
|
|
If defined in this way, a term encrypted with \spd{pk2(x)} can only be
|
|
decrypted with \spd{sk2(x)} and vice versa.
|
|
|
|
\section{Approximating equational theories}
|
|
|
|
\index{equational theories}
|
|
\index{exponentiation|see{Diffie-Hellman exponentiation}}
|
|
\index{Diffie-Hellman exponentiation}
|
|
\index{bidirectional keys}
|
|
\index{syntactic equality}
|
|
|
|
The operational semantics underlying Scyther currently only consider
|
|
syntactic equality: two (ground) terms are equal if and only if they are
|
|
syntactically equivalent. However, there are several common
|
|
cryptographic constructions that are more naturally modeled by using certain
|
|
equalities. For example:
|
|
\begin{enumerate}
|
|
\item $g^{ab} \; (\text{mod } N)$ and $g^{ba} \; (\text{mod }
|
|
N)$, to model Diffie-Hellman exponentiation.
|
|
\item $k(A,B)$ and $k(B,A)$, to model bidirectional long-term
|
|
keys.
|
|
\end{enumerate}
|
|
Although Scyther does not provide direct support for such equational
|
|
theories, there exists a straightforward underapproximation.
|
|
|
|
The core idea is that instead of modeling the term equality, we
|
|
provide the adversary with the ability to learn all terms in an
|
|
equivalence class if he learns one of its elements. For example, for
|
|
the equivalence class $\{ k(A,B), k(B,A) \}$ we can provide the
|
|
adversary with the ability to learn $k(B,A)$ from $k(A,B)$, and vice
|
|
versa. We can model this by introducing an appropriate helper protocol
|
|
(denoted by the prefix '@'):
|
|
\index{helper protocol}
|
|
\begin{spdl}
|
|
protocol @keysymmNaive(X) {
|
|
role X {
|
|
var Y: Agent;
|
|
|
|
recv_!1(X,X, k(X,Y) );
|
|
send_!2(X,X, k(Y,X) );
|
|
}
|
|
}
|
|
\end{spdl}
|
|
Because the role can be instantiated for any agents $X$ and $Y$, this
|
|
covers all possible combinations of agents.
|
|
|
|
The above naive approximation can be significantly improved. One
|
|
obvious and practically relevant
|
|
omission is that the adversary usually learns encrypted messages, but
|
|
not the key. In such cases, we still would like to model
|
|
that \spd{\{ m \}k(A,B)} = \spd{\{ m \}k(B,A)}. Thus we adapt our helper
|
|
protocol:
|
|
\begin{spdl}
|
|
protocol @keysymmInefficient(X,Y) {
|
|
role X {
|
|
var Y: Agent;
|
|
|
|
recv_!1(X,X, k(X,Y) );
|
|
send_!2(X,X, k(Y,X) );
|
|
}
|
|
role Y {
|
|
var X: Agent;
|
|
var m: Ticket;
|
|
|
|
recv_!1(Y,Y, { m }k(X,Y) );
|
|
send_!2(Y,Y, { m }k(Y,X) );
|
|
}
|
|
}
|
|
\end{spdl}
|
|
If the protocol contains further terms in which the symmetric keys
|
|
appear in other positions, such as in nested encryptions or hashes, we
|
|
would add further roles.
|
|
\remark{CC}{Maybe add pointer to more elaborate example in appendix?}
|
|
|
|
The above approximation is often inefficient in practice.
|
|
We can improve performance by making the helper protocol rules more
|
|
tight, \ie, by exploiting more type information about the protocol.
|
|
For example, if the protocol transmits two types of encrypted messages:
|
|
\begin{enumerate}
|
|
\item \spd{ \{ I,nI,nR \}k(I,R) }, and
|
|
\item \spd{ \{ nI \}k(I,R) },
|
|
\end{enumerate}
|
|
then we would modify the helper protocol in the following way:
|
|
\begin{spdl}
|
|
protocol @keysymm(X,Y,Z) {
|
|
role X {
|
|
var Y: Agent;
|
|
|
|
recv_!1(X,X, k(X,Y) );
|
|
send_!2(X,X, k(Y,X) );
|
|
}
|
|
role Y {
|
|
var X,Z: Agent;
|
|
var n1,n2: Nonce;
|
|
|
|
recv_!1(Y,Y, { Z,n1,n2 }k(X,Y) );
|
|
send_!2(Y,Y, { Z,n1,n2 }k(Y,X) );
|
|
}
|
|
role Z {
|
|
var X,Y: Agent;
|
|
var n1: Nonce;
|
|
|
|
recv_!1(Z,Z, { n1 }k(X,Y) );
|
|
send_!2(Z,Z, { n1 }k(Y,X) );
|
|
}
|
|
}
|
|
\end{spdl}
|
|
In general, one would manually inspect the protocol and extract all
|
|
positions in which a term from an equivalence class occurs as a subterm.
|
|
For each of these positions, we model an appropriate role in the helper
|
|
protocols.
|
|
|
|
This is also used to model, for example, Diffie-Hellman
|
|
exponentiation. For exponentiation we introduce an abstract function
|
|
symbol, \eg, \spd{exp}, and a public constant \spd{g}. We then introduce
|
|
a helper protocol with roles to model that
|
|
\spd{exp(exp(g,X),Y)} =
|
|
\spd{exp(exp(g,Y),X)}.
|
|
|
|
In practice, this type of underapproximation has proven to be extremely
|
|
effective, to the point that all known attacks on real-world protocols
|
|
that can be modeled using the ``real'' equational theory, are found by
|
|
Scyther when using the underapproximation.
|
|
|
|
One caveat is that while this approximation works well for secrecy and
|
|
data-agreement, it can cause message-based agreement properties (such as
|
|
synchronisation) to fail, because their message equality checks are
|
|
syntactical. These checks are not affected by the introduction of helper
|
|
protocols.
|
|
|
|
%\section{Approximating undirected symmetric long-term keys}
|
|
% $k(A,B) = k(B,A)$
|
|
% Refer back to helper protocols
|
|
|
|
%\section{Approximating Diffie-Hellman}
|
|
% Refer back to helper protocols
|
|
|
|
% \section{Modeling internal checks}
|
|
%
|
|
% \index{internal checks}
|
|
% \index{pattern matching}
|
|
% In most protocol models, the internal checks that a party performs
|
|
% when receiving a message are modeled by the pattern matching in the
|
|
% receive event. However, in some cases, this is not directly possible.
|
|
% For example, consider a protocol in which \spd{R} first receives
|
|
% an encrypted message \spd{\{knownString\}tempkey} that contains a
|
|
% specific constant encrypted with a fresh symmetric key. However,
|
|
% because $R$ does not have the key yet, he cannot decrypt the message,
|
|
% and simply stores the whole message in a variable \spd{T} of type Ticket. When
|
|
% \spd{R} later receives the key \spd{tempkey}, we would like to check that the message we
|
|
% received previously indeed is an encryption of the constant with the
|
|
% key, and abort if this is not the case. How can we model this?
|
|
%
|
|
% What we would need in this case is an internal check that \spd{T} is
|
|
% equal to $\{knownString\}tempkey$. For example, we would like to have
|
|
% an
|
|
% event ``\spd{match(X,Y)}'' whose intuitive semantics are: if the pattern
|
|
% \spd{X} matches the ground term \spd{Y}, then proceed with those variable
|
|
% instantiations. If they cannot be unified, the event is blocked and will
|
|
% not be executed. Using such an event, we can trivially implement the
|
|
% above check.
|
|
%
|
|
% Such a \spd{unify} event can be implemented in a role \spd{R} by the following
|
|
% specification:
|
|
% \begin{spdl}
|
|
% fresh newmatchkey: Nonce;
|
|
% send_!newlabel(R,R, { Y }newmatchkey);
|
|
% recv_!newlabel(R,R, { X }newmatchkey);
|
|
% \end{spdl}
|
|
% Note that \spd{newmatchkey} and \spd{newlabel} can have any value, as
|
|
% long as they do not occur anywhere else in the protocol specification.
|
|
% If a protocol implements multiple \spd{unify} events, then each of these
|
|
% should use distinct term and label names.
|
|
%
|
|
% This construction works because the fresh key is only used once. The
|
|
% adversary cannot learn the key; subsequently, there will be exactly one
|
|
% message that possibly matches the receive event.
|
|
%
|
|
% \index{delayed decryption}
|
|
% \index{committing to a term}
|
|
% \index{commit functionality}
|
|
% Using the above construction, protocols with delayed decryption, or that
|
|
% use hashes to implement ``committing to a term'' (commit functionality), can be modeled in a
|
|
% straightforward fashion.
|
|
|
|
\section{Modeling time-stamps and global counters}
|
|
\index{time-stamps|(}
|
|
\index{counter|see{global counter}}
|
|
\index{global counter|(}
|
|
|
|
Scyther's underlying protocol model currently does not provide support
|
|
for variables that are shared among the runs of an agent. Effectively, each run
|
|
starts with a ``clean slate'', independent of any runs that have been
|
|
executed previously. In other words, globally update state can not be
|
|
modeled directly.
|
|
|
|
In the following sections we provide some modeling approaches for
|
|
common problems.
|
|
|
|
\subsection{Modeling global counters}
|
|
|
|
Globally incremented counters can be modeled using freshly generated
|
|
values. This ensures
|
|
that each run uses a different value. The model is coarse in the sense
|
|
that the recipient of such a
|
|
counter cannot check that it is the successor of the previous
|
|
value of the counter.
|
|
|
|
\index{global counter|)}
|
|
|
|
\subsection{Modeling time-stamps using nonces}
|
|
|
|
There are at least two ways to model time-stamps.
|
|
|
|
The first model
|
|
is more appropriate for protocols where the probability that a given
|
|
time-stamp value is accepted by two runs is very low. This occurs when
|
|
time-stamps have great precision or when two runs occur only
|
|
sequentially, possibly with some delay time in between.
|
|
In this case, one can model time-stamps as freshly generated values,
|
|
\eg, nonces. To cater for the fact that the adversary typically knows
|
|
the time (and thus can also predict time-stamps), we prepend a
|
|
send event to the role that provides the adversary with the value of the
|
|
time-stamp that will be used. For example, we would
|
|
prepend the send with label \spd{!T1} for time-stamp \spd{T1} as in the
|
|
following example:
|
|
\begin{spdl}
|
|
usertype Timestamp;
|
|
|
|
protocol MyProtocol(Server,Client) {
|
|
role Server{
|
|
fresh T1: Timestamp;
|
|
|
|
/* Time-stamps are unique per run */
|
|
send_!T1(Server, Server, T1);
|
|
|
|
...
|
|
/* Server uses time-stamp value */
|
|
send_2(Server,Client, { Server, T1 }pk(Client) );
|
|
...
|
|
}
|
|
}
|
|
\end{spdl}
|
|
|
|
\subsection{Modeling time-stamps using variables}
|
|
|
|
The second model is more appropriate when it is reasonable that two runs
|
|
may accept the same time-stamp value. This is common for coarse
|
|
time-stamps, or for roles that are typically executed with high
|
|
parallelism, such as server roles. In such cases, one can instead model
|
|
timestamps as values that are determined by the adversary.
|
|
In contrast to the previous solution, this is done by prepending a
|
|
receive event. For example:
|
|
\begin{spdl}
|
|
usertype Timestamp;
|
|
|
|
protocol MyProtocol(Server,Client) {
|
|
role Server{
|
|
var T1: Timestamp;
|
|
|
|
/* Adversary chooses time-stamp value */
|
|
recv_!T1(Server, Server, T1);
|
|
|
|
...
|
|
/* Server uses time-stamp value */
|
|
send_2(Server,Client, { Server, T1 }pk(Client) );
|
|
...
|
|
}
|
|
}
|
|
\end{spdl}
|
|
|
|
|
|
|
|
\index{time-stamps|)}
|
|
|
|
|
|
\section{Multi-protocol attacks}
|
|
\label{sec:pma}
|
|
\index{multi-protocol attacks}
|
|
\index{cross-protocol attacks}
|
|
\index{chosen protocol attacks}
|
|
|
|
Scyther can be used to check for so-called \emph{multi-protocol attacks} (closely related concepts are \emph{cross-protocol attacks} and \emph{chosen protocol attacks}). These attacks depend on the interactions between different (sub)protocols: sometimes the adversary can use messages or message components from one protocol to attack another. For more information on this type of attack we refer to~\cite{Cr2006multiprotocol,kelsey97protocol}.
|
|
|
|
The easiest way to check for multi-protocol attacks in Scyther is to combine two protocol descriptions into a single file, i.e., create a new \scr{.spdl} file and paste into this file two other \scr{.spdl} files. The resulting file models an environment in which both protocols are running. Use Scyther to evaluate the claims in the combined file.
|
|
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Further reading}
|
|
\label{sec:further}
|
|
%----------------------------------------------------------------------------
|
|
|
|
% Note: this chapter should contain further reading that is purely tool
|
|
% related, such as protocol overviews, etc.
|
|
|
|
|
|
%==========================================================================
|
|
\bibliographystyle{plain}
|
|
\bibliography{biblio}
|
|
%==========================================================================
|
|
|
|
\appendix
|
|
|
|
|
|
%----------------------------------------------------------------------------
|
|
\chapter{Full specification for Needham-Schroeder public key}
|
|
\label{app:ns3}
|
|
%----------------------------------------------------------------------------
|
|
|
|
\begin{spdl}
|
|
/*
|
|
* Needham-Schroeder protocol
|
|
*/
|
|
|
|
|
|
// The protocol description
|
|
|
|
protocol ns3(I,R)
|
|
{
|
|
role I
|
|
{
|
|
fresh ni: Nonce;
|
|
var nr: Nonce;
|
|
|
|
send_1(I,R, {I,ni}pk(R) );
|
|
recv_2(R,I, {ni,nr}pk(I) );
|
|
claim(I,Running,R,ni,nr);
|
|
send_3(I,R, {nr}pk(R) );
|
|
|
|
claim_i1(I,Secret,ni);
|
|
claim_i2(I,Secret,nr);
|
|
claim_i3(I,Alive);
|
|
claim_i4(I,Weakagree);
|
|
claim_i5(I,Commit,R,ni,nr);
|
|
claim_i6(I,Niagree);
|
|
claim_i7(I,Nisynch);
|
|
}
|
|
|
|
role R
|
|
{
|
|
var ni: Nonce;
|
|
fresh nr: Nonce;
|
|
|
|
recv_1(I,R, {I,ni}pk(R) );
|
|
claim(R,Running,I,ni,nr);
|
|
send_2(R,I, {ni,nr}pk(I) );
|
|
recv_3(I,R, {nr}pk(R) );
|
|
|
|
claim_r1(R,Secret,ni);
|
|
claim_r2(R,Secret,nr);
|
|
claim_r3(R,Alive);
|
|
claim_r4(R,Weakagree);
|
|
claim_r5(R,Commit,I,ni,nr);
|
|
claim_r6(R,Niagree);
|
|
claim_r7(R,Nisynch);
|
|
}
|
|
}
|
|
\end{spdl}
|
|
|
|
%==================================================
|
|
\chapter{Obsolete constructions}
|
|
|
|
\section{Read event}
|
|
\spdindex{read}%
|
|
Note that in some protocol description files one may find the \spd{read}
|
|
keyword: this is obsolete syntax and can safely be substituted by
|
|
\spd{recv}.
|
|
|
|
|
|
|
|
%==================================================
|
|
|
|
\printindex
|
|
|
|
\end{document}
|