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.txt (rename to csolve.pl) 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, called CoProVe. It checks for solvability of a constraint set incrementally as node sequences are constructed. See the CoProVe site and the code directory. A modified version of their code is included here as coprove_pl.txt (rename to coprove.pl). The modifications allow it to use the same specifications and the same search commards as csolve. However, this version does not produce the diagram output.|
|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:
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.
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.) The nonce status is reflected in the construction of test bundles as described below.
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 reception containing the variables A, B:
The B-role strand appears in Prolog as:
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:
In the NSPK example, the nonces Na and Nb should be confidential. Testing for compromise involves defining a new 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.
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 Unix-like predicates pwd(dir) and cd(dir)
for checking and changing the current directory.
At the Prolog prompt, load the solver and protocol files like this:
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:
In this example, we get some search trial output, followed by the diagram shown earlier and the text of the solution:
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
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
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.