How does the CLP model checker work?

Protocol rules are specified using MSR with constraints.
Constraints are used for freshness, for distinguishing honest principals from
Trudy (id=0).

Goals are specified via "minimal violations", i.e., their denotations are the "upward closure"
of the set of predicate that specify the violations.

The CLP program tries to "saturate" the set of all possible "preconditions" with respect to the given
the given violations.

If a fixpoint is reached we can serach for "potential initial states".
This gives us a way to "infer" preconditions on possible attacks.

If no "real" initial state is found (e.g. states in which Trudy has no initial knowledge
about keys and nonces), then the violations cannot be "reached".

This proves the protocol free from "attacks" wrt the property take into
consideration (under the assumption taken in the model)
for any number of principals, nonces, and parallel sessions.

• Protocol spec
• Initial states
• Goal spec
• Pre-image/termination test
• Running the prototype
• Authentication
• Measuring Execution time
  

More details:

Protocol specification
The protocol is specified using multiset rewriting rule annotated
with constraints
E.g. first NS rule:

 fresh(X) ---> fresh(Y) | step1(A,<Na,B>) | enc(B,<Na,A>)  : A>0,B>0,Y>NA,NA>X

where fresh (together with the constraints) is used to ensure freshness of names
In CLP  the rules are written  using the predicate "rule", e.g.,

rule([fresh(X)], [fresh(Y),step1(A,tuple(NA,B)),enc(B,tuple(NA,A))], {A>0,B>0,Y>NA,NA>X}, first).


Initial states
You can leave the definition of the initial states "open".
E.g. I only require that there cannot be agents in an intermediate steps or
pending messages in an initial state.

I use the predicate init(K,L) for this.
I use it only after the fixpoint is reached.

Properties/Goals
You can express a set of "mininal violations" to a given "safety property"
as "constrained configurations"
E.g. "Bob believes he exchanged a nonce with Alice, Trudy got the nonce"

 step4(B,tuple(NA,_,A)) | mem(NA) : B>0,A>0

They represent "all multisets (configurations) that include an instance of the minimal
violation" (upward-closure of the instances, i.e., if I add other informations/agents
the resulting configuration still represents a "violation".
In CLP unsfae states are written using the predicate "unsafe" (that takes a list as
parameter)
E.g.
unsafe([
  unsafe([step3(A,tuple(NA,_,B)),mem(NA)], {A>0,B>0}),
  unsafe([step3(A,tuple(_,NB,B)),mem(NB)],  {A>0,B>0}),
  unsafe([step4(B,tuple(NA,_,A)),mem(NA)], {A>0,B>0}),
  unsafe([step4(B,tuple(_,NB,A)),mem(NB)], {A>0,B>0})   
]).

denote the "union" of each set of violations denoted by every constrained configurations
expressed as "unsafe(Multiset,Constraint)


Pre-image
Preconditions  are computed "symbolically" via  a "pre-image" operator
that combines "unification" and "constraint solving"

Fixpoint termination test
Everything works modulo "constraint entailment" and "multiset subsumbption"

E.g. fresh(X) | step1(A,<Na,B>) : B>=0,Na<X   
                "subsumes"
     fresh(X) | step1(A,<Na,B>) | step2(B,<Na,Nb,A>) :  B>0,Nb<Na,Na<X

This allows us to reason symbolically about an "unbounded number of parallel sessions"

Running the analysis
Download the CLP source code "secmsr_pl" and the code of the examples.
Save them using ".pl" extension.
Call sicstus prolog.
Load secmsr (if you saved it as "secmsr_pl")

:-[secmsr].

Load the example (if you saved it as "ns.pl")

:-[ns].

Start the fixpoint computation using predicate "go".

:-go.

If it terminates you can inspect the resulting fixpoint using:

:- ls.
(list of all constrained configurations, each one of them has a order number)

E.g.

  f(5, [fresh(A),step1(pk(1),tuple(nonce(1),pk(2)))], {A<2.0}, 16, 14, intruderreceiveamsg_1).

must be read as:
    At the 5th fixpoint iteration the constrained configuration number 16
    defined as fresh(A) | step1(pk(1) | tuple(nonce(1),pk(2))) : A<2.0
    has been obtained as symbolic precondition of that numbered 14 via the rule called
    "intruderreceiveamsg_1"

:- trace(K,L).
(search for error traces, using the spec of initial states given in the example code)

Authentication
The CLP prototype can also be used for authentication  properties (as explained in the
technical report).
During the analysis the model checker builds a symbolic backward reachability graph
that can be studied after termination of the exploration.
Suppose that the invocation of the goal

:-go.

terminates.
By using the command

:-le.

It is posible to see the set of edges of the symbolic backward reachability graph.
The Sicstus graph library can be used then to visit the resulting graph.
For instance,

:-buildgraph(G).

Builds show the adjacent matrix G$ associate to the graph.

:-allpaths(I).

Shows all acyclic paths starting from node I.

:-selpaths(I,K).

Shows all paths starting from node I and not passing thorough a node K.

Execution Time
To measure execution time of any CLP operation you can use the predicate  ptime
For instance,

:-ptime(go).

will print out information about CPU time needed to reach a fixpoint.