Information Technology Reference
In-Depth Information
Table 3.
Normal form covering procedure
nfc
(
C
;)
.
=
{C}
nfc
(
C
;
true
,C
1
)
.
=
nfc
(
C
;
C
1
)
nfc
(
C
;
false
,C
1
)
.
=
{
false
}
nfc
(
C
;
t ∈ t, C
1
)
.
=
nfc
(
C
;
C
1
)
nfc
(
C, x ∈ t
,C
;
x ∈ t, C
1
)
.
=
nfc
(
C, x ∈ t
,C
;
t
∈ t, C
1
)
nfc
(
C, x ∈
D
G
(
T
)
,C
;
x ∈ t, C
1
)
.
=
nfc
(
C, C
;
x ∈ t, t ∈
D
G
(
T
)
,C
1
)
nfc
(
C
;
x ∈ t, C
1
)
.
=
nfc
(
C
[
t/x
]
,x ∈ t
;
C
1
[
t/x
])
nfc
(
C
;
t ∈ x, C
1
)
.
=
nfc
(
C
;
x ∈ t, C
1
)
nfc
(
C
;
F
(
t
1
,...,t
n
)
∈ F
(
t
1
,...,t
n
)
,C
1
)
.
=
nfc
(
C
;
t
1
∈ t
1
,...,t
n
∈ t
n
,C
1
)
nfc
(
C
;
F
(
t
1
,...,t
m
)
∈ G
(
t
1
,...,t
n
)
,C
1
)
.
=
{
false
}
nfc
(
C
;
t ∈
D
G
(
T
)
,C
1
)
.
=
t
∈T
nfc
(
C, t ∈ t
i
)
∪
∪
C
∈G
-steps (T,t)
nfc
(
C, C
)
.
=
nfc
(
C, C
;
x ∈
D
G
(
T
∩ T
)
,C
1
)
nfc
(
C, x ∈
D
G
(
T
)
,C
;
x ∈
D
G
(
T
)
,C
1
)
.
=
nfc
(
C, x ∈ t
,C
;
t
∈
D
G
(
T
)
,C
1
)
nfc
(
C, x ∈ t
,C
;
x ∈
D
G
(
T
)
,C
1
)
.
=
(
C
2
)
∈S
-steps
(
T,t,app
)
nfc
(
C
;
C
2
,C
1
)
∪nfc
((
C
;
t ∈
D
G
(
T
)))
nfc
(
C
;
t ∈
D
R,app
(
T
)
,C
1
)
where:
G
-steps(
T,t
)=
{constr
(
r,
D
G
(
T
)
,v
)
,v ∈ t | r ∈ G
-rules
}
S
-steps(
T, t, app
)=
{
(
C
,t ∈
D
R,app∪{
(
r,t
)
}
(
T ∪{v}
))
|
r ∈ S
-rules
,t
∈ T,
(
r, t
)
∈ app, r
=
m
1
...m
p
...m
k
m
0
,
C
=
v ∈ m
0
,m
p
∈ t
,m
i
∈
D
G
(
T
)
}
3 Symbolic Hennessy-Milner Logic: A Logical Language
for the Description of Protocol Properties
We illustrate the logical language SHML, namely
Symbolic Hennessy-Milner
Logic
for the specification of the functional and security properties of a compound
system. We accommodate the common Hennessy-Milner Logic, i.e. a normal
multimodal logic (e.g., see [16]), with atomic propositions which make it possible
to specify whether a message may be deduced by a certain agent in the system.
Moreover, since here we have a symbolic semantics rather than a concrete one,
we need also to embody the constraints about the action relations. The syntax
of the logical language SHML is defined by the following grammar:
| K
X
|¬F |M
:
αF |∨
i∈I
F
i
F
::=
T
where
M
:
α ∈ Act
S
,
m
is a
closed
message,
X
is an agent identifier
2
and
I
is
an index set.
2
We note that a single identifier can be assigned to every sequential agent in a com-
pound system (e.g., the path from the root to the sequential agent term in the
parsing tree of the compound system term).
