Information Technology Reference
In-Depth Information
4 Verification of Security Protocols
through Partial Model Checking
We are mainly interested in the study of security properties like:
Is there an agent (intruder) that, communicating with the agents of the
system
S
, can retrieve a secret that should only be shared by some agents
of
S
?
Formally, this can be restated as follows:
C,γ
→
S
| X
φ
and
S
| X
φ
|
=
K
X
∃X
φ
s
.
t
.
S| X
φ
(2)
where
m
is the message which should remain secret
3
. However, we are not inter-
ested in every computation
C, γ
of
S | X
. Indeed, consider the following example
where the system
S
consists of the single agent
0
{m}
, whose unique secret is
m
.
Then, due to our semantic modeling of receiving actions (see rule (?) in Tab. 2),
it is possible for an intruder to obtain any secret messages. For instance, let
X
be
c
?
x.
0
, then:
0
{m}
| X
∅
true
:
c
?
x
0
{x}
Thus, since the constraint
m ∈
D
R
(
x
) is consistent, then there may be an in-
stance of
X
that discovers
m
after performing the receiving action
c
?
x
. This
means that
S
satisfies property (2), i.e. it is not secure, which contradicts our
intuition. However, note that the receiving action
c
?
x
simply models the po-
tential communication capability of
X
(and thus of the system
S | X
) with an
external (omniscient) environment. But, when we fix
X
φ
, we want to consider
S | X
φ
as a
closed
system and study only its internal communications, i.e. the
actual communications between the system
S
and its “hostile” environment rep-
resented by
X
. We thus consider a formulation where the context of evaluation
becomes (
S | X
)
−→
0
{m}
|
\ L
and
L
is the set of channels where
S
and
X
can communi-
cate, i.e.
Sort
(
S | X
). Note that all the possible computations of (
S | X
φ
)
\ L
are
actually the internal computations of
S | X
.
Since,
S
is finite, we can simply inspect each possible symbolic computation of
(
S | X
), which are in a finite number for whatever sequential agent
X
. Moreover,
we may find an integer, say
n
, s.t. the length of such computations is bounded
by
n
for whatever
X
. Thus, we can simply check whether there is an intruder
s.t.:
=
i≤n
true
:
τ
i
K
X
(
S | X
)
\ L |
Let
F
be the formula
i≤n
true
:
τ
i
K
X
. We simply apply a partial model
checking function (see below) and obtain a formula
F
s.t.
=
F
3
However, also several authentication properties can be checked only by inspecting
the intruder's knowledge, e.g., see [6,7].
(
S | X
)
\ L |
=
F
iff
X |
