How does the CLP model checker work?
Protocol rules are specified using MSR with constraints.
Constraints are used for freshness and time-stamps, for distinguishing
honest principals from
Trudy (id=0).
Initial states are defined via the special rule
init --> ...
Goals are specified via "minimal violations".
The CLP program computes all symbolic configurations reachable from
"init".
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
The initial configuration is define via the special rule:
init ---> M : C
where M is a multiset and C a constraint.
In CLP the rules are written using the predicate "rule",
e.g.,
rule([init],[time(T),fresh(K),init(1),init(1),resp(2),resp(2),valid(D)],{K>=0,T>=0,D>0},init).
Properties/Goals
You can express a set of "mininal violations" to a given "safety property"
as "constrained configurations" e.g.
goal([init(A,tuple(B,K,Sent)),resp(B,tuple(A,K,Rec))],
{Rec-Sent>2},goal).
Running the analysis
Download the CLP source code "forwardmsr_pl" and the code of the
examples.
Save them using ".pl" extension.
Call sicstus prolog.
Load secmsr (if you saved it as "secmsr_pl")
:-[forwardmsr].
Load the example (if you saved it as "falsifcwmf.pl")
:-[falsifcwmf].
Start the fixpoint computation using predicate "go".
:-g.
The CLP program will perform a forward exploration of the state space trying
to
find attacks.
If it returns "no", then ther considered "small model" has no attacks.
Execution Time
To measure execution time of any CLP operation you can use the predicate
ptime
For instance,
:-ptime(g).
will print out information about CPU time needed to reach a fixpoint.