=====================================================
	 CoProVe: CONSTRAINT-BASED SECURITY PROTOCOL VERIFIER
			  QUICK START GUIDE
	=====================================================

In this directory, you find the files
 
- Source code of CoProVe to be used in combination with either XSB or Eclipse
coprove_v12.p 

- Needham Shroeder specification (nspksec.p)

1. PROTOCOL VERIFICATION ROADMAP

The steps are:

1 Pick a protocol and identify different roles
2 Specify protocol roles templates
3 Prepare a session scenario
4 Add a security check to the session
5 Verify it
6 If attack, (try to) patch the protocol and go back to 1
7 If no attack, go back to 3 

GENERAL NOTATION

In general, the notation is the same of prolog:

Variables: They begin with uppercase or with the underscore _:
Na,Nb,A,B, _a are variables a,na,nb,b are non-variable terms.

Complex Terms. can be built using predicate (function) symbols: pk(b)
is a non-variable term (pk is a function symbol). 

Operators. Some predicate symbols (e.g. +, *) are declared as
operators. This helps writing things. E.g., pk(B) Nb*pk(B) is the same
as *(Nb,pk(B)): * is an infix-operator.  send(Nb*pk(B))

PROTOCOL NOTATION

[t1,t2,t3]: this is the message obtained by concatenaring t1,t2 and
t3.[a,b,c,d,e,S] is a list in Prolog So, if a message contrains three
subparts a,b,c, you write it as [a,b,c]

msg*k: asymmetric encryption

msg+k: symmetric encryption

pk(A): public key of Agent A

sk(A): secret key of Agent A

2. SPECIFYING A PROTOCOL

Consider the usual Needham-Shroeder:

  A->B : [A,Na]*pk(B)
  B->A : [Na,Nb]*pk(A)
  A->B : [Nb]*pk(B)

Here we follow the convention that 
Na, Nb: are nonces
A, B: are Agents (Alice and Bob)
Here we have 2 ROLES:

- one initiator (A)
- and one responder (B)

Other possible roles which may be present in other protocol
specification are e.g.: Server, etc

The crucial element in the specification of a role is the
specification of the list of ACTIONS it carries out. There are two
kind of actions (here t is a message):

- send(t)
- recv(t)

the crucial part of the specification of a role, is the specification
of the sequence of events it performs. This is simply the prolog list
of actions, in which agent names, nonces and keys are replaced by
variables. In the case of the initiator of the Needham-Schroeder, this
list is.

[send([A,Na]*pk(B)), recv([Na,Nb]*pk(A)),send(Nb*pk(B))]

The reason why all names, nonces and keys are filed out by variales is
that that roles are parametric. The actual instance of a role is
defined in the scenario (see below).

2.1 ADDING THE ORIGINATION ASSUMPTION. 

The protocol specification must obey to the "oririgination Assumption"
which in short states that 

	    Names should be received before they are sent

Consider again the initiator of NS:

       [send([A,Na]*pk(B)),recv([Na,Nb]*pk(A)),send(Nb*pk(B))]

here A and B are two role names that appear in a send before they
appear in a receive To solve the problem, add a recv in front of it.
The official specification becomes
	
 [recv([A,B]),send([A,Na]*pk(B)),recv([Na,Nb]*pk(A)),send(Nb*pk(B))]

2.2 ACTUALLY SPECIFYING THE ROLES. 

The specification of the roles, together with the specification of the
scenario (see below) should go in a separate prolog file, which you
can call e.g. protocol.p

A role is specified by adding a clause to this file of the form

name(Variables, [ListActions]).

Where "name" is the the name of the role (you can invent it)

In our case:

initiator(A,B,Na,Nb,[recv(A,B),
	send([A,Na]*pk(B)),
	recv([Na,Nb]*pk(A)),
	send(Nb*pk(B))]).

Now we need to add the specification of the responder. Basically this
is obtained by switching the send and receive actions of the initiator
(one has to check again whether the origination assumption is
satisfied and if so, to add a recv role to fix this. In our example, this is:

responder(A,B,Na,Nb, [ recv([A,Na]*pk(B)),
		     send([Na,Nb]*pk(A)),
		     recv(Nb*pk(B))]).

Notice that this specification satisfies the origination assumption
without any additional role, so it is left as it is.

3. SPECIFYING THE SCENARIO

Protocol roles provide "template" specifying the agent's standard
behaviour. Now we need to specify:

- how many agents are present in the scenario (how many initiators,
how many responders)

- the name of each agent in the scenario (there could be two
initiators, we have to give them two different names to distinguish
them).

- what does each agent knows (which of the variables in the role
specification should be instantiated to.

- introduce fresh nonce (e.g., make sure that nonces are fresh). 

3.1 THE ABSTRACT SCENARIO

Let us first talk about abstract scenario notation, later we'll see
how to ipement them. For instance, for the NS protocol, a possible
scenario (abstract notation) is

     [initiator(alice,B,na,Nb,List1), responder(A,bob,Na,nb,List2)]

Here there is one initiator played by agent alice and one responder
played by agent bob. While doing this we have specified that the
initiator knows only its own name and the nonce na (the rest is left
as variable), while the responder knows its ownn name and the nonce nb
(the rest is left as variables).

Variables indicate parameters that may assume any value (their value
is not known by the agent at the start).  For instance, the initiator
here does not know in advance the name of the responder.

Fresh nonces are modeled by new terms (ground terms that don't occur
elsewhere in the scenario specification).

List1 and List2 must be distinct variables.

The one name you must never use is "e", (together with pk(e) and
sk(e)), which is the name of the intruder, and never changes.

Other possible abstract scenarios are 

- [initiator(a,B,na,Nb,List1), responder(a,b,Na,nb,List2)]

  In this scenario the responder knows alredy the name of the
  initiator. Such a scenario is useful to remove the traces in which
  the intruder (who is always called "e") talks directly to the
  responder. This is the most efficient scenario which still allows to
  find the secrecy and authentication flows. Try it and see what
  happens.

- [initiator(a,b,na,nb,List1), responder(a,b,na,nb,List2)]

  In this scenario the responder knows alredy the name and the nonce
  of the initiator, and vice-versa. This is not only unrealistic, but
  it would not allow to find any attack.

- [initiator(a,b,na,nb), responder(c,d,nc,nd)] Here there is no
communication possible, no communication!

3.2 THE CONCRETE SCENARIO

The concrete scenario is specified by defining the predicate scenario
with a clause as follows:

scenario([
           [name_1,Var_1],
           ...,
           [name_n,Var_n]
           ]
          ) :-
   role_1(...,Var_1),
   ...
   role_n(...,Var_n).
 
where the part role_1(...), ..., role_n(...) is equal to the abstract
scenario described above; name_1,...,name_n are non-variable terms
indicating the names of the participating agents, and Var_1,...,Var_n
are variable linking the list of names to the roles. For instance.

scenario([
           [alice,Init1],
           [bob,Resp1],
           [sec,Secr1] %SEE LATER
           ]
          ) :-

   initiator(a,B,na,Nb,Init1),
   responder(a,b,Na,nb,Resp1),
   secrecy(nb, Secr1).

After the scenario, one has to specify the names of the agents which
are required to finish their run. This is done by defining the
predicate has_to_finish as follows.

has_to_finish([listofnames]).

In our example, this is

has_to_finish([sec]).

If no agent is required to finish, then the argument is the empty
list:

has_to_finish([]).

3.2 THE INTRUDER KNOWLEDGE

At last we have to set up the initial intruder knowledge, which is
done by adding to the program the clause

initial_intruder_knowledge([LIST OF TOKENS THE INTRUDER KNOWS]). 

Typically, the intruder knows the agent names, in our example.

initial_intruder_knowledge([a,b,e]).


4. ADDING THE SECURITY CHECK

To check if a given item remains secret, one has to:

a: add a standard secrecy role secrecy(X,[recv(X)]).  

b: add the role in the scenario as in the example above 

c: check if the agent playing the secrecy role (in the above case,
"sec") can finish its run (IF THIS IS THE CASE THEN THERE IS CERTAINLY
A SECRECY FLAW). This can be done rather easily by putting "sec" in
the list of agents which can finish their run.

For authentication flaws, the matter is more complex (see slides and
CE02).


			  RUNNING THE SYSTEM

To run CoProVe in your own system, you have to install XSB Prolog
(http://xsb.sourceforge.net). To use it in combination with Eclipse,
you have to slightly modify the code (how to do this is explained in
the code itself), and to change the suffixes of prolog programs, from
.p to .pl

To run CoProVe in your own system:

(1) Invoke xsb.
(2) Invoke CoProVe together with the protocol specification, with the command:

| ?- [coprove_v12,PROTOCOLTOBEVERIFIED].

For example, to verify the Needham-Shroeder public key protocol, whose
specification (together with the scenario etc), is written in the file
nspksec.p, you'll have to invoke.

| ?- [coprove_v12,nspksec]. 

Conventionally, any file to be loaded in XSB Prolog should have the
extension ".p". Once you are using the interpreter, to load a new
protocol definition you just have to type 

| ?- [PROTOCOLTOBEVERIFIED].

(3) Verify the protocol by invoking the either the command "checkone"
(which produces only one trace saatisfying the specification) or the
command "checkall" (which produces all traces matching the spec).
command: (Note: there are more than one scenarios with different
properties to check in rpc_concrete.P.  Choose one scenario only at a
time.)

So the two possibilities are 

| ?- checkone.

or

| ?- checkall.

(3) Analyze the output.

The output is a list of events, together with a State. When you invoke
"checkall" rather than "checkone" you can have more than one output,
e.g.:

| ?- checkall.
SOLUTION FOUND
State: [[a,[]],[b,[]],[sec,[]]]
Trace:
[a,recv([a,e])]
[a,send([a,na] * pk(e))]
[b,recv([a,na] * pk(b))]
[b,send([na,nb] * pk(a))]
[a,recv([na,nb] * pk(a))]
[a,send(nb * pk(e))]
[b,recv(nb * pk(b))]
[sec,recv(nb)]

SOLUTION FOUND
State: [[a,[]],[b,[]],[sec,[]]]
Trace:
[a,recv([a,e])]
[a,send([a,na] * pk(e))]
[b,recv([a,na] * pk(b))]
[b,send([na,nb] * pk(a))]
[a,recv([na,nb] * pk(a))]
[a,send(nb * pk(e))]
[sec,recv(nb)]
[b,recv(nb * pk(b))]

SOLUTION FOUND
State: [[a,[]],[b,[recv(nb * pk(b))]],[sec,[]]]
Trace:
[a,recv([a,e])]
[a,send([a,na] * pk(e))]
[b,recv([a,na] * pk(b))]
[b,send([na,nb] * pk(a))]
[a,recv([na,nb] * pk(a))]
[a,send(nb * pk(e))]
[sec,recv(nb)]


yes
| ?-

The meaning of the trace is rather straightforward. It consists of
elements of the form [agent,action]. For instance

[a,send([a,na] * pk(e))] indicates action of sending the message
[a,na] * pk(e) undertaken by agent a. The same applies to the receive
action.

The State, on the other hand, is basically what is left of the
semibundle and indicates which actions each agent did not manage to
carry out in the given trace, the syntax is a list of pairs of the
form [agent,listofactionsstilltobedone]. For instance the state
[[a,[]],[b,[]],[sec,[]]] indicates that all three agents involved
(a,b, and sec) have completed their run, as they have an empty list
next to them.

On the other hand, the state: [[a,[]],[b,[recv(nb * pk(b))]],[sec,[]]]
indicates that in the trace that this state referres to the agent b
did not manage to complete all actions. In particular, he could not
carry out the action recv(nb * pk(b)).

In both cases, the fact that the secrecy strand "sec" has finished its
run means that whatever was supposed to remain secret was actually
disclosed. 

References:

[CES05] R. Corin and S. Etalle and A. Saptawijaya: PS-LTL for
Constraint-based Security Protocol Analysis, Centre for Telematics and
Information Technology, Univ. of Twente, The Netherlands, Technical
report, nr. to appear, Jun. , 2005.

[CE02] Ricardo Corin, Sandro Etalle: An Improved Constraint-Based
System for the Verification of Security Protocols. SAS 2002: 326-341

[MS01] Jonathan K. Millen, Vitaly Shmatikov: Constraint solving for
bounded-process cryptographic protocol analysis. ACM Conference on
Computer and Communications Security 2001: 166-175