% PWC2003 
% http://www.iit.cnr.it/pwc2003/papers.html
% Full papers due: February 10, 2003
% Notification: May 10, 2003
% Camera Ready due: June 10, 2003
% Submitted papers should be approximately 20 double-spaced pages (use times 12pt
% as a reference). The cover page must contain an abstract of about 150 words,
% 3-5 keywords, name and affiliation of author(s) as well as the correspondence
% author's e-mail, telephone number, fax number and postal address. Because of
% the size limitation on the final manuscript, and to ensure that the reviewed
% paper and the final version have a similar size, please take into
% consideration that the final manuscript should be approximately 5000 words
% including tables and figures (each table and figure corresponds to 200 words).
% To make it easy to adhere to the final formatting standard use as a reference
% a 12-page manuscript formatted with the Springer-Verlag LNCS formatting
% standard, http://www.springer.de/comp/lncs/authors.html.
%
% My protocol design methodology
% 1. When sending a message, always identify itself, but not necessarily the
% receiver

\documentclass[runningheads]{llncs}
%In order to omit page numbers and running heads
%please use the following line instead of the first command line:
%\documentclass{llncs}.
%Furthermore change the line \pagestyle{headings} to
%\pagestyle{empty}.
\usepackage[dvips]{graphicx}
\usepackage[dvips]{color}
\usepackage{url}
\usepackage{tabularx}
\usepackage[fleqn]{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{bar}
\usepackage{ecltree}
\usepackage{epic}

\graphicspath{{figures/}}
\newcommand{\gl}[1]{\textbf{\footnotesize{\fontfamily{cmss}\fontseries{sbc}\selectfont #1}}}

\input{psfig.sty}

\begin{document}

\pagestyle{headings}
%In order to omit page numbers and running heads
%please change this line to
%\pagestyle{empty}
%and change the first command line too, see above.

\mainmatter

\title{The Design and Verification of a Decentralized Key Management Architecture for Wireless Sensor Networks}
%\titlerunning{Lecture Notes in Computer Science}
%\author{Alfred Hofmann\inst{1}
%\and Ingrid Beyer\inst{1} \and
%Anna Kramer\inst{1} \and Erika Siebert-Cole\inst{1} \and\\
%Angelika Bernauer-Budiman\inst{2} \and
%Martina Wiese\inst{2} \and Anita B\"urk\inst{3}}
%\author{Yee Wei Law\inst{1} \and Ricardo Corin\inst{1} Roberto Di Pietro\inst{2}
%\and Sandro Etalle\inst{1} \and Pieter H. Hartel\inst{1}}
\author{Yee Wei Law \and Ricardo Corin \and Sandro Etalle \and Pieter H. Hartel}
%\authorrunning{Alfred Hofmann et al.}

%\institute{Springer-Verlag, Computer Science Editorial III,
%Postfach 10 52 80,\\
%69042 Heidelberg, Germany\\
%\email{\{Hofmann, Beyer, Kramer, Erika.Siebert-Cole, LNCS\}@Springer.de}\\
%\texttt{http://www.springer.de/comp/lncs/index.html}
%\and
%Springer-Verlag, Computer Science Production, Postfach 10 52 80,\\
%69042 Heidelberg, Germany\\
%\email{\{Bernauer, Wiese\}@Springer.de}
%\and
%Springer-Verlag, Marketing Management, Postfach 10 52 80,\\
%69042 Heidelberg, Germany\\
%\email{Buerk@Springer.de}}
\institute{
Faculty of Electrical Engineering, Mathematics and Computer Science
\\
University of Twente, 7512 BM Enschede, The Netherlands
\footnote{Partially sponsored by the European Union as part of the
EYES project IST-2001-34734 (\url{http://eyes.eu.org}).}
\\
\email{\{ywlaw, corin, etalle, pieter\}@cs.utwente.nl}
%\and
%Dipartimento di Scienze dell'Informazione\\ 
%Universit{\`a} di Roma ``La Sapienza'', Via Salaria 113, 00198 Roma, Italy\\
%\email{dipietro@dsi.uniroma1.it}
}

\maketitle

\begin{abstract}
% what is the purpose of this paper
% what have we achieved
As part of the EnergY-Efficient Sensor networks (EYES) project ()
\end{abstract}

\section{Introduction}
% why?
Key management is the process by which keys are generated, stored, protected,
transferred, loaded, used, and destroyed. Key management is a challenging
problem for wireless sensor networks (WSNs) due to the hardware constraints of
the sensors and the dynamic nature of WSNs themselves. The hardware constraints
of sensors are in terms of~\cite{dipietro02secure}:
\begin{enumerate}
\item \textbf{Cost}: Sensors are generally not made tamper-resistant.

\item \textbf{Space}: They can only store as many keys as are usually allowed by the
remaining storage left over by the operating system and application code, which
is not much.

\item \textbf{Energy}: They need to optimize the use of cryptography
since cryptographic operations tend to be resource-intensive.  Ideally, the amount of
expended resouces should be proportional to the intended level of security (the
quantification of which is outside the scope of this paper).

\item \textbf{Time}: Public-key cryptography should be avoided or at least
limited to applications which are not time-constrained, because they are a few
order of magnitude more resource and time consuming than symmetric-key
cryptography~\cite{brown00pgp}. 
\end{enumerate}

The security and functional requirements of WSNs are such that under the above
constraints, the following guidelines need to be complied with:
\begin{enumerate}
\item \gl{NO\_SINGLE\_KEY}: The system should not operate on a system-wide key
(or keys).  Due to the sensor nodes' lack of tamper-resistance, having a
vulnerable system-wide key is \emph{not} better than having no key at all. 

\item \gl{NO\_SINGLE\_POINT}: The system should not have a single point (e.g.
node) of vulnerability.

\item \gl{SCALABILITY}: The system should be scalable in the sense that the
addition of new nodes would not cause excessive rise in computation, communication
and administrative overhead in the network.

\item \gl{ROUTING\_DEPENDENCE}: The system should not assume the underlying routing
protocol to be secure lest the inter-dependency of the key management and
routing architecture becomes a design deadlock. 

\item \gl{BIDIRECTIONALITY}: The system, to be realistic, should not assume
radio links to be bidirectional (see \ref{sec:bidirectionality}).

% this is not necessary in this paper:
%\item The system, for the highest level of security, should not rely on
%cryptography alone. Due to their tamper-irresistant nature, no nodes can be
%ascertained to be secure. Crypto-supplementary means such as monitoring and
%intrusion detection are necessary. 
%Consider the case of ActiveCX attack in Hu et al.'s~\cite{hu01ariadne}.
%Monitoring is required~\cite{marti00mitigating}.  
\end{enumerate}

As of writing, we are not aware of any key management architecture that
satisfies all the above hardware constraints as well as the guidelines.  Take for
example Basagni et al's proposal~\cite{basagni01secure}. In this proposal ,
sensors are assumed to be tamper-resistant (contrary to our assumption) and
share a network-wide system key. Although repeated key refreshment (aka
re-keying) would thwart cryptanalytic attampts on the traffic encryption key,
the compromise of a single node compromises the system key and thus the whole
network, leading to the violation of guideline \gl{NO\_SINGLE\_KEY} and
\gl{NO\_SINGLE\_POINT}. Morever, the clustering mechanism violates guideline
\gl{BIDIRECTIONALITY}. The proposal does not specify any routing scheme.

Perrig et al's testbed for the SPINS protocol suite possesses a single point of
vulnerability that is the base station~\cite{perrig01spins}, violating guideline
\gl{NO\_SINGLE\_POINT} in addition to \gl{SCALABILITY}. Authenticated routing
has been proposed as an application of the SPINS protocols but at the expense of
violating guideline \gl{BIDIRECTIONALITY}.

%In this paper, we focus on key deployment, i.e. how keys are deployed (or
%strategically distributed) on the sensor nodes before the nodes themselves are
%deployed. 

% what do we contribute
Our contribution is twofold. Our decentralized key management architecture,
which we call EYES Security Architecture 1 (ESA1), satisfies all the above
hardware constraints and architecture guidelines. In addition, authenticated
routing is directly implementable on top of the architecture, allowing an
integrated security architecture to be specified (and to be described in a later
paper).  Last but not least, all the protocols employed in our architecture have
been verified using Corin and Etalle's tool~\cite{corin02improved}. The
verification results imply that our protocols are secure in our standard set of
test scenarios (see Section~\ref{sec:usage}).

%\begin{itemize}
%\item Simple: The architecture is based on the well-known concepts of
%supervisors and clustering (Section~\ref{sec:overview}), the two-tier
%hierarchical architecture (Section~\ref{sec:overview}) is more amenable to
%analysis and easier to be adapted to other system requirements.

%\item Feasible: The design exerts no exotic requirements on the topology (e.g.
%must be arranged in hexagonal grids~\cite{slijepcevic02communication}) and the
%hardware (e.g. tamper-resistant hardware~\cite{basagni99distributed}) of the
%system.

%\item Practical: The design is based on realistic and explicit system
%assumptions as laid out earlier.  
%e.g. links are possibly unidirectional links
%(Section~\ref{sec:comm}), underlying routing protocol is possibly insecure
%(Section~\ref{sec:comm}), nodes are mobile (Section~\ref{sec:migration}).

%\item Flexible: Inter-cluster trust relationships are multi-level and
%application-adjustable (Section~\ref{sec:comm}). Both unicast and multicast
%are support (Section~\ref{sec:comm}).

%\item Scalable: There is no single point of control in the sensor network and
%the network is cluster-wise expandable (Section~\ref{sec:overview}).

%\item Verified: All cryptographic protocols employed in the architecture have
%been verified using Corin and Etalle's protocol analyzer~\cite{corin02improved}.
%\end{itemize}

\paragraph{Overview} In this paper, we discuss our key management architecture
in three inter-related aspects: (1) key deployment
(Section~\ref{sec:deployment}): the strategic distribution of keys on sensor
nodes during the bootstrap phase; (2) key refreshment (Section~\ref{sec:rekey}):
the refreshment of keys for increasing the cryptanalytic attack threshold and
birthday attack threshold; (3) key usage (Section~\ref{sec:usage}): the usage
scheme of keys for establishing secure channels.  Section~\ref{sec:related}
discusses important related work.  Section~\ref{sec:conclusion} concludes and
wraps up with a list of future work.

%Section~\ref{sec:overview} provides an overview of the cluster-based
%architecture. Section~\ref{sec:comm} drills into the details of intra- and
%inter-cluster communication.

\paragraph{Notation} To simplify the discussion below, we are using the
following standard notation:
\begin{itemize}
    \item $E_{K}(M)$ represents the ciphertext as a result of encrypting
    plaintext $M$ with key $K$.

    \item $MAC_{K}(M)$ represents the message authentication code (MAC) of
    message $M$ using key $K$.
    
    \item If $A,B \in \{0,1\}^*$, then $A|B$ is their concatenation.
\end{itemize}
and the following non-standard notation:
\begin{itemize} 
    \item $A \rightsquigarrow B$: $B$ is within the radio range of $A$, or $A$'s
    transmission reaches $B$ in a single hop but not necessarily vice versa.
    
    \item $A \leftrightsquigarrow B$: $A$ and $B$ are within each other's radio
    range.  
\end{itemize}
Warning: for the ease of reading, a different naming scheme is used in the
protocol description in Section~\ref{sec:usage} than that is used in
Secion~\ref{sec:deployment}.


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\section{Key Deployment}\label{sec:deployment}

\begin{figure}[ht]
    \begin{minipage}{0.6\linewidth}
    \centering
    \includegraphics[scale=0.75]{arch1.eps}    
    \end{minipage}
    \begin{minipage}{0.4\linewidth}
    \centering
    \footnotesize 
    \begin{bundle}{$D$}
        %\drawwith{\dashline{3}}
        %\thicklines
        \chunk{%
            \begin{bundle}{$S$}
                \chunk{$N$}
                \chunk{$N$}
                \chunk{...}
            \end{bundle}
        }
        \chunk{%
            \begin{bundle}{$S$}
                \chunk{$N$}
                \chunk{$N$}
                \chunk{...}
            \end{bundle}
        }
        \chunk{%
            \begin{bundle}{...}
                \chunk{$N$}
                \chunk{...}
            \end{bundle}
        }
    \end{bundle}
    \normalsize
    \end{minipage}    

    \begin{minipage}{0.6\linewidth}
    \begin{center}\bigskip(a)\end{center}
    \end{minipage}
    \begin{minipage}{0.4\linewidth}
    \begin{center}\bigskip(b)\end{center}
    \end{minipage}    
    \caption{\label{fig:arch1}(a) Key deployment in ESA1 (where $N^i_j
    \{K^i,K^i_j\}$ means node $N^i_j$ with keys $K^i,K^i_j$; dashed lines
    represent supervisors' radio range). (b) Three-tier hierarchy: $D$=Domain,
    $S$=Supervisor, $N$=Node.}
\end{figure}

%defined differently than the conventional concept of cluster
In ESA1, the key deployment scheme is superimposed on a structure of supervised
and unsupervised clusters. A supervised cluster consists of a supervisor node
(e.g. $S^\alpha$ and $S^\beta$ in Figure~\ref{fig:arch1}) and a group of
supervised nodes (e.g. $N^\alpha_1$, $N^\beta_1$ and $N^\beta_2$ in
Figure~\ref{fig:arch1}). The supervisor is usually a tamper-resistant Rich
Uncle~\cite{carman00constraints} while the supervised nodes are normal sensor
nodes. The key deployment scheme is such that every supervised node $N^\alpha_j$
($1<j<n$) of cluster $\alpha$ is equipped with a unique \emph{node key}
$K^\alpha_j$ and the supervisor $S^\alpha$ is equipped with the individual keys
of all the supervised nodes of its cluster.  Additionally $S^\alpha, N^\alpha_1,
\ldots, N^\alpha_n$ share the same \emph{cluster key} $K^\alpha$. The cluster
key is a backup key that is only used when the supervisor is not available, in
which case the supervised cluster downgrades to an unsupervised cluster.
Therefore in contrast to what Figure~\ref{fig:arch1} might suggest, although the
cluster boundary is defined by the radio range of the supervisor, the cluster
membership is not -- the membership of node $N$ in cluster $\alpha$ depends on
(1) whether there is a shared key between $N$ and $S^\alpha$; and (2) whether
$N$ possesses the cluster key $K^\alpha$. The design is optimized for the common
case when a supervised node $N^\alpha_j$ remains in the cluster of its
supervisor, or its \emph{home cluster}, i.e. when $S^\alpha \rightsquigarrow
N^\alpha_j$.  When a supervised node (e.g. $N^\beta_1$ in
Figure~\ref{fig:arch1}) roams out of its home cluster into another cluster,
called a \emph{foreign cluster}, it is said to have migrated. Staying in the
home cluster avoids the overhead and security risk associated with migration
(Section~\ref{sec:usage}), as well as facilitates intrusion detection which
however has to be discussed in a later paper. 

To establish trust between supervisors, we leave two options open. The first
option involves a further domain tier higher in the hierarchy
(Figure~\ref{fig:arch1}(b)), and it is to connect all the supervisors at
bootstrap to a \emph{domain controller}. The domain controller partitions the
set of supervisors into \emph{domains}. Only supervisors that belong to the same
domain are given the same domain key (a symmetric key) and thus share the common
trust. This scheme uses only symmetric cryptography but can only facilitate a
static and coarse notion of trust. The second option is to resort to SSL/TLS
(which uses public-key cryptography) to secure communication between supervisors.
This scheme facilates flexible and fine-grained access control at the expense of
higher overhead and energy consumption. All in all, the suitability of each of
these two options depends on the construction of the supervisors and the actual
application scenario. In this paper, we focus on the node/cluster tiers of the
hierarchy.

%As shall be seen later, the biggest benefit is reaped when a
%supervised node $N^i_j$ remains in the cluster of its supervisor, or its
%\emph{home cluster}, i.e. when $S^i \rightsquigarrow N^i_j$.

%The cluster boundary becomes significant in the context of intrusion detection
%scheme which however is out of scope of this paper. 

An unsupervised cluster consists only of unsupervised nodes (e.g. $N^\gamma_1$
in Figure~\ref{fig:arch1}), which usually are just normal sensor nodes.  In an
unsupervised cluster $\gamma$, every node shares the same cluster key
$K^\gamma$.  Unlike supervised clusters, for unsupervised clusters, a cluster
boundary is meaningless. Cluster membership depends solely on the possession of
$K^\gamma$.

\paragraph{Intruder Model} In relation to this key deployment scheme, our
intruder model extends that of Dolev and Yao's (wherein the intruders have full
capability of listening, intercepting, modifying, forging any message -- or
equivalently, the network can be identified as the intruder
itself~\cite{dolev83security}) with the possibility of any node except the
supervisors being compromised. Here, by compromise we mean the exposure of keys
(individual key and cluster key for supervised nodes, and cluster key for
unsupervised nodes), and/or the modification of program code. 
 
\paragraph{Security Objectives} What we do not tackle in this
paper is denial-of-service attacks like jamming (one of the toughest enemies of
WSNs and even the ubiquitous IEEE 802.11~\cite{stahlberg00radio}) and arbitrary
routing disruption~\cite{hu02ariadne}. What we do
indeed tackle is the confidentiality and authentication (implying integrity)
requirements of differennt modes of communications in our architecture.  First,
we define two \emph{security realms}: the set of all unsupervised clusters
constitute an unsupervised realm, while the set of all supervised clusters
constitute a supervised realm. Our security objectives can be grouped as follows
(in the following, a secure communication or secure channel means a
communication channel which is authenticated and optionally confidential, i.e.
depending on application requirements): 
\begin{itemize}
    \item In the supervised realm, secure \emph{node-to-node} communication
    within a single supervised cluster, as well as between different supervised
    clusters are facilitated for which \emph{intra-supervised cluster keying} 
    and respectively \emph{inter-supervised cluster keying} are used to
    establish the session keys. In these modes of communication, the effect of
    any node's compromise is isolated, i.e. if a supervised node $N^\alpha_1$ is
    compromised, only sessions that involve $N^\alpha_1$ are compromised. When
    $N^\alpha_1$ with node key $K^\alpha_1$ and of cluster $\alpha$ supervised
    by $S^\alpha$ migrates to a foreign cluster $\beta$ supervised by $S^\beta$,
    $N^\alpha_1$ must allow $S^\beta$ to acquire $K^\alpha_1$ (actually a key
    $derived(K^\alpha_1)$ derived from $K^\alpha_1$) from $S^\alpha$, so that
    (1) $N^\alpha_1$ is able to set up secure channels with members of cluster
    $\beta$ using intra-supervised cluster keying, and (2) $N^\alpha_1$ is still
    able to set up secure channels with member of other clusters using
    inter-supervised cluster keying. This mechanism is called \emph{key
    migration}. We have to emphasize that by migration, we actually mean that it
    is the key $derived(K^\alpha_1)$ that migrates, while $K^\alpha_1$ always
    stays with $S^\alpha$. 
    
    % Messy draft:
    %Key migration makes sure that whichever foreign cluster $A$ goes to, as
    %long as there is trust between $S_A$ and the supervisor of the foreign
    %cluster, let's say $S_B$, $A$ is able to set up secure channels with the
    %nodes of its home cluster as well as any node of the other foreign
    %clusters.
    
    \item In the unsupervised realm, confidential and authenticated \emph{group}
    communication within a single unsupervised cluster is facilitated by
    \emph{intra-unsupervised cluster keying}. In this mode of communication, the
    compromise of a node compromises the security of the whole cluster. Between
    unsupervised clusters, communication is open and unauthenticated.

    \item Between the supervised realm and the unsupervised realm, confidential
    but unauthenticated communication is facilitated by
    \emph{unsupervised-to-supervised cluster keying}, although by default there
    is no trust between the two realms (see Section~\ref{sec:usage}). 
\end{itemize}
% Draft:
%\begin{itemize}
%\item \textbf{Within a supervised cluster}, 
%(1) Within a supervised cluster, our architecture facilitates secure
%communication between any node and the supervisor, and between any pair of nodes
%(one-to-many, or multicast communication is outside the scope of this paper).
%The effect of any node's compromise is isolated, i.e.  if a node $A$ is
%compromised, only sessions that involve $A$ are compromised.
%\item \textbf{Within an unsupervised cluster}, 
%(2) Within an unsupervised cluster, authentication and confidentiality can only
%be achieved on the group level. The compromise of a node compromises the
%security of the whole cluster since all the cluster members share the same
%cluster key. 
%\item \textbf{Between supervised clusters}, 
%(3) Between supervised clusters, secure communication can be established between
%any supervised node or supervisor, and any other supervised node or supervisor. 
%\item %\textbf{Between unsupervised clusters}, 
%(4) Between unsupervised clusters, any communication is open and
%unauthenticated. 
%\item %\textbf{Between supervised and unsupervised clusters},     
%(5) Between supervised and unsupervised clusters, confidential but
%unauthenticated cross-realm communication is facilitated although by default
%there is no trust between the unsupervised and supervised realm
%(Section~\ref{sec:usage}). 
%\end{itemize}
The topic of application-level security like access control is left to a
higher-level specification than that is appropriate for this key management
architecture. 

%To appreciate these objectives... 

%SPKI/SDSI access control list (ACL).
%Bell LaPadula model 


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\section{Key Refreshment}\label{sec:rekey}

The effectiveness of a key is not only bounded by its length but also by the
number of plaintexts it has been used to encrypt, because with enough
ciphertexts an intruder is able to launch cryptanalytic attack and birthday
attack~\cite{abdalla00increasing}. What `enough' means depends on the
cryptanalytic threshold and respectively the birthday threshold, the least of
which is the \emph{encryption threshold}, or the number of plaintexts of some
fixed length that can be safely encrypted. Therefore, as part of any key
management architecture, we need a scheme to `refresh' the deployed keys before
the encryption threshold is reached. Given an initial shared key $K_0$ between
two nodes $A$ and $B$, the encryption and message authentication code (MAC) keys
are derived \emph{serially} at each $i$-th re-key as follows: 
\begin{equation}
K_{enc,i} = MAC_{K_i}(1) \text{\hspace{1cm}and\hspace{1cm}} K_{MAC,i} = MAC_{K_i}(2) 
\label{eqn:rekey}
\end{equation}
where $K_{i+1} = MAC_{K_{i}}(0)$ and $i=0,1,2,\ldots$. A convention in this
paper is that a pair of encryption key and MAC key derived from key $K$ is
written as $K'$ and $K''$. 

%It is important to note that although the protocol descriptions in this paper
%always use the same key for both encryption and MAC, it should be understood
%that the keys are actually different in the sense of Equation~\ref{eqn:rekey}.

% re-key trigger mechanism
In a supervised cluster, re-keying is message-count driven, i.e. when the
encrypted message count approaches the encryption threshold (e.g.  $2^{2k/3}$
for CBC mode, where $k$ is the key length~\cite{abdalla00increasing}), re-keying
is initiated. In a supervised cluster, if the shared key is between a node and
the superviser, or between a node and another node, re-keying can be initiated
by either end of the secure channel. In an unsupervised cluster, re-keying of
the cluster key can proceed in a similar fashion described by Basagni et
al~\cite{basagni01secure}.

%different encryption threshold for different modes: CBC mode, OCB mode, CTR mode

%Such re-key mechanism however does not assure forward secrecy, as typical with
%any scheme that uses MAC or hash function to derive new keys. 

%why not time driven? because if any node can be dissected live, it doesn't make
%sense 


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\section{Key Usage}\label{sec:usage}

%With the key deployment scheme in place, we discuss key usage in terms of
%cluster-based communication. 

A good key deployment scheme faciliates establishment of secure channels at low
overhead. In ESA1, secure one-to-one (unicast) and one-to-many (multicast)
communications have to be facilitated between and within clusters. However for
this paper, only unicast will be described. Session establishment has two
phases: (1) key setup and (2) route setup. During key setup, the initiator
engages the node it wants to communicate with in a key establishment (keying for
short) protocol, using an underlying, not necessarily secure routing protocol.
Recall that such insecure routing can be described by Dolev and Yao's intruder
model. Leveraging the newly established shared key, route setup involves setting
up the to-and-fro routes between the two parties using an adaptation of
Ariadne~\cite{hu02ariadne}, since Ariadne requires only a shared secret key
between the two communicating parties. Ariadne is an secure (authenticated to be
specific) routing protocol built on top of unoptimized Dynamic Source
Routing~\cite{johnson96dynamic}, but it must be adapted to handle unidirectional
links -- the details is however left to a later paper. Route setup is routine
for every instance of session establishment, so in the ensuing discussion only
key setups would be described. 

\paragraph{Formal Protocol Verification} For the keying protocols
below, verification is carried out using Corin and Etalle's constraint
solving-based protocol verifier CoProVe at \url{wwwes.cs.utwente.nl/24cqet}
\cite{corin02improved}. 
%The most prominent advantage of this tool is that it is fast and easy to use. 
% system scenario -> role -> model-checking
The verifier works by taking as input a specification of the protocol and a
\emph{system scenario} describing the roles involved in the protocol, e.g. the
initiator, the responder or a server of the protocol. Since the verifier works
by model-checking, system scenarios must be finite -- a restriction shared by
every model-checking-based approach. (Other approaches like theorem proving do
not have this drawback but sacrifice termination guarantee.) As such, a protocol
cannot be verified as secure w.r.t. an unbounded number of sessions, but only to
the finite tested scenarios. There is no assurance that an attack would not
actually be found in a larger scenario. Another problem of the model-checking
approach is that the addition of more roles in the scenario may result in state
space explosion. This is because the addition of a role means the addition of a
new `concurrent' process that may interleave its execution with all the rest of
the roles in the scenario. CoProVe is designed to minimize this effect, by
avoiding useless variable instantiations and working in a lazy fashion.
Therefore CoProVe is efficient. In this paper, CoProVe is used to verify these
properties:
\begin{itemize}
    \item Confidentiality: There is no builtin logic for expressing security
    properties, in CoProVe we can however `encode' the desired security property
    in the system scenario, along with the normal roles. For confidentiality,
    this is done by creating a  special `secrecy' role, which attempts to
    \emph{receive} the secret we want to guard.  If there is no corresponding
    role in the specification that sends the secret, but the receiving role
    finishes (i.e.  is able to receive the secret), then we can deduce that it
    can only be the intruder who sent it, and therefore the intruder
    \emph{knows} the secret.

    \item Authentication: To verify authentication, we fix some role, say a
    responder, but we exclude the corresponding initiator.  If the responder is
    able to run to completion, we can regard the protocol as having
    authentication failure, since there exists the possiblity of an intruder
    impersonating the initiator, thereby finishing the protocol with the
    responder. 

    \item Replay resistance: The meaning of replay attack on a role $S$ is the
    possibility of unauthenticated parties to cause $S$ to run, i.e. for $S$ to
    process replayed messages. If $S$ happens to maintain state of every run,
    then it would be maintaining incorrect states. In CoProVe, we verify replay
    resistance of $S$ by checking if two instances of $S$ can complete regardless
    of the other roles.
\end{itemize}

% -- [corin] begin --
%As we already mentioned, verification of the proposed protocols was done 
%with our constraint-based protocol verifier, CoProVe \cite{CE02}. In the 
%tool, protocols are modelled by specifying each role of the protocol 
%separately (e.g. initiator, responder, server). Each role provide a 
%`template' that, later, can be instantiated by a real agent. This would 
%model that an agent is playing some specific role in the network.

%Also, a `system scenario' must be supplied to the tool. This system scenario 
%contains the actual information about the participants that take part of 
%the communication. For instance, we can have a system scenario that 
%consist of only one initiator, one responder and one server. 

%System scenarios must be finite, since the verifier works by 
%model-checking it to find situations that represent actual attacks over 
%the protocol. This restriction is shared by every approach based on 
%model-checking. (Other approaches, e.g. those based on theorem proving, do 
%not have this defficiency, but, on the other hand, sacrifice termination.)
%Because of this, a protocol cannot be regarded as secure w.r.t. an 
%unbounded number of sessions, but only to the finite tested scenarios. It 
%cannot be assured that a larger scenario may actually find an attack.

%Another problem in the model-checking approach is that when roles are 
%added to a scenario, state/space explosion may occur. This is so since 
%addition of a role means addition of a new `concurrent' process that may 
%interleave its execution with all the rest of the roles in the scenario. 
%CoProVe is designed in a way that can minimize this effect; this is 
%achievied, basically, by preventing useless variable instantiations and 
%working in a lazy fashion. Therefore, the tool performs verification efficiently.

%Checking for Secrecy and Authentication

%Since we have no logic for expressing the security properties, we need to 
%somehow `encode' the desired security property in the system scenario, 
%along with the normal roles. For secrecy, this is easy: we can create a 
%special `secrecy' role, which only tries to \emph{receive} the secret we want to check. 
%Since there is no corresponding role that sends the secret, if the 
%receiving role finishes (i.e., the secret is sent to it) then we can 
%deduce that the intruder sent it, and therefore the intruder \emph{knows} 
%the secret.

%Authentication can be verified in the following way: in a scenario, we fix 
%some role, say, a responder, but we exclude the corresponding initiator. 
%Then, we start verification, and check if the responder role can finish 
%its execution. If so, then we can regard the protocol as having an 
%authentication failure, since the intruder must had impersonated the 
%initiator succesfully in order to make the responder to finish.

%Verifying the Eyes protocols

%We verified each protocol of the previous sections. For each one, we fixed 
%up scenarios that checked the proposed security objectives. The protocols 
%passed succesfully the tests, which can assure us some level of trust. (Of 
%course, as we already mentioned, larger scenarios may find new attacks).

%The protocol specifications, along with the tested scenarios, can be found 
%on the CoProVe online demo (reachable at http://wwwes.cs.utwente.nl/24cqet/).

% -- [corin] end --

%, i.e. we have the following types of communication:
%\begin{enumerate}
%    \item Intra-cluster communication
%    \begin{enumerate}
%        \item Within supervised cluster
%        \item Within unsupervised cluster
%    \end{enumerate}
%    
%    \item Inter-cluster communication
%    \begin{enumerate}
%        \item Between supervised clusters
%        \item Between supervised and unsupervised clusters
%        \item Between unsupervised clusters
%    \end{enumerate}
%\end{enumerate}

\subsection{Intra-Supervised Cluster Keying} 
We start our verification with the keying protocol that is used within a
supervised cluster.  Suppose in a cluster supervised by $S$, a node $A$ (which
shares key $K_A$ with $S$) wants to initiate a session with $B$ (which shares
key $K_B$ with $S$). The keying protocol for this scenario could be adapted from
the node-to-node key agreement protocol of SPINS~\cite{perrig01spins}: 
\footnotesize
\begin{alignat}{2}
1.\;& A \rightarrow B &:\;& N_A, A 
\notag\\
2.\;& B \rightarrow S &:\;& N_A, N_B, A, B, MAC_{K''_B}(N_A|N_B|A|B) 
\notag\\        
3.\;& S \rightarrow A &:\;& E_{K'_A}(K_{AB}), MAC_{K''_A}(N_A|B|E_{K'_A}(K_{AB})) 
\notag\\        
4.\;& S \rightarrow B &:\;& E_{K'_B}(K_{AB}), MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB})) 
\notag\\
5.\;& A \rightarrow B &:\;& \text{Ack}, MAC_{K''_{AB}}(\text{Ack})
\label{eqn:spins}
\end{alignat}
\normalsize
where the first four messages are from SPINS, and the fifth message is added to
prevent authentication failure. This protocol is verified (1) secure in the
confidentiality of $K_{AB}$, (2) secure in the mutual authentication between $A$
and $B$, and (3) secure against replay attacks on $S$. The drawback of this
protocol is that while there is no attack, it is far too easy for an intruder to
generate bogus requests (at step 1) and hence bogus protocol instances, that
would cause $B$ to wait at step 5 for the protocol instances to finish.
% Note: DoS attack cannot be used as a reason
%If the implementation is such that after the 4th round $B$ will drop all further
%requests including genuine requests from $A$, until $I$ acknowledges or the
%bogus session times out, a denial-of-service (DoS) attack has occured. Think
%another way, let's say the request is indeed from $A$ and at the 5th round while
%$B$ is waiting for $A$'s acknowledgement, $B$ does not block further requests,
%then any intruder who sends/replays the message $N_A, A$ would be able to cause
%the session to be re-keyed, possibly without $A$'s knowledge. This is in
%fact also a DoS attack and in conclusion the protocol from SPINS cannot be used.
%
% Note: Timeout is always there
%Adding a 5th message so that $A$ authenticates itself to $B$ does not help
%because the timeout would still be there.
%
% Note: B would at least have to send one message anyway
%From another angle, the energy $B$ spends on forwarding this bogus requests to
%$S$ is also wasted. <-- this cannot be helped, in any secure protocol, 
%
% -- Protocol: --
% Version 1 (Vulnerable to replay attack on B): 
% Note: $A$ cannot give $K_{AB}$ to $B$ directly, because $B$ cannot
% authenticate $A$. 
%\begin{align*}
%A \rightarrow S &: N_A, B, MAC_{K_A''}(N_A|B) 
%\\
%S \rightarrow A &: N_S, E_{K'_A}(K_{AB}), 
%MAC_{K''_A}(N_A|B|N_S|E_{K'_A}(K_{AB}|N_S)) 
%\\
%S \rightarrow B &: N_S, A, E_{K'_B}(K_{AB}), MAC_{K''_B}(N_S|A|E_{K'_B}(K_{AB})) 
%\\
%A \rightarrow B &: E_{K'_{AB}}(N_{A2}), MAC_{K''_{AB}}(N_S|E_{K'_{AB}}(N_{A2}))
%\\
%B \rightarrow A &: E_{K'_{AB}}(N_{A2}+1) 
%\end{align*}
%
% Version 2:
Our design principle is such that $A$ is made to do more work compared with $B$
in order to finish the protocol.  
\footnotesize
\begin{alignat}{2}
% don't start by sending to B otherwise will end up having the same problem as
% SPINS
% S is able to auth A, so don't need to MAC A
1.\;& A \rightarrow S   &:\;& N_A, B, MAC_{K''_A}(N_A|B) 
\notag\\
% always MAC B as well because B is not an info related to A 
2.\;& S \rightarrow A   &:\;& E_{K'_A}(E_{K'_B}(N_S)|K_{AB}),
MAC_{K''_A}(N_A|B|E_{K'_A}(N_S)|K_{AB}) 
\notag\\
% if A is forged, then S would know, leave out B per convention
% cannot use N_{A2} which causes auth failure of A to B
% timeliness completely depends on N_S
3.\;& A \rightarrow B   &:\;& A, E_{K'_B}(N_S)
\notag\\
% remember to use N_S in the MAC here; B is sent here to make explicit A's
% request is to B
4.\;& B \rightarrow S   &:\;& B, N_B, A, MAC_{K''_B}(N_S|B|N_B|A)
\notag\\
% MAC A because "A" is not part of B
5.\;& S \rightarrow B   &:\;& E_{K'_B}(K_{AB}),
MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB})) 
\notag\\
% N_{A2} is not used here same as explained before 
6.\;& B \rightarrow A   &:\;& \text{Ack}, MAC_{K''_{AB}}(\text{Ack})
\label{eqn:intra}
\end{alignat}
\normalsize
Now it takes three messages for $A$ to get $B$ to respond, and $S$ is able tell
$B$ whether $A$'s request is genuine at step 5. The drawback is that $B$ has to
send one more message in total than Protocol~\eqref{eqn:spins}, and $S$ has to
maintain state, i.e. $N_S$, for some time. The fact that it takes more messages
in total for Protocol~\eqref{eqn:intra} cannot be helped by our requirement that
$A$ authenticates itself with $S$ first. Special attention is given to the MAC
at step 6 because MAC'ed acknowledgements are susceptible replays depending on
the mode used. We assume if CCM (CTR + CBC-MAC)~\cite{jonsson02security} is
used, we should be able to minimize this risk. This also applies to other
instances of MAC'ed acknowledgement in the other protocols in the rest of this
paper. This protocol is verified (1) secure in the confidentiality of $K_{AB}$,
(2) secure in the mutual authentication between $A$ and $B$, and (3) secure
against replay attacks on $S$. 

% [corin]
%One way of solving this problem is by introducing a fifth message where $A$ can
%prove she is really her:
%\begin{align*}
%A \rightarrow B &: E_{K_{AB}}(N_A)
%\end{align*}
%In this message $A$ is proving her identity only to $B$. Similarly, a sixth
%message to $S$ could be added.
%The following replay attack can be mounted against $S$:
%\begin{align*}
%1. \  A \rightarrow B &: N_A, A 
%\\        
%2. \  B \rightarrow S &: N_A, N_B, A, B, MAC_{K''_B}(N_A|N_B|A|B) 
%\\        
%3. \  S \rightarrow A &: E_{K'_A}(K_{AB}), MAC_{K''_A}(N_A|B|E_{K'_A}(K_{AB})) 
%\\             
%4. \  S \rightarrow B &: E_{K'_B}(K_{AB}), MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB})) 
%\\
%2'.\  I_B \rightarrow S &: N_A, N_B, A, B, MAC_{K''_B}(N_A|N_B|A|B) 
%\\        
%3'. \ S \rightarrow I_A &: E_{K'_A}(K_{AB'}), MAC_{K''_A}(N_A|B|E_{K'_A}(K_{AB})) 
%\\             
%4'. \  S \rightarrow I_B &: E_{K'_B}(K_{AB'}), MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB})) 
%\end{align*}
%After a normal execution of the protocol, an intruder can replay message 2 and
%start a new session impersonating $B$. Since the server $S$ does not save old
%nonces, it will continue the execution of the protocol.
%
%This attack can be avoided by modifying message 3 and 4, adding a nonce $N_S$. Then, 
%adding a fifth where $B$ prove he is really executing the protocol with $S$:
%\begin{align*}
%A \rightarrow B &: N_A, A 
%\\        
%B \rightarrow S &: N_A, N_B, A, B, MAC_{K''_B}(N_A|N_B|A|B) 
%\\        
%S \rightarrow A &: E_{K'_A}(K_{AB}|N_S), MAC_{K''_A}(N_A|B|E_{K'_A}(K_{AB})) 
%\\             
%S \rightarrow B &: E_{K'_B}(K_{AB}|N_S), MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB})) 
%\\
%B \rightarrow S &: E_{K_{AB}}(N_A|N_S)        
%\end{align*}

\subsection{Inter-Supervised Cluster Keying}
After solving the problem of keying two nodes in the same cluster, let us
consider keying two nodes from two different clusters in the supervised realm.
The following protocol is proposed:
% Version 1 (Susceptible to replay attacks):
%\begin{alignat*}{2}
%& A \rightarrow B     &:\;& N_A, A 
%\\
% please don't delete A
%& A \rightarrow S_A   &:\;& N_A, A, B, MAC_{K'_A}(N_A|A|B)
%\\
% please don't delete B
%& B \rightarrow S_B   &:\;& N_A, N_B, A, B, MAC_{K'_B}(N_A|N_B|A|B)
%\\
% what's the use of telling S_A about N_B?
% how hard is it to get hold of A? in fact, not hard, because an intruder
% might be get hold of N_A sent in cleartext
%& S_B \rightarrow S_A &:\;& E_{K'_{SS}}(K_1), MAC_{K''_{SS}}(N_A|A|B|E_{K'_{SS}}(K_1))
%\\    
% encrypting K_2 with K_1 is not necessary
%& S_A \rightarrow S_B &:\;& E_{K'_{SS}}(K_2), MAC_{K''_{SS}}(N_A|A|B|E_{K'_{SS}}(K_2))    
%\\
%& S_A \rightarrow A   &:\;& E_{K'_A}(K_{AB}), MAC_{K''_A}(N_A|B|E_{K'_A}(K_{AB}))
%\\
%& S_B \rightarrow B   &:\;& E_{K'_B}(K_{AB}), MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB}))    
%\end{alignat*}
%where $K_{AB} = K_1 \bigoplus K_2$.
%
%Again, secrecy of $K_{AB}$ is not violated in any of the scenarios tested in
%the verifier. 
%
%But a different vulnerability was exposed by the tool:
%\begin{alignat*}{2}
%& A \rightarrow B     &:\;& N_A, A 
%\\
%& A \rightarrow S_A   &:\;& N_A, A, B, MAC_{K'_A}(N_A|A|B)
%\\
%& B \rightarrow S_B   &:\;& N_A, N_B, A, B, MAC_{K'_B}(N_A|N_B|A|B)
%\\
%& S_B \rightarrow S_A &:\;& E_{K'_{SS}}(K_1), MAC_{K''_{SS}}(N_A|A|B|E_{K'_{SS}}(K_1))
%\\    
%& I_{S_A} \rightarrow S_B &:\;& E_{K'_{SS}}(K_1), MAC_{K''_{SS}}(N_A|A|B|E_{K'_{SS}}(K_1))    
%\\
%& S_A \rightarrow A   &:\;& E_{K'_A}(K_{AB}'), MAC_{K''_A}(N_A|B|E_{K'_A}(K_{AB}'))
%\\
%& S_B \rightarrow B   &:\;& E_{K'_B}(K_{AB}), MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB}))    
%\end{alignat*}
% 
%Here, $K_{AB}=K_1 \bigoplus K_2$, but $K_{AB}=K_1 \bigoplus K_1=0$!. The
%intruder replay message 4 as message 5, intercepting the real sending of $K_2$
%and placing instead the sending of $K_1$ back to $S_A$.
%
%A possible solution to this lies in modifying message 5:
%\begin{alignat*}{2}
%& S_A \rightarrow S_B &:\;& E_{K'_{SS}}(K_1), MAC_{K''_{SS}}(N_A|E_{K'_{SS}}(K_1))    
%\end{alignat*}
%
% Version 3:
\footnotesize
\begin{alignat*}{2}
1.\;& A \rightarrow S_A   &:\;& N_A, B, MAC_{K''_A}(N_A|B) 
\\
2.\;& S_A \rightarrow A   &:\;& E_{K'_{SS}}(N_{S_A}), MAC_{K''_A}(N_A|B|E_{K'_{SS}}(N_{S_A}))
\\
% took out N_{A2}, but not verified yet
3.\;& A \rightarrow B     &:\;& A, B, E_{K'_{SS}}(N_{S_A})
\\
4.\;& B \rightarrow S_B   &:\;& B, N_B, A, E_{K'_{SS}}(N_{S_A}),
MAC_{K''_B}(B|N_B|A|E_{K'_{SS}}(N_{S_A}))
\\
5.\;& S_B \rightarrow S_A &:\;& N_{S_B}, A, B, E_{K'_{SS}}(K_{AB2}),
MAC_{K''_{SS}}(N_{S_A}|N_{S_B}|A|B|E_{K'_{SS}}(K_{AB2}))
\\
6.\;& S_A \rightarrow S_B &:\;& E_{K'_{SS}}(K_{AB1}), MAC_{K''_{SS}}(N_{S_B}|A|B|E_{K''{SS}}(K_{AB1}))
\\
7.\;& S_A \rightarrow A   &:\;& E_{K'_A}(K_{AB}), MAC_{K''_A}(N_A|B|E_{K'_A}(K_{AB})) 
\\
8.\;& S_B \rightarrow B   &:\;& E_{K'_B}(K_{AB}), MAC_{K''_B}(N_B|A|E_{K'_B}(K_{AB}))
\\
% took out N_{A_2}, but not verified yet 
9.\;& B   \rightarrow A   &:\;& \text{Ack}, MAC_{K_{AB}}(\text{Ack})
\end{alignat*}
\normalsize
where $K_{AB} = K_{AB1}|K_{AB2}$. Note that $A$ does not need to know who
$B$'s supervisor is -- that is $S_A$'s job. 

% todo: comment on the key length

\subsection{Key Migration}
% Version 1 (Induceable migration attack):
%\begin{alignat*}{2}
%& A \rightarrow S_B   &:\;& N_A, A 
%\\        
%& S_B \rightarrow S_A &:\;& N_A, N_{S_B}, A, S_B, MAC_{K''_{SS}}(N_A|N_{S_B}|A|S_B) 
%\\        
%& S_A \rightarrow S_B &:\;& E_{K'_{SS}}(K_A), MAC_{K''_{SS}}(N_{S_B}|A|E_{K'_{SS}}(K_A)) 
%\\        
%& S_A \rightarrow A   &:\;& \text{Success}, MAC_{K''_A}(N_A|S_B|\text{Success}) 
%\end{alignat*}
%where $K_A$ is the refreshed key between $A$ and $S_A$ as a result of the
%protocol, i.e. if $K$ is the shared key between $A$ and $S_A$ before the
%protocol begins, then $K_A = H(K)$.
%
%Again, secrecy of $K_A$ is not violated. The verifier found a vulnerability,
%though, where the intruder can impersonate $A$ a perform a node migration, even
%if $A$ never asked this:
%\begin{alignat*}{2}
%& I_A \rightarrow S_B   &:\;& N_A, A 
%\\        
%& S_B \rightarrow S_A &:\;& N_A, N_{S_B}, A, S_B, MAC_{K''_{SS}}(N_A|N_{S_B}|A|S_B) 
%\\        
%& S_A \rightarrow S_B &:\;& E_{K'_{SS}}(K_A), MAC_{K''_{SS}}(N_{S_B}|A|E_{K'_{SS}}(K_A)) 
%\\        
%& S_A \rightarrow A   &:\;& \text{Success}, MAC_{K''_A}(N_A|S_B|\text{Success}) 
%\end{alignat*}
%
%A possible patch for this failure is as follows:
%\begin{alignat*}{2}
%& A \rightarrow S_B   &:\;& N_A, A 
%\\        
%& S_B \rightarrow S_A &:\;& N_A, N_{S_B}, A, S_B, MAC_{K''_{SS}}(N_A|N_{S_B}|A|S_B) 
%\\
%& S_A \rightarrow A   &:\;& N_{S_B}
%\\
%& A \rightarrow S_A   &:\;& E_K(N_{S_B})
%\\        
%& S_A \rightarrow S_B &:\;& E_{K'_{SS}}(K_A), MAC_{K''_{SS}}(N_{S_B}|A|E_{K'_{SS}}(K_A)) 
%\\        
%& S_A \rightarrow A   &:\;& \text{Success}, MAC_{K''_A}(N_A|S_B|\text{Success}) 
%\end{alignat*}
%
%Adding messages 3 and 4, we assure that $A$ is online, and that she is really
%$A$, since otherwise she could never have created message 4 (since $K$ only
%belongs to her).
%
% Version 2 (Vulnerable to replay attack):
%My problem with the above protocol and my original protocol is that $S_A$ is not
%sure whether $A$ really asked for the key to be migrated. And the flying back
%and forth of $N_{S_B}$ and $E_K(N_{S_B})$ is a magnet for replay and cryptanalytic
%attacks. My humble idea:
%\begin{alignat*}{2}
%& A \rightarrow S_B   &:\;& I, E_{K'_A}(N_A)
%\\
%& A \rightarrow S_A   &:\;& E_{K'_A}(N_A|S_B), MAC_{K''_A}(E_{K'_A}(N_A|S_B))
%\\        
%& S_B \rightarrow S_A &:\;& N_{S_B}, A, MAC_{K''_{SS}}(E_{K'_A}(N_A)|N_{S_B}|A) 
%\\
%& S_A \rightarrow S_B &:\;& E_{K'_{SS}}(K_{A2}|H(N_A)),
%MAC_{K''_{SS}}(N_{S_B}|E_{K'_{SS}}(K_{A2}|H(N_A)))
%\\
%& S_B \rightarrow A   &:\;& I, MAC_{K''_{A2}}(H(N_A)|I)
%\end{alignat*}
%
%Where $K_{A2} = MAC_{K_A}(0)$, $I$ is a migration session identifer; and the use
%of $H(N_A)$ instead of $N_A$ is to thwart cryptanalytic attacks on
%$E_{K'_A}(N_A)$. The drawback now is that $A$ has to do more encryption and send
%more bytes. Perhaps you can verify this protocol and would find it interesting
%to optimize the resource requirement.
%
% Version 3:
Intra-supervised cluster keying and inter-supervised cluster keying work most
efficiently if $A$ is in its home cluster. While in a foreign cluster, $A$ may
`employ' the supervisor of the foreign cluster to be its temporary supervisor,
by migrating its key from the home cluster to the foreign cluster.  Suppose $A$
migrates from the cluster supervised by $S_A$ to the cluster supervised by
$S_B$, the security objective of this protocol is to prevent unauthorized
migrations, i.e. if $A$ did not authorize the migration, the migration should
not occur. The following is the proposed protocol: 
\footnotesize
\begin{alignat}{2}
% A doesn't need to be MAC'ed -- redundant
1.\;& A \rightarrow S_A   &:\;& N_A, S_B, MAC_{K''_A}(N_A|S_B) 
\notag\\
2.\;& S_A \rightarrow A   &:\;& E_{K'_A}(E_{K'_{SS}}(N_{S_A})), MAC_{K''_A}(N_A|S_B|E_{K'_{SS}}(N_{S_A})) 
\notag\\
% took out N_{A2}
3.\;& A \rightarrow S_B   &:\;& A, S_A, E_{K'_{SS}}(N_{S_A})
\notag\\
4.\;& S_B \rightarrow S_A &:\;& S_B, N_{S_B}, A, MAC_{K''_{SS}}(N_{S_A}|S_B|N_{S_B}|A)
\notag\\        
5.\;& S_A \rightarrow S_B &:\;& E_{K''_{SS}}(K_{A2}),
MAC_{K''_{SS}}(N_{S_B}|A|E_{K''_{SS}}(K_{A2})) 
\notag\\
% took out N_{A2} and S_A
6.\;& S_B \rightarrow A   &:\;& \text{Sucess}, MAC_{K''_{A2}}(\text{Sucess})
\label{eqn:migration}
\end{alignat}
\normalsize
where $K_{A2} = MAC_{K_{A}}(0)$. This protocol is verified (1) secure in the
confidentiality of $K_{A2}$, (2) secure in the authentication of $A$ to $S_A$
and $S_B$, of $S_A$ to $A$ and $S_B$, of $S_B$ to $A$ and $S_B$, and (3) secure
against replay attacks on $S_A$.  

\subsection{Intra-Unsupervised Cluster Keying} 
When two nodes in an unsupervised cluster want to communicate with each other,
the only key they can use is the cluster key. To state the obvious, the cluster
is never used directly, instead, for each session a new pair of encryption and
MAC keys are derived from the cluster key using the mechanism of
Section~\ref{sec:rekey}. 

% Wrong, re-key is message count-driven: Throughout each
%session, the pair of keys are continuously and periodically refreshed, to
%prevent birthday attacks.  

\subsection{Unsupervised-to-Supervised Node Keying} 



%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\section{Related Work}\label{sec:related}

% No space to mention this:
%The amended needham schroeder protocol involves 7 messages, in which the server
%is only required to send one message (this is understandable from the denial of
%service attack prevention point of view). $A$ sends 4 messages whereas $B$ sends
%2 messages.

% compare with proposals in key management architecture
Slijepcevic et al's proposal~\cite{slijepcevic02communication} of using a list
of master keys and a pseudorandom generator to select the active key at
runtime does not apply to us, because our assumption is that sensor nodes are
not tamper-resistant. The set of master keys, the corresponding pseudorandom
number generator and the see are easily exposed. In short, having more keys
are not necessarily more secure. The same proposal also suggests deploying keys
according to the location, with the obvious requirement of nodes being able to
discover out their own coordinates. 

Luo et al \cite{luo02selfsecuring}, various multicast scheme

Yi et al \cite{yi01securityaware}

Zhou et al~\cite{zhou99securing} propose using  


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\section{Conclusion and Future Work}\label{sec:conclusion}

% 1. what we don't do
% 2. what we do
% 3. how we do it
% 4. how we think we did it

If the architecture described in this paper is perceived to be simple, then it
has achieved its purpose. Attacks on the WSNs are only bounded by imagination.
What we intend to achieve in this paper is, on the basis of the absence of more
destructive attacks (e.g. jamming), securing the communication between sensor
nodes. Motivated by the assumption that sensors are not tamper-resistant, we
have devised an architecture in which two security realms namely the supervised
realm and the unsupervised realm provide two levels of security.  Communication
in the supervised realm entails various protocols to facilitate intra- and
inter- supervised cluster keying, which we have verified with our tool CoProVe.
In the unsupervsied realm, security suffers from the fact that a cluster key is
shared by all members of the same cluster. The trade-off provides WSN
implementors with an option to partition their system according to the actual
security requirements. The protocols we have proposed are meant to be correct
first rather than to be optimal. For future work, we plan to measure and
optimize the overall energy consumption of the protocols. We are also 
motivated to extend our architecture to support directed
diffusion (which implies multicast
communication)~\cite{intanagonwiwat00directed}. As of now, our assumption is
that a node knows exactly the name of the other node it wants to communicate
with, which is not the case in directed diffusion.


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\setcounter{section}{0}
\renewcommand{\thesection}{Appendix \Alph{section}}
\section{The Bidirectionality Assumption}\label{sec:bidirectionality}
\renewcommand{\thesection}{\Alph{section}}

Bidirectionality offers a lot of advantage, e.g. routing and clustering would be
easier, but links become unidirectional due to differing propagation patterns,
or sources of interference anyway. In the following, we argue that
bi-directional is not a necessary (and possibly desirable) assumption:

\begin{figure}[ht]
    \centering
    \scalebox{0.75}{\includegraphics{bidirectional-woes.eps}}
    \caption{\label{fig:bidirectional-woes}(a) Range expansion chain reaction.
    Radio range expansion chain reaction. (b) Expansion of ellipsoidal range.
    (Continuous circles represent original ranges, dashed circles represent
    expanded ranges.)}
\end{figure}

\begin{enumerate}
    \item Although the nodes are generally able to modify their radio range by
    increasing/decreasing their transmission power, doing so would set up a
    chain reaction that might not be necessary for the normal functioning of the
    network. In Figure~\ref{fig:bidirectional-woes}(a), let us say $C
    \rightsquigarrow B$, but $B \not\rightsquigarrow C$, so $B$ enlarges its
    radio range, which enables $B$ to contact $C$ and inadvertently $A$, but $A$
    originally cannot contact $B$ nor $C$, so $A$ enlarges its radio range and
    by doing so enables $A$ to contact $B$ and inadvertantly $C$, and $C$ has to
    enlarge its radio range to be able to contact $A$. The chain reaction would
    potentially produce a ripple throughout the network.

    \item On the data link level (MAC), in the TDMA-based EMACs protocol (not
    yet published) for example, neighbouring nodes have to share a fixed number
    of slots per frame. What if expanding the radio range would increase the
    number of neighbours of a node to such a degree that the number of available
    slots is exhausted?
    
    \item One more thing is that if the radio range is very ellipsoidal instead
    of near-spherical, getting bidirectionality requires much more transmission
    power in the scenario of Figure~\ref{fig:bidirectional-woes}(b), where $A$
    lies along the shorter radius of $B$.
\end{enumerate}


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

\bibliographystyle{plain}
\bibliography{references}

% todo: use this for the final draft%
\footnotesize
%\begin{thebibliography}{n}
%\bibitem{}
%\end{thebibliography}
\normalsize


\end{document}
