JAIST Repository
https://dspace.jaist.ac.jp/

Title

On‑the‑fly Model Checking Security Protocols and
Its Implementation by Maude

Author(s)Li, Guoqiang; Ogawa, Mizuhito

CitationIssue Date

2006‑11‑29

Type

Presentation

Text version

publisher

URL

http://hdl.handle.net/10119/8307

RightsDescription

Theorem Proving and Provers Meeting(2nd TPP)での発表資料, 開催：2006年11月29日〜30日, 開催場所
：JAIST 情報科学研究科棟II・Collaboration Room 7(5F)

Japan Advanced Institute of Science and Technology

On-the-fly Model Checking Security Protocols
and Its Implementation by Maude
Guoqiang Li, Mizuhito Ogawa
Japan Advanced Institute of Science and Technology

Nov. 29, 2006

Problems• When model checking security protocols, it suffers frominfinite states. Such infinity comes from:• Infinitely many sessions of protocols: each principal can

initiate or act as a responser infinitely many protocol
sessions.
• Infinitely many principals in the network: each principal may
communicate with infinitely many other principals.
• Infinitely many messages that intruders can generate: each
intruder can produce infinitely many messages based onmessages leaked in the network(Dolev-Yao).

Our approaches• A typed process calculus that avoids recursive operations

is proposed, so that only finitely many sessions are
considered.
• A bound variable is introduced to represent a sender’sintended destination, so that the unbounded number ofprincipals are finitely described.
• (νx : I)a1{M}k[A,x]• Messages with the same effect in a protocol are unified toa parametric message based on type information.
• a1(x).a2x• Each possible run of a protocol is represented as a trace.

Model a network• Principals exchange the messages

with the environment.
• A message that a receiver receives

may not be the same as what asender sends.

A
B• Environment can produce, modify

messages during thecommunication of principals(represented as a deductive
system).

C

Environment

Syntax

M, N, L ::=n | x | (M, N) | {M}L | m[M1 , . . . , Mn ]P, Q, R ::=0aM.Pa(x).P[M = N] P(νx : A)P
let (x, y) = M in P
case M of {x}L in P
PkQ

Nil
output
input
match
range
pair splitting
decryption
composition

An approximation on sending a message(Usages of ranges and binders)• Ranges and binders are used when aprincipal initiates a protocol, or one can
not obtain his communicator’s name.
• (νx : I)a1{A, NA }+k[x] . . . z . . . a3{z}+k[x]• (νx : I)a1{A, NA }+k[x] . . . yb , z . . . [yb =x] . . . a3{z}+k[yb ]NSPK protocol
A −→ B :{A, NA }+KB

B −→ A :{NA , NB }+KA

A −→ B :{NB }+KB

Fixed NSPK protocol• An approximation is used that the principal

A −→ B :{A, NA }+KB

sends the same message randomly todifferent principals.

B −→ A :{B, NA , NB }+KA

A −→ B :{NB }+KB

Representation of Abadi-Gordon protocol(An example of the binder)
A −→ S :S −→ B :A −→ B :A, {B, KAB }KAS
{A, KAB }KSB
A, {A, M}KAB

A ,(νx : I)a1(A, {x, k[A, x]}k[A,S] ).a2(A, {A, M}k[A,x] ).0
B ,b1(x).case x of {x 0 }k[B,S] in let (y , z) = x 0 in
b2(w).let (w 0 , w 00 ) = w in [w 0 = y ] case w 00 of {u}z inlet (u 0 , u 00 ) = u in [u 0 = y] acc w.0
S ,s1(x).let (y , z) = x in case z of {u}k[y,S] in let (u 0 , u 00 ) = u ins2{y , u 00 }k[u0 ,S] .0
SYS ,AkSkB

Representation of Woo-Lam protocol(An example of the Decryption)
A −→ B :B −→ A :A −→ B :B −→ S :S −→ B :ANB{NB }KAS
B, {A, {NB }KAS }KBS{A, NB }KBS

A ,a1 A.a2(xa ).a3 {xa }k[A,S] .0
B ,b1(xb ). b2 NB .b3(yb ).b4 (B, {xb , yb }k[B,S] ).b5(zb ).
case zb of {ub }k[B,S] in let(wb , tb ) = ub in [wb = xb ][ub = NB ] acc yb .0
S ,s1(xs ).let (xs0 , xs00 ) = xs in case xs00 of {ys }k[xs0 ,S] in let (zs , ws ) = ys
in case ws of {us }k[zs ,S] in s2 {zs , us }k[xs0 ,S] .0
SYS ,AkSkB

Representing each possible run as a trace

A −→ S :S −→ B :A −→ B :A, {B, KAB }KAS
{A, KAB }KSB
A, {A, M}KAB

A −→ B :B −→ A :A −→ B :B −→ S :S −→ B :ANB{NB }KAS
B, {A, {NB }KAS }KBS{A, NB }KBS

• a1(A, {B, k[A, B]}k[A,S] )• a1(A, {I, k[A, I]}k[A,S] )• a1A.b1(A).b2NB• a1(A, {B, k[A, B]}k[A,S] ).
s1(A, {B, k[A, B]}k[A,S] )• b1(A).b2NB .a1A.a2(NI )• a1(A, {B, k[A, B]}k[A,S] ).
b1({A, k[A, B]}k[B,S] )×• b1(A).b2NB .b3(NB ).
b4(B, {A, NB }k[B,S] ).b5(B, {A, NB }k[B,S] )Environment ability• If two messages are leaked the environment:(A, {B, M}k[A,S] ), (k[A, S], {B, M}k[B,S] )• The environment can split and decrypt the message:

A, {B, M}k[A,S] , k[A, S], {B, M}k[B,S] , M . . .
• The environment can compose and encrypt the message:{A}k[A,S] , (A, M), {{B, M}k[B,S] }k[A,S] . . .
• The environment knows some common messages:

A, +k[A], . . .
• The environment can produce new messages:

I, NI , . . .
• The environment can produce infinite many messages!

(S B M)

Formal definition of traces• Action α is a term of aM or a(M). An action is ground if theattached message does not have any variables.
• eg: b1 x, a1(A, {B, KAB }KAS )• Trace s is a string of ground actions such that for each s 0 ,s00 and a(M), if s = s0 .a(M).s”, then msg(s0 ) B M.
•√

b1(A).b2NB .a1A.a2{I}k[I,S]• × a1(A, {B, k[A, B]}k[A,S] ).b1({A, k[A, B]}k[B,S] )• Configuration is a pair hs, Pi,in which s is a trace and P isa closed process (All variables are bound).

Type• A type system is proposed such that the type of eachvariable, message and process can be inferred• {B, k[A, B]}k[A,S] : (i ∗ k [i ∗ i])• b1(x).let (y, z) = x in [z = A].0 : α ∗ i → unit
• x : α ∗ i; y : α; z : i• A principal will be stuck if it receives a message whosetype can not unify the type of the input variable• b1({B, k[A, B]}k[A,S] ).let (y, z) = {B, k[A, B]}k[A,S] in [z = A].0

• A variable (or a subexpression) with type variable as its

type can be unified to any type, so that it can besubstituted to any message

Reasons that cause the system to be infinite
Operational semantics(INPUT ) hs, a(x).P : τ1 → τ2 i −→ hs.a(M), P{M/x}is B M, Γ ` M : τ1
(OUTPUT ) hs, aM.Pi −→ hs.aM, Pi(RANGE) hs, (νx : A)Pi −→ hs, P{m/x}i m ∈ A
, a1M.a(x).0, (νx : I)a1{M }+k[x] .0a1M, a(x).0a1{M }+k[B] , 0 · · · a1{M }+k[C] , 0 · · · a1{M }+k[I] , 0
a1M.a(M ), 0 · · · a1M.a((M, M )), 0 · · · a1M.a({M }+k[I] ), 0

Approach of parametric model• Each sub-expression with a type variable as its type will bemarked with a parametric variable that will not be further
instantiated.
• Any message that instantiates the sub-expression will takethe same effect to the protocol.
, a1M.a(x).0, a1M.a(x̂).0a1M, a(x).0a1M, a(x̂).0a1M.a(M ), 0 · · · a1M.a((M, M )), 0 · · · a1M.a({M }+k[I] ), 0a1M.a(x̂), 0

Approach of parametric model (cont.)• A binder will not be instantiated instantly, it will be

instantiated “when needed”(We will explain the “need”
later), (νx : I)a1{M }+k[x] .0a1{M }+k[B] , 0 · · · a1{M }+k[C] , 0 · · · a1{M }+k[I] , 0, (νx : I)a1{M }+k[x̂i ] .0a1{M }+k[x̂i ] , 0

(PINPUT ) hŝ, a(M̂).P̂i −→p hŝ.a(M̂), P̂i(POUTPUT ) hŝ, aM̂.P̂i −→p hŝ.aM̂, P̂i(PRANGLE) hŝ, (ν x̂ : A)P̂i −→p hŝ, P̂i

Parametric process and trace• In a parametric system, parametric traces will be used torepresent each possible run of a protocol.
• Each trace in an original system has an abstraction trace inits parametric system.
• A parametric trace may have infinitely many instantiatedtraces in its original system (named concretizations).
• It may have no concretizations!
• a1(A, {B, k[A, B]}k[A,S] ).b1({A, x̂}k[B,S] )Unchangeable messages• An unchangeable message (UM) is an encrypted input

message such that its key is not leaked in the environment.
• A parametric variable in an unchangeable message cannot
be instantiated to arbitrary ground messages. So we must
explicitly instantiate it (by unification).
• If a unification is failed, the parametric trace has noconcretizations.
A −→ B : {A, M}k[A,B]
a1{A, M }k[A,B]

a1{A, M }k[A,B]

b1{A, x̂}k[A,B]×
a1{A, M }k[A,B] .b1{A, x̂}k[A,B]

a1{A, M }k[A,B] .b1{A, M }k[A,B]
a1{A, M }k[A,B] .b1{A, M }k[A,B]×

Explicit trace• An explicit trace is a parametric trace that each UM can be

deduced by its prefix parametric trace.
• An explicit trace can be obtained by gradually unifying

each UM with messages in its prefix parametric trace.
a1{A, B, M }k[A,S] .s1{x̂, ŷ, ẑ}k[x̂,S] .s2({x̂, ŷ, ẑ}k[ŷ,Ŝ] ).b1({A, B, ŵ}k[B,S] )a1{A, B, M }k[A,S] .s1{A, B, ẑ}k[A,S] .s2({A, B, ẑ}k[B,Ŝ] ).b1({A, B, ẑ}k[B,S] )a1{A, B, M }k[A,S] .s1{A, B, M }k[A,S] .s2({A, B, M }k[B,Ŝ] ).b1({A, B, M }k[B,S] )• The number of explicit trace of one parametric trace isfinite. Each explicit trace represents a possible run of the
protocol.

Deducing to an explicit trace(Woo-Lam)(More than one unifications)b1(A).b2 NB .b3(ŷb ).b4 (B, {A, ŷb }k[B,S] ).s1(x̂s , {ŷs , {ẑs }k[ŷs ,S] }k[x̂s ,S] ).
s2 {x̂s , ẑs }k[ŷs ,S] .b5({A, NB }k[B,S] ),→b1(A).b2 NB .b3(NB ).b4 (B, {A, NB }k[B,S] ).s1(x̂s , {ŷs , {ẑs }k[ŷs ,S] }k[x̂s ,S] ).
s2 {x̂s , ẑs }k[ŷs ,S] .b5({A, NB }k[B,S]
b1(A).b2 NB .b3(ŷb ).b4 (B, {A, ŷb }k[B,S] ).s1(x̂s , {ŷs , {ẑs }k[ŷs ,S] }k[x̂s ,S] ).
s2 {x̂s , ẑs }k[ŷs ,S] .b5({A, NB }k[B,S] ),→b1(A).b2 NB .b3(ŷb ).b4 (B, {A, ŷb }k[B,S] ).s1(A, {B, {NB }k[B,S] }k[A,S] ).
s2 {A, NB }k[B,S] .b5({A, NB }k[B,S] ),→×

Authentication properties• Intuitively, principal A isauthenticated to B means if B
“thinks” he accepts a message
from A, then it really comes fromA.

A −→ B :A

B −→ A :NB

A −→ B :{NB }KAS

B −→ S :B, {A, {NB }KAS }KBSS −→ B :{A, NB }K

BS• In the original model, it is definedas: if acc occurs in a trace, thenA ,a1 A.a2(xa ).a3 {xa }k[A,S] .0
a3 must occurs in the trace
before acc, and both of them are B ,b1(xb ). b2 NB .b3(yb ).b4 (B, {xb , yb }k[B,S] ).
attached with the same message.
b5(zb ).case zb of {ub }k[B,S] in(h, Sysi |= a3x ←- accx)
let(w , t ) = u in [w = x ][u = N ]b• The definition is equivalent to thesame definition defined in explicit
traces.

acc yb .0

b

b

b

b

b

B

On-the-fly model checking by Maude• Two reasons to use Maude:• A new parametric trace generation is decided on-the-fly bytrying to unify UM(it may fail)• It is easily to transfer a specification property to areachability problem.
• The way of implementation by Maude• Each elementary definition and function in the parametricmodel is implemented to functional modules.
• A trace generating system is represented in a systemmodule.
• search command is used to find whether the negation of a
specification is reachable.

Trace generating system• A state of the trace generating system is a 3-tuple:

htr , S, k i, where• tr is a parametric trace.
• S is a list of substitutions.
• k is a type of tr , where k ∈ {ot, et, pt}. ot represents an

original trace, et represents an explicit trace and pt
represents a pending trace.
A −→ B : {A, M }k[A,B], N il, ota1{A, M }k[A,B] , N il, ota1{A, M }k[A,B] , N il, et

a1{A, M }k[A,B] .b1{A, x̂}k[A,B] , N il, ota1{A, M }k[A,B] .b1{A, x̂}k[A,B] , {x̂ → M }, pta1{A, M }k[A,B] .b1{A, M }k[A,B] , N il, etb1{A, x̂}k[A,B] , N il, otb1{A, x̂}k[A,B] , N il, pt

, N il, etTransition rules of Woo-Lam protocol• Initial state: h, {}, oti• Parametric transition relation:• htr , S, oti ,→ htr .a1A, S, oti if a1 6∈ tr• htr , S, oti ,→ htr .b1(x̂), S, oti if b1 6∈ tr
A −→ B :• ...
B −→ A :• Reduction relation:
A −→ B :• htr , θ#S, pti ,→ htr θ, ES(tr θ), pti
B −→ S :if not Exp(tr θ)S −→ B :• htr , θ#S, pti ,→ htr , S, pti• Trace type transferred relation:• htr , S, oti ,→ htr , ES(tr ), pti if not Exp(tr )• htr , S, oti ,→ htr , {}, eti if Exp(tr )• htr , θ#S, pti ,→ htr θ, {}, eti if Exp(tr θ)ANB{NB }KAS
B, {A, {NB }KAS }KBS{A, NB }KBSPart source code of Woo-Lam protocol

Experimental results
protocols
NSPK protocol
fixed NSPK protocol
Woo-Lam protocol*
Yahalom protocol
Otway-Ree protocol
Woo-lam protocol

sessions
1
1
1
2
2
2

lines
20+33020+33025+33036+33034+33042+330states
46
164
168
536
2,164
105,423

times(ms)
130
637
160
1,039
22,316
476,507flaws
detected
securedetecteddetecteddetecteddetected

The tests were preformed on a Pentium 1.4 GHz, 1.5G Memory, Win XP.
A benchmark of analyzing security protocol (by horn logic)
protocols
times(ms)
NSPK protocol
8
fixed NSPK protocol
5
Woo-Lam protocol*
6
Yahalom protocol
16
Otway-Ree protocol
14
Woo-lam protocol
failsRelated work
(Benchmark)• Based on Horn clauses and resolution, checking the properties
in infinite sessions of the protocol.
• att({m}k ) ∧ att(k ) → att(m)• att(nb) → att({nb}kas ) (Woo-Lam protocol)• It sometimes does not terminate. (NSPK, Woo-Lam)• A tag system makes system terminating. Security of a tagged
protocol does not imply security of its untagged version.
• Related references are:• Bruno Blanchet. An Efficient Cryptographic Protocol Verifier Based on
Logic Programming. CSFW-14, 2001

• Bruno Blanchet and Andreas Podelski. Verification of Cryptographic
Protocols: Tagging Enforces Termination. Theoretical Computer
Science 333, 2005

Related work
(OFMC, Lazy intruder)• David Basin, et al. proposed an On-the-flymodel checking methods (OFMC).
• They use a high-level language HLPSL torepresent a protocol, then translate
automatically to a low-level one, IF.
• An intruder’s messages are instantiatedwhen necessary (UM is similar).
• An intruder’s role is explicitly assigned,thus flexible and efficient (we need tocheck each role).

... ...
Messages
1. A -> B : A, NA
2. B -> S: B, {|A, NA, NB|}k(B,S)
3. ... ...
Session_instances[A:a; B:b; S:s]
[A:i; B:b; S:s]... ...
state(roleA,step0,sess1,a,b,s,k(a,s)).
state(roleB,step0,sess1,a,b,s,k(b,s)).
state(roleS,step0,sess1,a,b,s,k).
state(roleA,step0,sess2,a,b,s,k(a,s)).
state(roleS,step0,sess2,a,b,s,k).
i_knows(a).i_knows(b).i_knows(s).
i_knows(s).i_knows(i).i_knows(k(i,s)).

Related works(Process calculus)• Gavin Lowe firstly uses trace analysis on CSP. The intruder

is represented as a recursive process. states are restrictedby imposing upper-bounds.
• Abadi et al. use some bisimulation to define the security
properties. The main problem is that those equivalences
are usually undecidable for implementation.
• Sysimp ∼= Sysspec• Their another approach is statical analysis by type system.

The attacker model is weaker than Dolev-Yao model,
assuming that the intruder is partially trusted.

Related work
(Type system vs. tag system)• J. Heather et al. show that a tagging

A −→ B :A

system can prevent type flaw attacks.
• A tag is a few bits attached to eachmessage, with different bit patterns
allocated to different types

B −→ A :NB

A −→ B :{NB }KAS

B −→ S :B, {A, {NB }KAS }KBSS −→ B :{A, NB }KBS• (nonce, N) means N is intended to be anonce.

I(A) −→ B :AB −→ I(A) :NB

messages can be bounded in the search I(A) −→ B :for an attack when the principals are
B −→ I(S) :bounded.
I(S) −→ B :NB• The work infers that the depth of ground

B, {A, NB }KBS{A, NB }KBS((agent, {agent, {nonce}sk}sk),((agent, B), ({agent, {nonce}sk}sk, {(agent, A), {(nonce, NB )}KAS }KBS )))Related work
(Binder vs. Principals Restriction)• The research of H. Comon-Lundh et

al. is based on the Horn clauses,
which proved that it is sufficient toonly consider a bound number ofprincipals when verifying somesecurity properties.
• Given an attack using n agents, we

project every honest identity on one
single identity and every dishonest
identity on one dishonest identity.

• A→B:A, Na(Yahalom protocol)• Fresh(t, s), T (t) ⇒T ([st(a, 0, ha, b, srv i), s].t)
s: session, t: trace• T(t),
In([st(a, 0, ha, b, srv i), s], t),
NotPlayed(a, 1, s, t) ⇒T ([ha, n1 (a, s)i, s].
[st(a, 1, ha, b, srv i), s].t)• Solution: Keep a uninstantiated.

Future work

• Develop a parser that transfers an original system to its

counterpart Maude source code.
• Try to perform model checking on other security properties

such as non-repudiation, fairness, anonymity, etc.
• Extend the calculus to one that can define recursive

process so that we can model checking a protocol with
infinite sessions.

Thank you!