Symbolic Cryptographic Protocol Constraint Solving

The constraint solver is a protocol security analyzer implemented in Prolog and documented in "Constraint Solving for Bounded-Process Cryptographic Protocol Analysis," presented at ACM CCS-8 in 2001. To run the analyzer, you must (1) download the Prolog Constraint Solver program, (2) install the SWI-Prolog interpreter, (3) specify a protocol of interest in a Prolog representation of a strand space model, (4) specify a security objective and test environment, and (5) invoke the solver.

Download the Program

The version of the constraint solver in the file csolve.pl (rename csolve_pl.txt to csolve.pl after downloading) is slightly extended beyond what is described in the CCS-8 paper. It allows n-ary (non-associative) concatenation, not just binary. It assumes that the attacker knows all public keys pk(A), and it includes a routine for displaying message sequence diagrams in addition to the usual text output of solution traces. This version uses three nonstandard predicates of SWI-Prolog (term_to_atom, gensym, reset_gensym). It can be used only on specifications where each message has the following restricted 3-item-list format: [sender, receiver, term].

Here is an example diagram produced by csolve, for the well-known attack on the Needham-Schroeder public-key protocol. The end columns have labels that change to specify the active principal, but the middle column always represents the attacker "e". The message syntax will be explained below under specification format.

a                                     |                                     |
|                  e                  |                                     |
|<------------------------------------|                                     |
|                                     |                                     e
|            [a, na]*pk(e)            |                                     |
|------------------------------------>|                                     |
|                                     |                                     b
|                                     |            [a, na]*pk(b)            |
|                                     |------------------------------------>|
a                                     |                                     |
|                                     |           [na, nb]*pk(a)            |
|                                     |<------------------------------------|
|                                     |                                     e
|           [na, nb]*pk(a)            |                                     |
|<------------------------------------|                                     |
|              nb*pk(e)               |                                     |
|------------------------------------>|                                     |
|                                     |                                     b
|                                     |              nb*pk(b)               |
|                                     |------------------------------------>|
|                                     |                                     e
|                                     |                 nb                  |
|                                     |------------------------------------>|
There is a version of the constraint solver with improved performance, due to R. Corin and S. Etalle, at U. Twente in the Netherlands, called CoProVe. It checks for solvability of a constraint set incrementally as node sequences are constructed. A modified version of their code is included here as coproved.pl (rename _pl.txt to .pl). The modifications allow it to use the same specifications and the same search commards as csolve. It invokes the separate display program showp.pl (rename _pl.txt to .pl).

A new experimental extension of csolve called csolvex adds an invertible signature syntax A//P where P is atomic (and should be a principal) and A can be read from the signature, like a certificate. Download the program as csolvex.pl (rename _pl.txt to .pl). The separate display program showp.pl is needed for csolvex.

Install Prolog

The constraint solver is written for SWI-Prolog, but it will run, with minor modifications, on any Prolog interpreter supporting standard Edinburgh Prolog. The three nonstandard predicates mentioned earlier are used only for the diagram output, which can be removed by commenting out the call on showp. SWI-Prolog versions for Unix, Windows, and Macintosh can be downloaded from the SWI-Prolog Website.

Specify a Protocol

Protocols are specified in a variant of the strand space model (Thayer, Herzog and Guttman, "Strand spaces: proving security protocols correct", JCS 7(2/3), 1999, 191-230). This kind of protocol specification can be produced manually with little difficulty.

Each role in a protocol is specified as a sequence of messages it sends and receives. The message sequence can be specified by defining a Prolog predicate strand(role,A,B,...,[messages]), where role is a constant naming the role, A, B, ... are protocol variables, and the messages are triples [P, Q, M] where P and Q are the sender and receiver, and M is the message represented in a term syntax given below.

For example, consider the Needham-Shroeder Public-Key (NSPK) protocol, whose message list might appear in a textbook as:
A → B: {A,Na}pk(B);
B → A: {Na, Nb}pk(A);
A → B: {Nb}pk(B);
The A-role strand would appear in Prolog as:
strand(roleA,A,B,Na,Nb,[ 
  send([A,B,[A,Na]*pk(B)]),
  recv([B,A,[Na,Nb]*pk(A)]),
  send([A,B,Nb*pk(B)])
]).
This is actually a schema or "parametric" strand because it contains variables (beginning with capital letters in Prolog). In the Prolog strand version, roleA is a constant naming the initiator role. Concatenation is indicated using the Prolog list brackets [,]. Public-key encryption is denoted with an infix * operator, and symmetric-key encryption with an infix + operator. The period (.) following the strand term is Prolog syntax causing the strand term to be declared as a "fact."

The program is limited in its vocabulary of operators available to the attacker. The only other operators available are sha( ) for a hash function and infix / to represent a signature. In particular, the term X/pk(A) is the signature of X by A. This kind of signature is not invertible; it represents an encrypted hash rather than just public-key encryption with the private key, and the form pk(A) must follow the / for some identifier A representing a principal.

A new experimental extension called csolvex adds an invertible signature //, where A//B is expanded internally to [A,A//B] before solving. The only new reduction rule allows A//e to be constructed from A.

Other functional operators, e.g., f(A), may be used. All such new functions may appear in legitimate strands, but they are neither computable nor invertible by the attacker.

To specify a strand fully, it is also essential to know which variables are nonces for that role, i.e., variables that will be chosen to have constant values unique to each instantiation of the strand. For the A-role strand, the variable Na is the only nonce. (Although Nb is also a nonce, it is not chosen by the A-role, but rather received in a message, and the A-role principal has no way to know that its value is unique. Nb will, however, be a nonce for the B-role.) In any test bundle, nonce variables must be instantiated with (symbolic) constants in each strand that generates them, and nonce constants must be different for each strand.

There is a general restriction on strands in test bundles, called the origination assumption: a variable always occurs for the first time in a "recv" message. This is certainly true for nonces generated in a different role. However, other variables, such as the names of principals in the first sent message, must also be instantiated somehow. This can be done either by replacing them by symbolic constants in the test bundle, or by having the attacker choose them (since the attacker can be assumed to know principal names and other public data).

To have the attacker choose data for a sender's variables, The sender role can be given an artificial initial recv message from the attacker with the attacker-chosen values. This is appropriate for a worst-case analysis. In our example, role A could initially receive the message
   recv([e,A,B])
to allow the attacker to choose the responder principal.

The B-role strand appears in Prolog as:
strand(roleB,A,B,Na,Nb,[
  recv([A,B,[A,Na]*pk(B)]),
  send([B,A,[Na,Nb]*pk(A)]),
  recv([A,B,Nb*pk(B)])
]).

Specify a Test Environment

A test environment is a list of strands forming a "semibundle". The semibundle contains all of the strand instantiations that will be considered in the analysis run. Besides the instantiations of the specified roles, the semibundle contains a "test" strand to detect confidentiality violations. While it is possible to set up authentication property tests, only a test for confidentiality of a nonce will be illustrated below.

In Prolog, a semibundle is represented by a list term containing strands in which generated nonces have been instantiated with (symbolic) constants. For example, a semibundle with one A-role strand and one B-role strand could be defined as:
  nspkn([Sa,Sb]) :- 
    strand(roleA,A,B,na,Nb,Sa),
    strand(roleB,A,B,Na,nb,Sb).
Constants in Prolog begin with a lower-case letter, so Na in the A-role has been instantiated with a constant na and Nb in the B-role has been instantiated with a constant nb. As it stands, this semibundle could be presented to the constraint solver to test the reachability of a normal execution of the protocol, with no security objective.

In the NSPK example, the nonces Na and Nb should be confidential. Testing for compromise involves defining a new test strand:
  strand(test,N,[recv([e,e,N])])
In the semibundle used for analysis, the argument N is instantiated with the nonce (na or nb, for example) being tested for confidentiality. The idea of the test strand is that if an attacker compromises the secret nb, it is possible for that attacker to send nb as a message that can be received by anyone, in particular e, in the test strand.

The semibundle used for analysis must include all legitimate strands that are being considered for participation in the environment. Thus, in order to test for an attack involving two sessions of the protocol, strands for both sessions must be included. Three sessions would take a larger semibundle, and so on.

To find the attack on NSPK, it is sufficient to present a semibundle for one A-role strand and one B-role strand, given below.
nspk0([Sa,Sb,St]) :-
  strand(roleA,A,B,na,Nb,Sa),
  strand(roleB,a,b,Na,nb,Sb),
  strand(test,nb,St).
In the B-strand, the principals A and B have been instantiated by constants a and b, because the confidential nonce nb originated in that strand was intended by some particular responder b to be shared with some particular initiator a. If A and B were left as variables, the solver would find a solution in which the attacker e was the legitimate initiator, and that would not actually be an attack.

The protocol specification and environment semibundles should be placed in one or more text files so that they can be loaded by the Prolog interpreter. The NSPK example is in nspk_pl.txt (rename to nspk.pl).

Invoke the Solver

Start Prolog in whatever way is appropriate for your installation, as detailed in the SWI-Prolog Website. Navigate if necessary to the folder or directory containing the solver and protocol files. Note that SWI-Prolog has a predicate working_directory/2 for checking and changing the current directory.

At the Prolog prompt, load the solver and protocol files like this:
| ?- [csolve,nspk].
This works if the files have the extension ".pl" and are in the current directory. Otherwise you will need pathnames, such as 'specs/nspk.pl' instead of just nspk. (The quotes ensure that Prolog will not misinterpret / and . as operators.)

The main solver predicate is search(B,I,A) where B is a semibundle, I is a list of terms initially known to the attacker, and A is an "authentication message", which will be explained later. It is set to [ ] (the empty list) when the security objective is secrecy rather than authentication.

The search query may be called with a two-argument form search(B,A). This is translated to search(B,[a,b,e],A). The attacker is always "e". (The initial knowledge list argument should be specified explicitly if some list other than [a, b, e] is desired.)

Thus, a complete test query would be:
| ?- nspk0(B),search(B,[]).
Prolog will then respond with either "false", meaning that no complete bundle consistent with the given semibundle is reachable, or "true" together with an instantiation for B.

In this example, we get some search trial output, followed by the diagram shown earlier and the text of the solution:
Trace:
recv([e,a,e])
send([a,e,[a,na]*pk(e)])
recv([a,b,[a,na]*pk(b)])
send([b,a,[na,nb]*pk(a)])
recv([e,a,[na,nb]*pk(a)])
send([a,e,nb*pk(e)])
recv([a,b,nb*pk(b)])
recv([e,e,nb])

Bundle:
[recv([e,a,e]),send([a,e,[a,na]*pk(e)]),recv([e,a,[na,nb]*pk(a)]),
               send([a,e,nb*pk(e)])]
[recv([a,b,[a,na]*pk(b)]),send([b,a,[na,nb]*pk(a)]),recv([a,b,nb*pk(b)])]
[recv([e,e,nb])]
The "Trace" shows the sequence of messages sent and received, and the "Bundle" is the bundle B instantiated. In the compromise, the A-role strand conducted a normal session with e, and the B-role had a normal-looking session apparently with a, but its secret nonce nb was sent by a to e.

The NSL Type Flaw

The Needham-Schroeder-Lowe (NSL) protocol changes the second message [Na,Nb]*pk(A) to [Na,Nb,B]*pk(A) to fix the problem in NSPK. A variety of this version still has a type-flaw vulnerability, summarized below. To work, this attack requires b to accept a principal e as a nonce, and it requires a to accept a pair [nb, b] as a nonce. The flawed protocol is actually a variant of the original NSL protocol, in which the first message is [Na, A] rather than [A, Na].

Session 1: e masquerades as a; b generates nb to share with a
Session 2: e initiates, a responds; nb is compromised
a(e) → b: [a, e]*pk(b)
b → a(e): [e, [nb, b]]*pk(a)

e → a: [e, [nb, b]]*pk(a)
a → e: [[nb, b], [na, a]]*pk(e)
The problem goes away when the original form of the first message is used. It also goes away when triple concatenations are expressed with ternary concatenation rather than nested binary concatenation. The NSL version with the flaw is in nsla.pl and the version with ternary concatenation is in nsl.pl (change _pl.txt to .pl).

Stopping and Authentication

The constraint solver has features to support early exit and authentication. Normally, the search predicate attempts to find a bundle in which all strands in the semibundle are completed, in the sense that every received message has been proved to be derivable by the attacker. However, if any strand sends the message "stop" (either send(stop) or send([a, b, stop])), once that message has been sent, the search is terminated. The "stop" feature makes it possible to terminate the search immediately once a secret has been compromised, or when an authentication goal can be tested. The send-stop message can be added to the test strand for a compromise goal.

The argument A of the search call search(B,I,A) is used to support authentication goals of a type often referred to as agreement goals. An authentication (agreement) goal may be expressed as "if roleB has reached a state instantiating certain parameters, e.g., B = bob, A = alice, K = ks, etc., then there must be an instance of roleA in the same bundle, agreeing with roleB on the corresponding parameters of roleA."

Alice's state can be signalled with an artificial authentication message like
[A,B,roleA(A,B,Nb)] that indicates Alice's role and agreement parameters. This message can be added to the specification at any spot where the parameters are fully defined. (The roleA term is treated by csolve as an unknown function that is not computable or invertible by the attacker.)

Then, if roleA(a,b,nb) (for example) is specified as the authentication argument in the search call, instantiated with Bob's values, the solver will search only for traces that do not contain that authentication message. If the search succeeds without seeing it, it must indicate a failure of the agreement property.