Verifying cryptographic protocols, II: a simple example
[general verification automation Not long ago I wrote about cryptographic protocols and their verification. In this post, we shall see a simple example: the famous Needham-Schroeder public key protocol and its verification using Isabelle/HOL. The protocol will be the version as corrected by Lowe: the original provides weaker guarantees and is harder to reason about. Only highlights can be shown here. The proofs rely on a lot of formal machinery, which is described in the journal paper (also available here). For many people, crypto protocol verification rather than Isabelle seems to be my main research achievement, and yet they can’t really be separated: these techniques don’t seem to be reproducible in those proof assistants that have weaker automation, namely, all of them. I know that an attempt was made using a Certain Verification System.
Messages and operations on them
Lowe’s work was the starting point for much of the work on protocol verification undertaken during the late 1990s, and sometimes it was even acknowledged. It completely superseded earlier work on authentication logics such as BAN, which although celebrated at first, didn’t yield reliable results. In particular, BAN validates the incorrect version of the protocol discussed here.
First, we set up a common framework for analysing security protocols in general. The principals or agents consist of a trusted authentication server (required by many protocols), infinitely many friendly agents, and the intruder or Spy.
datatype agent = Server | Friend nat | Spy
Messages are constructed by hashing, concatenation or encryption over the four primitive message elements: agent names, etc.
datatype msg = Agent agent ― ‹Agent names› | Number nat ― ‹Ordinary integers, timestamps, ...› | Nonce nat ― ‹Unguessable nonces› | Key key ― ‹Crypto keys› | Hash msg ― ‹Hashing› | MPair msg msg ― ‹Compound messages› | Crypt key msg ― ‹Encryption, public- or shared-key›
The formalisation of crypto keys is omitted here. Briefly: keys are integers and every key has an inverse, which in the case of shared-key encryption is identical to the key itself. No encryption algorithms are formalised.
Several operators are defined inductively to specify what can be derived
from a set of (presumably intercepted) messages.
For reasoning about secrecy, analz specifies the set of message components that can be extracted from a given set.
The body of an encrypted message becomes available
if the decryption key is available.
inductive_set analz :: "msg set ⇒ msg set" for H :: "msg set" where Inj [intro,simp]: "X ∈ H ⟹ X ∈ analz H" | Fst: "⦃X,Y⦄ ∈ analz H ⟹ X ∈ analz H" | Snd: "⦃X,Y⦄ ∈ analz H ⟹ Y ∈ analz H" | Decrypt: "⟦Crypt K X ∈ analz H; Key(invKey K) ∈ analz H⟧ ⟹ X ∈ analz H"
The function parts (omitted here) is an over-approximation of analz,
defined similarly except that decryption does not require a key.
It is useful for reasoning about all secrets that have been communicated,
whereas analz is for reasoning about secrets that are no longer secret.
The function synth describes the set of messages that could be synthesised
from a given set of message components.
It is here that the “unguessable” property of keys and nonces
is formalised. All numbers are guessable
(this makes sense for small integers, and timestamps).
To create an encrypted message, you need the encryption key.
inductive_set synth :: "msg set => msg set" for H :: "msg set" where Inj [intro]: "X ∈ H ⟹ X ∈ synth H" | Agent [intro]: "Agent agt ∈ synth H" | Number [intro]: "Number n ∈ synth H" | Hash [intro]: "X ∈ synth H ⟹ Hash X ∈ synth H" | MPair [intro]: "⟦X ∈ synth H; Y ∈ synth H⟧ ⟹ ⦃X,Y⦄ ∈ synth H" | Crypt [intro]: "⟦X ∈ synth H; Key(K) ∈ H⟧ ⟹ Crypt K X ∈ synth H"
Innumerable properties are for these operators by simple inductions. They turn out to be idempotent and monotonic. Identities are proved to simplify the arguments of the operators, for example to pull out inserted elements. We can pull out an inserted nonce, for example:
lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
There is no analogous law for inserted keys because keys can be used to decrypt.
Among the more interesting laws is the following, which shows that synthesis can be decoupled from analysis. Suitable laws are proved for all combinations of the operators in order to simplify nested expressions.
lemma analz_synth [simp]: "analz (synth H) = analz H ∪ synth H"
The most critical combination is synthesis of analysis,
for that is what the Spy does: break down past traffic,
then combine the components into new messages.
The following theorem allows us to eliminate an occurrence
of such a fake message X from the argument of analz,
which turns out to provide a general method for
solving the subgoal corresponding to a fake message.
lemma Fake_analz_insert: "X ∈ synth (analz G) ⟹ analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H)"
Events, traces and other basic notions
Protocols are formalised with respect to a “God’s eye” trace model. The trace holds all message send attempts from the beginning of time, including multiple protocol runs possibly interleaved with any number of parties.
datatype event = Says agent agent msg | Gets agent msg | Notes agent msg
The event Says A B X represents the attempt by agent A to send message X to agent B.
This was at one point the only event in the model.
Later I introduced Notes, to represent the local storage of an agent and also
information leakage outside the protocol.
Giampaolo Bella, one of my PhD students, introduced Gets to signify the reception of a message
by a specific agent, who (because the Spy controls the network)
has no way of knowing who the true sender was.
Giampaolo felt that the explicit Gets event made for clearer protocol specifications.
Giampaolo went on to do an enormous amount of work on protocol verification,
including timestamp-based protocols, smartcard protocols and other advanced configurations, and even wrote a book on the subject.
(Later still, Jean Martina
investigated multicast protocols.)
But I never updated the Needham-Schroeder formalisation, so we don’t need
Gets here.
The basic model includes several other primitives, which can be briefly described as follows:
bad: the set of compromised agents (their keys are known to the Spy)used: the set of all message components ever sent, whether visible or notspies: the set of message components visible to the SpypubEK: the public encryption key of a given agent
Formalising the protocol
The earlier post described the Needham–Schroeder public key protocol and mentioned the flaw found by Gavin Lowe. The corrected protocol mentions $B$ in message 2:
\[\newcommand\Na{\mathit{Na}} \newcommand\Nb{\mathit{Nb}} \newcommand\Ka{\mathit{Ka}} \newcommand\Kb{\mathit{Kb}} \def\lbb{\mathopen{\{\kern-.30em|}} \def\rbb{\mathclose{|\kern-.32em\}}} \def\comp#1{\lbb#1\rbb} \begin{alignat*}{2} &1.&\quad A\to B &: \comp{\Na,A}_{\Kb} \\ &2.&\quad B\to A &: \comp{\Na,\Nb,B}_{\Ka} \\ &3.&\quad A\to B &: \comp{\Nb}_{\Kb} \end{alignat*}\]A reminder of the notation. Some arbitrary principal “Alice” decides for some reason to run the protocol with some other principal, “Bob” and sends the first message (which contains a fresh random number). Upon the receipt of what appears to be an instance of message 1, Bob can continue the protocol by sending message 2 (containing another random number) back to Alice. Alice, upon receiving message 2, checks that it has the correct form, which for this version of the protocol involves confirming both her nonce and the name $B$. If everything is okay, she sends message 3, and if Bob actually receives this message, he will check for his nonce and that will constitute a successful run. If any of the messages fail to get through or do not have the required form, the protocol attempt will simply be abandoned.
We reason informally about such a protocol by saying for example “Bob knows Alice is present by message 3, when his nonce challenge was correctly returned to him. Only Alice could have done this, because that nonce was encrypted using her public key.” This is inductive reasoning, so it’s not surprising that a cryptographic protocol can naturally be modelled by an inductive definition, effectively an operational semantics.
inductive_set ns_public :: "event list set" where Nil: "[] ∈ ns_public" ― ‹Initial trace is empty› | Fake: "⟦evsf ∈ ns_public; X ∈ synth (analz (spies evsf))⟧ ⟹ Says Spy B X # evsf ∈ ns_public" ― ‹The spy can say almost anything.› | NS1: "⟦evs1 ∈ ns_public; Nonce NA ∉ used evs1⟧ ⟹ Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) # evs1 ∈ ns_public" ― ‹Alice initiates a protocol run, sending a nonce to Bob› | NS2: "⟦evs2 ∈ ns_public; Nonce NB ∉ used evs2; Says A' B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs2⟧ ⟹ Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) # evs2 ∈ ns_public" ― ‹Bob responds to Alice's message with a further nonce› | NS3: "⟦evs3 ∈ ns_public; Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs3; Says B' A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ set evs3⟧ ⟹ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 ∈ ns_public" ― ‹Alice proves her existence by sending @{term NB} back to Bob.›
We formalise a protocol by specifying the possible traces of messages that could be sent
over the network. Starting with the empty trace our possibilities are any of the three protocol messages or a Fake message from the Spy, using the synth and analz operators
to generate arbitrary messages.
Some aspects of the formalisation of the protocol messages deserve comment.
- Protocol message
NS1, says that any trace can be extended by a message containing a nonceNAthat has never appeared before. That knowledge is not available, but the constraint can be achieved with high probability simply by generating a random number. - Message
NS2extends the trace (including another random number) provided a suitable copy of message 1 has already appeared. The decryption of that message is implicit in requiring that it be encrypted with B’s public key. The sender of the message 1 is written as A’ because it is not possible to know who the true sender of a message is (ascertaining this is the very purpose of authentication). - Again for message
NS3, the comparison between the instance message 2 just received and the message 1 originally sent is implicit in the formulation itself, with no decryption or comparison operations necessary.
It’s nice that the formal specification is so close to the conventional notation. It’s not cluttered with any implementation details. That’s also a reminder that the proof offers no guarantees against implementation errors.
Some properties proved of this protocol
Our protocol model only allows the proof of safety properties, i.e., that all executions are safe. It cannot prove liveness properties, because the Spy has the power to prevent anything from happening by intercepting all messages. With this sort of model, if you make a mistake and specify a protocol that simply cannot run (typically because the message formats aren’t consistent), then all the safety properties will hold vacuously. Therefore the first thing to do is run a little sanity check. The following result isn’t interesting except to show that traces exist in which the final protocol message is actually sent. The proof involves simply joining up the protocol rules in the correct order and checking that the side conditions can be satisfied.
lemma "∃NB. ∃evs ∈ ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) ∈ set evs"
The objectives of the protocol are sufficiently vague (“Alice and Bob are authenticated to one another”) that we need to decide for ourselves what to prove. The following are technical properties that turned out to be necessary in order to prove more clear-cut properties about secrecy. As so often happens in machine proofs, they look too easy to bother with. First we prove that it is impossible for a nonce used in message 1 to be identical to a nonce used in message 2 (intuitively, because they are chosen randomly).
lemma no_nonce_NS1_NS2: "⟦evs ∈ ns_public; Crypt (pubEK C) ⦃NA', Nonce NA, Agent D⦄ ∈ parts (spies evs); Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs)⟧ ⟹ Nonce NA ∈ analz (spies evs)" by (induct rule: ns_public.induct) (auto intro: analz_insertI)
Next comes what I have called a unicity property: that a particular nonce uniquely identifies all the message components bound up with it. This fact relies on the assumption that the nonce in question is not known to the Spy, who could otherwise do anything with it. Honest agents generate a fresh nonce every time, hence this property.
lemma unique_NA: assumes NA: "Crypt(pubEK B) ⦃Nonce NA, Agent A ⦄ ∈ parts(spies evs)" "Crypt(pubEK B') ⦃Nonce NA, Agent A'⦄ ∈ parts(spies evs)" "Nonce NA ∉ analz (spies evs)" and evs: "evs ∈ ns_public" shows "A=A' ∧ B=B'"
The proofs start to get messier, so I prefer to omit some of them.
A dogmatic approach to structured proofs doesn’t work in verification generally,
where proof steps can easily generate gigantic subgoals.
And by the way: the reason the trace variable has distinctive names evs1,
evs2, evs3 is to make it easy to see which protocol rule we are talking about
in a messy, non-structured induction.
The following theorem is a key protocol objective: Alice’s nonce from message 1 will remain forever secret from the Spy, provided both Alice and Bob are trustworthy.
theorem Spy_not_see_NA: assumes NA: "Says A B (Crypt(pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs" "A ∉ bad" "B ∉ bad" and evs: "evs ∈ ns_public" shows "Nonce NA ∉ analz (spies evs)" using evs NA proof (induction rule: ns_public.induct) case (Fake evsf X B) then show ?case by spy_analz next case (NS2 evs2 NB A' B NA A) then show ?case by simp (metis Says_imp_analz_Spy analz_into_parts parts.simps unique_NA usedI) next case (NS3 evs3 A B NA B' NB) then show ?case by simp (meson Says_imp_analz_Spy analz_into_parts no_nonce_NS1_NS2) qed auto
An analogous property can be proved for Bob’s nonce from message 2. It doesn’t hold for the original, flawed version of Needham–Schroeder.
The following theorem authenticates Bob to Alice. More formally, if Alice has sent message 1 and receives a copy of message 2 containing a copy of the nonce that she sent, then it was in fact sent by Bob.
theorem A_trusts_NS2: "⟦Says A B (Crypt(pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs; Says B' A (Crypt(pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ set evs; A ∉ bad; B ∉ bad; evs ∈ ns_public⟧ ⟹ Says B A (Crypt(pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ set evs"
And this theorem authenticates Alice to Bob.
theorem B_trusts_NS3: "⟦Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ set evs; Says A' B (Crypt (pubEK B) (Nonce NB)) ∈ set evs; A ∉ bad; B ∉ bad; evs ∈ ns_public⟧ ⟹ Says A B (Crypt (pubEK B) (Nonce NB)) ∈ set evs"
The last two properties above guarantee to Alice and Bob that the other person indeed participated in the protocol. The secrecy properties assure them that the nonces they exchanged are available to them alone. A practical application of this protocol might involve calculating a session key from those nonces in order to transmit a serious amount of data.
Postscript
It’s careless to talk about “verifying” anything unless it has a definitive formal specification. A cryptographic protocol — the last time I looked, admittedly quite a while ago — is typically proposed through an RFC, a mixture of prose and technical diagrams showing the formats of messages down to bitfield boundaries. The aims will be taken for granted (“establish secure communications”) with little discussion of specific protocol objectives and no abstract protocol design independent of its machine implementation. As discussed in the earlier post, ambiguity about the original protocol’s security assumptions resulted in disagreements among experts as to whether it was correct or not.
If you check the corresponding formal development online, you will find much uglier proofs than those shown here. I took the opportunity to beautify them, but the new proofs will not be visible until the release of Isabelle2023.
My colleagues and I wrote numerous papers on protocol verification. But my proofs are too labour intensive. Others have taken the field forward, and crypto protocol verification is today done almost exclusively by fully automatic techniques.