Constraint Solving in Prolog
Download the ProgramThe version of the constraint solver in the file csolve.P 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) (though this assumption can be removed easily), and it includes a mutual shared-symmetric-key lookup function msk(A,B) such that msk(A,B) = msk(B,A) and the attacker "e" knows msk(e,A) for all A. This version finds the type-flaw vulnerability in one version of the Needham-Schroeder-Lowe protocol.
There is a faster version of the constraint solver due to Corin and Etalle at the University of Twente, in Holland [CE02]. It checks for solvability of a constraint set incrementally as node sequences are constructed. Corin's web page has downloadable code and an online demonstration. A modified version of their code is included here as mysv.P. The modifications are for compatibility with csolve.P, so the same protocol specifications can be used.
Several example protocol specifications are in this directory.
Install PrologThe constraint solver will run, possibly with minor modifications, on any Prolog interpreter supporting standard Edinburgh Prolog. Two web sites from which a public-domain Prolog interpreter can be obtained are given below. Prolog implementations for UNIX, Windows, and Macintosh are available. XSB Prolog has the advantage that it supports "tabling," a kind of memoizing that causes an order-of-magnitude performance improvement in analyses (but it can also run out of tabling space in complex examples). The tabling control statement is commented out in the csolve.P and mysv.P files for transportability, but it should be restored if you use XSB Prolog.
Specify a ProtocolProtocols are specified in a variant of the strand space model (see [THG99] in the bibliography). A connector translating from CAPSL to this representation is in preparation, but 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 is represented as a Prolog term of the form strand(role,A,B,...,[messages]), where A, B, ... are protocol variables and the messages are represented in a term syntax given below.
For example, consider the Needham-Shroeder Public-Key (NSPK) protocol, whose message list might appear in CAPSL 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,Na]*pk(B)), recv([Na,Nb]*pk(A)), send(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 A-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, and does not cover the CAPSL prelude. 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.
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.) As described in the paper, there is an additional restriction on the strand specification, called the origination assumption: a variable always occurs for the first time in a "recv" message (except for nonces generated in the strand; these will be instantiated with symbolic constants in the semibundle to be analyzed). This means that the A-role strand is not correct as it stands. We add a new initial message in which the variables A, B are received:
recv([A,B]),With this new first message, the A-role strand satisfies the origination assumption.
The B-role strand appears in Prolog as:
strand(roleB,A,B,Na,Nb,[ recv([A,Na]*pk(B)), send([Na,Nb]*pk(A)), recv(Nb*pk(B)) ]).
Specify a Test EnvironmentA test environment is a list of strands forming a "semibundle," in the strand space sense. 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 that detects security 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:
semibundle_1([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(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 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 to ensure that the confidential nonce nb originated in that strand was not intended to be shared with a principal under the control of the attacker. By convention, the attacker, when acting as a principal, has the name "e" (for enemy), in the constraint solver.
Invoke the SolverThe protocol specification and environment semibundles should be placed in one or more text files so that they can be loaded by the Prolog interpreter. Several protocol examples are given in this directory.
There is an individual file for the Needham-Schroeder Public Key handshake, called nspk.P. (The ".P" extension is an XSB convention. In SWI-Prolog, the corresponding convention is "_pl", as in csolve_pl. A file nspk.P could still be loaded by protecting the dotted name in quotes, as 'nspk.P'.)
At the Prolog prompt, load the solver and protocol files:
| ?- [csolve,nspk]. [csolve loaded] [nspk loaded] yesIn XSB Prolog, it is also necessary to load the system file "basics" which contains some list processing predicates.
The main solver predicate is search(B,A) where B is a semibundle, and A is an "authentication message" that will be explained later, and can be set to  (the empty list) when the security objective is secrecy rather than authentication. (This predicate is essentially a wrapper on a more flexible predicate search with more arguments, for convenience.)
Thus, a complete test query would be:
| ?- nspk0(B),search(B,).Prolog will then respond with either "no", meaning that no complete bundle consistent with the given semibundle is reachable, or "yes" together with instantiations for B and F.
In this example, we get some search trial output, followed by the solution:
Trace: recv([a,e]) send([a,na] * pk(e)) recv([a,na] * pk(b)) send([na,nb] * pk(a)) recv([na,nb] * pk(a)) send(nb * pk(e)) recv(nb * pk(b)) recv(nb) Bundle: [recv([a,e]),send([a,na] * pk(e)),recv([na,nb] * pk(a)), send(nb * pk(e))] [recv([a,na] * pk(b)),send([na,nb] * pk(a)),recv(nb * pk(b))] [recv(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.
You can download the NSPK specification. This specification has some additional messages related to authentication.
The NSL Type FlawWe also have a version of the NSL specification; this 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 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
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.
Stopping and AuthenticationThe constraint solver, both csolve and mysv versions, 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", once that message has been sent, the bundle is considered successfully reached. The "stop" feature makes it possible to terminate the search immediately once a secret has been compromised.
The search call search(B,A) has a second argument that is used to support authentication tests. An authentication goal may be expressed as "if Bob has reached a stop state, then there must be an instance of Alice in the same session, i.e., agreeing with Bob on certain parameters (nonce, session key, Alice and Bob's identity, etc.)." Bob's stop state can be indicated with a stop message (add "send(stop)" to Bob's strand). Alice's presence can be signalled with an artificial message like "send(roleA(A,B,Nb))" that indicates Alice's role and agreement parameters. If this form is specified as the second argument in the search call, appropriately instantiated, the solver will search only for traces that reach "stop" but which do not contain the authentication message, and which therefore indicate a failure of the authentication property. (In the nspk.P file supplied, the stop message is sent by a separate strand so that the same specification can be used to test secrecy without missing cases where the secret is exposed after Bob finishes.)
Connector from CILIf you have a CIL specification produced using the CAPSL translator, a "connector" can be used to translate it further to the Prolog form required by the constraint solver. The cil2pbundle Java connector is in the tar file tobundle.tar. This file contains the necessary Java classes and a CIL spec of NSPK. The connector is invoked with, for example,
The connector creates strands for legitimate parties as specified, plus one test strand for a variable data item.
Alternatively, download the jar file tobundle.jar (don't just click, use the "Save Link Target" or similar function in your browser) and the CIL example nspk.cil separately and use the jar file as your classpath, as in
The connector classes are cil2pbundle, Pbundle, and Pstrand. There are supporting classes that are also used in other parts of the translator, namely LabelNode, treeparse, and a few other classes generated by JavaCC. The class treeparse is used to parse the .cil file and it comes from a treeparse.jj grammar. Source code for these classes is available on request.