Information Technology Reference
In-Depth Information
For security analysis, the satisfiability of such a formula
F
is a decidable prob-
lem. (It turns out that the set of constraints is monotonic.) This give us a decid-
able procedure to symbolically check the security of finite systems with almost
generic inference systems.
The partial evaluation functions are given in the Tables 5 and 6.
Proposition 2.
Given a system
S
, a list of constraints
M
, an agent
X
φ
(with
φ
finite set of closed messages) and a logical formula
F
∈L
then:
=
M
F//
S,φ,M
.
For our purposes, it is also useful to consider the context ( )
S | X
φ
|
=
M
F
iff
X
φ
|
\ L
, which consists
only of the restriction. The partial evaluation function for such context w.r.t.
the formulas in
is given in Tab 6. The next proposition states its correctness.
Proposition 3.
Given a set of channels
L
and a logical formula
F
L
∈L
,we
have that:
(
S
)
\ L |
=
F
iff
S |
=
F//
\L
.
Table 5.
Partial evaluation function for
S | X
.
=
T
T
//
S,φ,M
T
A
=
X
and
ctc
(
nfc
(;
M, m ∈
D
R
(
φ
))) =
true
F
A
=
X
and
ctc
(
nfc
(;
M, m ∈
D
R
(
φ
))) =
false
T
A ∈ S, A
=
A
φ
.
=
K
A
//
S,φ,M
and
ctc
(
nfc
(;
M, m ∈
D
R
(
φ
))) =
true
F
A ∈ S, A
=
A
φ
and
ctc
(
nfc
(;
M, m ∈
D
R
(
φ
))) =
false
.
=
(
¬F
)
//
S,φ,M
¬
(
F//
S,φ,M
)
.
=
M
,m ∈
D
R
(
φ
):
c
!
m
(
F//
S,φ,
(
M,M
,m∈
D
R
(
φ
))
)
∨
(
M
:
c
!
mF
)
//
S,φ,M
S
F//
S
,φ,
(
M,M
,M
,m∈m
)
S
M
:
c
!
m
−→
s
∨
.
=
M
:
c
?
xF
)
//
S,φ,M
M
:
c
?
x
(
(
F//
S,φ∪{x},M,M
)
−→
s
S
F//
S
,φ,
(
M,M
,M
,x∈y
)
M
:
c
?
y
S
.
=
(
M
:
τ F
)
//
S,φ,M
S
M
:
c
?
x
(
F//
S
,φ∪{x},
(
M,M
,M
,x∈m
)
)
S
M
:
c
!
m
−→
s
∨
−→
s
S
M
,y ∈
D
R
(
φ
):
c
!
y
(
F//
S
,φ,
(
M,M
,M
,y∈
D
R
(
φ
)
,x∈y
)
)
S
M
:
c
?
x
∨
−→
s
S
F//
S
,φ,
(
M,M
,M
)
S
M
:
τ
.
=
∨
i∈I
F
i
//
S,φ,M
∨
i∈I
(
F
i
//
S,φ,M
)
Proposition 4.
Given a system
S
,a
φ
finite set of closed messages is decidable
whether there exists or not a term
X
φ
(with
Sort
(
S | X
)
⊆ L
) s.t.
=
i≤n
true
:
τ
i
K
X
(
S | X
φ
)
\ L |
Basically, by exploiting partial model checking we can reduce our verification
problem to a satisfiability one for a formula which consists only logical constants,
disjunction and possibility formulas, whose list of constraints are monotonic.
