Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols

Space limitations make it impossible to describe all of the background material. The long-established VDM notation is not described here but can be studied in [18]; there is also an international standard on VDM [14].

A convenient publication outlining the rely-guarantee ideas is [12]; early papers on rely/guarantee ideas include [15, 16, 17]; an algebraic presentation and more recent references are covered in [13]. R-G was conceived as a way of decomposing a specified component into sub-components that executed concurrently. It was subsequently observed (e.g. [20]) that rely conditions could be used to describe assumptions about external components that were not being designed: they were part of the problem space. In a further development (e.g. [8]) it was shown how layered R-G conditions could be used to describe fault-tolerant systems: optimistic rely conditions are linked to optimal behaviour but useful behaviour can still be achieved under weaker assumptions.

Most protocol discussions start by listing the (expected) interactions; for example the public key version of Needham-Schroeder (N-S) is normally presented as [24]:

$\mathit{}(a1)A:enc([A,NA],pkeym(B))\newline (b1)B:enc([NA,NB],pkeym(A))\newline (a2)A:enc([NB],pkeym(B))$

A train of thought about this exchange might be that only $\mathit{}B$ can decrypt $\mathit{}a1$ and therefore $\mathit{}A$ has evidence¹¹1We avoid terms such as “$\mathit{}A$ believes …” because such protocols are algorithms being followed as defined; one might choose to say that “a designer believes …”. in message $\mathit{}b1$ both that $\mathit{}B$ received $\mathit{}a1$ and that $\mathit{}NB$ was created by $\mathit{}B$; similarly $\mathit{}a2$ provides evidence to $\mathit{}B$ that $\mathit{}A$ received $\mathit{}b1$.

Clearly, encryption provides some level of security against attack but it is important to identify how little can be concluded: for example, $\mathit{}B$ has no evidence from message $\mathit{}a1$ as to who actually sent it or the uniqueness of $\mathit{}NA$; whilst $\mathit{}A$ has evidence from receipt of $\mathit{}b1$ that $\mathit{}B$ (or someone with $\mathit{}B$’s secret key) must have decrypted message $\mathit{}a1$, this does not establish that no one else now has $\mathit{}NA$. Apart from the lack of specification/assumptions, it is not made explicit under what circumstances the protocol should abort.

The objective of the current paper is to make the specifications of such protocols precise — in particular, recording assumptions that are required in order to verify that the protocols satisfy their specifications.

A significant and recurrent problem is the lack of precise specifications for protocols in the literature. In both the original paper by Needham and Schroeder and Lowe’s version [22], the overall goal of the protocol is never actually stated, thus making it difficult to employ formal verification.

At first it might appear that the aim is to allow two participants to share secrets that are invisible to all other users. However, this cannot be the case, as there is no way to ensure the secrecy of the messages unless both participants are guaranteed to conform to the protocol. In the presence of dishonest users, a user who legitimately receives a message can forward it to anyone else.²²2This seems to contrast with Lowe’s claim that the shared message nonces can be used for authentication purposes for further transactions; perhaps Lowe’s intent was that the shared nonces be used in conjunction with the confirmed identities of the participants. This could be stated as:

As an alternative, it might be assumed that the aim of the N-S protocol is instead to provide some form of authentication, i.e. allowing each participant to confirm the identity of the other participant with whom they are communicating. This would appear to be the view of [7, §4.3.3] and could be stated as:

As will be seen in the following sections, these conjectures only hold under strong assumptions. In the case of Conjecture 1, the required assumptions are unrealistic and this property therefore does not hold in practice for the un-modified N-S protocol (nor, in fact, the Lowe correction).

Any abstraction leaves out certain aspects (e.g. hiding “side-channel” attacks), while exposing other aspects. The question is whether a given model exposes the required aspects. The current authors wonder whether using process algebra channels can inadvertently hide assumptions. The temptation to base specification and verification on process algebra (CSP is used by Lowe in [23]) might be dangerous because hiding information on channels is precisely the problem that has to be solved.

The goal of the rely/guarantee approach is precisely to identify and record assumptions. In our model, all messages are visible to every user,³³3This makes it easy to model “man in the middle” attacks; see, for example, the discussion in the next section. but, if properly encrypted, only the intended recipient can decrypt a message. This follows the principles of the Dolev-Yao intruder model [10], often used in security protocol verification.

Messages are modelled as a record containing the $\mathit{}Uid$ of the intended recipient, the sender’s $\mathit{}Uid$ and the content of the message.

$\mathit{}Msg$ ::  $\mathit{}rec$ : $\mathit{}Uid$ $\mathit{}sender$ : $\mathit{}Uid$ $\mathit{}content$ : $\mathit{}Item^{*}$

All users can access all $\mathit{}Msg$s, so they are all in the $\mathit{}history$ component of the state ($\mathit{}\mathchar 6\relax$); the $\mathit{}rec$ field governs who can access the $\mathit{}content$. The $\mathit{}sender$ field is a “ghost variable” that is used in correctness arguments; it is not to be confused with data included in the $\mathit{}content$ field that can be a $\mathit{}Uid$ (but might be fraudulently set).

$\mathit{}Item=Nonce|Uid$

Considering only one protocol exchange can be confusing since it is possible for any user process to be involved in multiple overlapping “sessions”. One example is where a “man in the middle” uses an innocent receiver to generate nonces that are replayed to an initiating user of another session. For this reason, the models below separate information by session identifiers and record the origin of nonces.

Information about $\mathit{}User$s is stored in:⁵⁵5The secret key fields ($\mathit{}skey:SKey$) and public keys ($\mathit{}PKey$) are discussed in Section 5.

$\mathit{}User$ ::  $\mathit{}intPartner$ : $\mathit{}Sid\buildrel m\over{\longrightarrow}Uid$ $\mathit{}knows$ : $\mathit{}Sid\buildrel m\over{\longrightarrow}Nonce-\hbox{\bf set\/}$ $\mathit{}skey$ : $\mathit{}SKey$ $\mathit{}conforms$ : $\mathit{}\Bool$ $\mathit{}complete$ : $\mathit{}Sid\buildrel m\over{\longrightarrow}\Bool$

Assumptions about the behaviour of other users could be recorded as rely conditions but it is more convenient to make them invariants. Note that –as in [19]– preservation of the invariant by any context becomes an extra assumption as though it were part of every rely condition and an extra obligation as though it were conjoined to every guarantee condition.

The notion of $\mathit{}Action$ includes both messages and invention of nonces:

$\mathit{}Action=Msg|Invent$

$\mathit{}Invent$ ::  $\mathit{}user$ : $\mathit{}Uid\hskip 100.00015pt$ $\mathit{}what$ : $\mathit{}Nonce$

The following function yields the history restricted to a single user’s activities.

$\mathit{}\hbox{$\mathit{}uHist$}(as,user)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \vtop{\hbox to0.0pt{\hbox{\bf if \/}\vtop{\noindent$\mathit{}as=[\,]$}\hss}\hbox to0.0pt{\hbox{\bf then \/}\vtop{\noindent$\mathit{}[\,]$}\hss}\hbox to0.0pt{\hbox{\bf else \/}\vtop{\noindent$\mathit{}{\vtop{\hbox to0.0pt{\hbox{\bf if \/}\vtop{\noindent$\mathit{}\hbox{\bf hd\kern 1.66672pt\/}\nobreak{as}\in Msg\land((\hbox{\bf hd\kern 1.66672pt\/}\nobreak{as}).rec=user\mathchar 12895\relax(\hbox{\bf hd\kern 1.66672pt\/}\nobreak{as}).sender=user)$}\hss}\hbox to0.0pt{\hbox{\bf then \/}\vtop{\noindent$\mathit{}[\hbox{\bf hd\kern 1.66672pt\/}\nobreak{as}]\mathbin{\hbox{\raise 4.30554pt\hbox{$\mathit{}\@sc@nc$}}}uHist(\hbox{\bf tl\kern 1.66672pt\/}\nobreak{as},user)$}\hss}\hbox to0.0pt{\hbox{\bf else \/}\vtop{\noindent$\mathit{}{\vtop{\hbox to0.0pt{\hbox{\bf if \/}\vtop{\noindent$\mathit{}\hbox{\bf hd\kern 1.66672pt\/}\nobreak{as}\in Invent\land(\hbox{\bf hd\kern 1.66672pt\/}\nobreak{as}).user=user$}\hss}\hbox to0.0pt{\hbox{\bf then \/}\vtop{\noindent$\mathit{}[\hbox{\bf hd\kern 1.66672pt\/}\nobreak{as}]\mathbin{\hbox{\raise 4.30554pt\hbox{$\mathit{}\@sc@nc$}}}uHist(\hbox{\bf tl\kern 1.66672pt\/}\nobreak{as},user)$}\hss}\hbox to0.0pt{\hbox{\bf else \/}\vtop{\noindent$\mathit{}uHist(\hbox{\bf tl\kern 1.66672pt\/}\nobreak{as},user)$}\hss}}}$}\hss}}}$}\hss}}$  

To record the overall intent of the protocol, the most abstract specification is based on a state:

$\mathit{}\mathchar 6\relax$ ::  $\mathit{}users$ : $\mathit{}Uid\buildrel m\over{\longrightarrow}User$ $\mathit{}history$ : $\mathit{}Action^{*}$ $\mathit{}pkeys$ : $\mathit{}Uid\buildrel m\over{\longrightarrow}PKey$

where

$\mathit{}\hbox{$\mathit{}inv-\mathchar 6\relax$}(\sigma)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline unique-nonces(\sigma.history)\land no-read-others(\sigma)\land\newline \Forall u\in\hbox{\bf dom\kern 1.66672pt\/}\nobreak{\sigma.users}\suchthat\hfil\break\hbox to409.75496pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\sigma.users(u).conforms\penalty-35\mskip 6.0mu plus 2.0mu minus 1.0mu\Rightarrow\mskip 6.0mu plus 2.0mu minus 1.0mu\newline no-leaks(uHist(\sigma.history,u))\land no-forge(uHist(\sigma.history,u))$}\hss}$  

The predicates used in $\mathit{}inv-\mathchar 6\relax$ are now defined. $\mathit{}Nonce$s are assumed to be “fresh”:⁶⁶6This assumption is not treated formally below but actually depends on the low probability of a clash in a sufficiently large space.

$\mathit{}\hbox{$\mathit{}unique-nonces$}(as)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \Forall i,j\in\hbox{\bf inds\kern 1.66672pt\/}\nobreak{as}\suchthat\hfil\break\hbox to409.75496pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\{as(i),as(j)\}\subseteq Invent\land as(i).what=as(j).what\penalty-35\mskip 6.0mu plus 2.0mu minus 1.0mu\Rightarrow\mskip 6.0mu plus 2.0mu minus 1.0mui=j$}\hss}$  

The predicate $\mathit{}no-read-others$ records the assumption that no user can read the contents of a message other than the intended recipient (given by the $\mathit{}rec$ field of the message). This is an abstract version of the idea of encryption, which is explored in Section 5.

$\mathit{}\hbox{$\mathit{}no-read-others$}(\sigma)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \Forall u\in\hbox{\bf dom\kern 1.66672pt\/}\nobreak\sigma.users\suchthat\hfil\break\hbox to409.75496pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\Forall n\in\sigma.users(u).knows\suchthat\hfil\break\hbox to399.75494pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\Exists m\in\hbox{\bf rng\kern 1.66672pt\/}\nobreak\sigma.history\suchthat\hfil\break\hbox to389.75493pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}m\in Invent\,\land\,m.user=u\,\land\,m.what=n\mathchar 12895\relax\newline m\in Msg\,\land\,m.rec=u\,\land\,n\in\hbox{\bf elems\kern 1.66672pt\/}\nobreak{m.content}$}\hss}$}\hss}$}\hss}$  

A predicate that limits sending of non-locally generated nonces must, however, allow their return to the believed originator. There are two ways of tackling this: the simpler employs the ghost variable field $\mathit{}sender$, which has to be a ghost variable since no user process can actually determine which user sent a $\mathit{}Msg$.

$\mathit{}\hbox{$\mathit{}no-leaks$}(as)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \Forall i,j\in\hbox{\bf inds\kern 1.66672pt\/}\nobreak{as}\suchthat\hfil\break\hbox to409.75496pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}i<j\penalty-35\mskip 6.0mu plus 2.0mu minus 1.0mu\Rightarrow\mskip 6.0mu plus 2.0mu minus 1.0mu\newline \vtop{\hbox to0.0pt{\hbox{\bf let \/}\vtop{\noindent$\mathit{}mk-Msg(\beta,\alpha,vl_{i})=as(i)\hskip 5.0pt\hbox{\bf in\/}$}\hss}}\hfil\break\vtop{\hbox to0.0pt{\hbox{\bf let \/}\vtop{\noindent$\mathit{}mk-Msg(\gamma,\beta,vl_{j})=as(j)\hskip 5.0pt\hbox{\bf in\/}$}\hss}}\hfil\break({\Exists c\in Nonce}\suchthat c\in\hbox{\bf elems\kern 1.66672pt\/}\nobreak{vl_{i}\cap\hbox{\bf elems\kern 1.66672pt\/}\nobreak{vl_{j}}})\penalty-35\mskip 6.0mu plus 2.0mu minus 1.0mu\Rightarrow\mskip 6.0mu plus 2.0mu minus 1.0mu\gamma=\alpha$}\hss}$  

$\mathit{}\hbox{$\mathit{}no-app-leaks$}(as)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \Forall i,j\in\hbox{\bf inds\kern 1.66672pt\/}\nobreak{as}\suchthat\hfil\break\hbox to409.75496pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}i<j\penalty-35\mskip 6.0mu plus 2.0mu minus 1.0mu\Rightarrow\mskip 6.0mu plus 2.0mu minus 1.0mu\newline \vtop{\hbox to0.0pt{\hbox{\bf let \/}\vtop{\noindent$\mathit{}mk-Msg(\beta,,vl_{i})=as(i)\hskip 5.0pt\hbox{\bf in\/}$}\hss}}\hfil\break\vtop{\hbox to0.0pt{\hbox{\bf let \/}\vtop{\noindent$\mathit{}mk-Msg(\gamma,,vl_{j})=as(j)\hskip 5.0pt\hbox{\bf in\/}$}\hss}}\hfil\break\Exists\alpha\in Uid,c\in Nonce\suchthat\hfil\break\hbox to399.75494pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\alpha\in\hbox{\bf elems\kern 1.66672pt\/}\nobreak{vl_{i}}\land c\in\hbox{\bf elems\kern 1.66672pt\/}\nobreak{vl_{i}\cap\hbox{\bf elems\kern 1.66672pt\/}\nobreak{vl_{j}}}\penalty-35\mskip 6.0mu plus 2.0mu minus 1.0mu\Rightarrow\mskip 6.0mu plus 2.0mu minus 1.0mu\gamma=\alpha$}\hss}$}\hss}$  

A predicate for ensuring that users only sign honestly is:

$\mathit{}\hbox{$\mathit{}no-forge$}(as)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \Forall mk-Msg(\beta,\alpha,vl)\in\hbox{\bf elems\kern 1.66672pt\/}\nobreak{as}\suchthat\hfil\break\hbox to409.75496pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\Forall i\in\hbox{\bf inds\kern 1.66672pt\/}\nobreak{vl}\suchthat\hfil\break\hbox to399.75494pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}vl(i)\in Uid\penalty-35\mskip 6.0mu plus 2.0mu minus 1.0mu\Rightarrow\mskip 6.0mu plus 2.0mu minus 1.0muvl(i)=\alpha$}\hss}$}\hss}$  

The following dynamic invariant also holds on the states: this requires that nothing can change an $\mathit{}Action$ that has occurred, a user’s conformity cannot change and that users retain all the information that was added to $\mathit{}knows$.

$\mathit{}\hbox{$\mathit{}dyn-inv$}(\sigma,\sigma^{\prime})\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \sigma.history\subseteq\sigma^{\prime}.history\land\newline \Forall u\in\sigma.users\suchthat\hfil\break\hbox to409.75496pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\Forall sess\in\hbox{\bf dom\kern 1.66672pt\/}\nobreak\sigma.knows(sess)\suchthat\hfil\break\hbox to399.75494pt{\hbox{\bf\quad\/}\vtop{\noindent$\mathit{}\sigma.users(u).knows(sess)\subseteq\sigma^{\prime}.users(u).knows(sess)\land\newline \sigma^{\prime}.users(u).conforms=\sigma.users(u).conforms$}\hss}$}\hss}$  

An optimistic overall objective can be captured by the specification given in Fig. 1. The argument is that N-S and the NS(L) code satisfies this strong specification and that Lowe’s extension (see Section 4) also does something sensible (aborts) in the case of Lowe’s attack.

The pseudo-code for NS is given in Fig. 2, which uses statements with the following semantics:
$\mathit{}\hbox{\bf invent\/}:history:\mathbin{\hbox{\raise 4.30554pt\hbox{$\mathit{}\@sc@nc$}}}mk-Invent(me,n)$ ($\mathit{}n$ is completely new)
$\mathit{}\hbox{\bf send\/}(to,b):\mathbin{\hbox{\raise 4.30554pt\hbox{$\mathit{}\@sc@nc$}}}mk-Msg(to,this,b)$
$\mathit{}\hbox{\bf rcv\/}\cdots$: picks up the most recent unread $\mathit{}Msg$ whose $\mathit{}rec$ field matches $\mathit{}this$.
Analogous with $\mathit{}x:+1$, $\mathit{}s:\cup t$ sets the final value of $\mathit{}s$ to $\mathit{}s\cup t$, etc.

The correctness of the decomposition of $\mathit{}NS1$:

$\mathit{}NS1=sender(to)\parallel receiver()\parallel other$

$\mathit{}\hbox{$\mathit{}subseq$}(s1,s2)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad{\Exists sel\in\Bool^{*}}\suchthat\hbox{\bf len\kern 1.66672pt\/}\nobreak{sel}=\hbox{\bf len\kern 1.66672pt\/}\nobreak{s2}\land select(sel,s2)=s1$  

$\mathit{}\hbox{$\mathit{}select$}(sel,s)\quad\raise 2.15277pt\hbox{\footnotesize\text@underline{$\mathit{}\mathchar 12852\relax$}}\penalty-100\quad\newline \vtop{\hbox to0.0pt{\hbox{\bf if \/}\vtop{\noindent$\mathit{}sel=[\,]$}\hss}\hbox to0.0pt{\hbox{\bf then \/}\vtop{\noindent$\mathit{}[\,]$}\hss}\hbox to0.0pt{\hbox{\bf else \/}\vtop{\noindent$\mathit{}{\hbox to0.0pt{\vtop{\noindent$\mathit{}\hbox{\bf if \/}\nobreak\hbox{\bf hd\kern 1.66672pt\/}\nobreak{sel}\penalty 0\hskip 5.0pt\hbox{\bf then \/}\nobreak[\hbox{\bf hd\kern 1.66672pt\/}\nobreak{s}]\mathbin{\hbox{\raise 4.30554pt\hbox{$\mathit{}\@sc@nc$}}}select(\hbox{\bf tl\kern 1.66672pt\/}\nobreak{sel},\hbox{\bf tl\kern 1.66672pt\/}\nobreak{s})\penalty-100\hskip 5.0pt\hbox{\bf else \/}\nobreak select(\hbox{\bf tl\kern 1.66672pt\/}\nobreak{sel},\hbox{\bf tl\kern 1.66672pt\/}\nobreak{s})$}\hss}}$}\hss}}$   pre $\mathit{}\hbox{\bf len\kern 1.66672pt\/}\nobreak{sel}=\hbox{\bf len\kern 1.66672pt\/}\nobreak{s}$

Proof. Providing there are no other messages, the combined code would have the same effect as the obvious combined code. If there is another message before the first rcv in $\mathit{}receiver$, it would initiate a separate session. Because of the assumptions in $\mathit{}no-read-others$, no $\mathit{}other$ user can generate a $\mathit{}Msg$ that is accepted by the rcv in $\mathit{}sender$. The argument is similar for the second rcv in $\mathit{}receiver$.

Proof. This holds because the chosen nonces are created by invent.

The dynamic invariant $\mathit{}dyn-inv$ requires that $\mathit{}history$ is only extended, which is true of both processes.

Proof. The $\mathit{}sender$ operation transmits a nonce ($\mathit{}Nt$) that it received in a $\mathit{}Msg$, but it returns it to the $\mathit{}Uid$ from where it appeared to have been sent, and similarly for $\mathit{}Nf$ in $\mathit{}receiver$.

Proof. Only $\mathit{}sender$ (in pure $\mathit{}NS$) includes a $\mathit{}Uid$ in the body of a $\mathit{}Msg$, which is not a forgery because it sends its own $\mathit{}Uid$ ($\mathit{}this$).