Symbolic Cryptographic Protocol Constraint Solving

Download the Program

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                  |
|                                     |------------------------------------>|

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

Specify a Protocol

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

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

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

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 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.