Information Technology Reference
In-Depth Information
Table 2.
Symbolic operational semantics, where the symmetric rules for
|
1
, |
2
, \
1
are
omitted
(!
s
)
(?
s
)
(
c
!
m.A
)
φ
true
:
c
!
m
(
c
?
x.A
)
φ
true
:
c
?
x
−→
s
(
A
)
φ
−→
s
(
A
)
φ∪{x}
(
A
1
)
φ∪{x}
M
:
α
−→
s
(
A
1
)
φ
([
m
1
...m
n
r
x
]
A
1
)
φ
(
D
s
)
N
= constr(
r,
(
m
1
,...,m
n
)
,x
)
M,N
:
α
−→
s
(
A
1
)
φ
(
|
2s
)
S
M
:
c
!
m
S
1
N
:
c
?
x
S
M
:
α
S
S
1
(
\
1s
)
S
M
:
c
!
m
−→
s
S
S
−→
s
−→
s
−→
s
c∈ L
(
|
1s
)
M
:
α
−→
s
S
| S
1
S | S
1
M,N,x∈m
:
τ
S \ L
M
:
c
!
m
S
| S
1
S
\ L
S | S
1
−→
s
−→
s
x ∈
D
R
(
{t
1
,...,t
n
}
) to express that
x
can be deduced by applying the rules in
R
{t
1
,...,t
n
}
from the messages
. Such contraints on variables may be extended to
constraints on terms, i.e. we may require that
F
(
x
)
∈
D
R
(
{t
1
,...,t
n
}
)
,G
(
z
)
∈ y
and so on.
The lists of constraints on the set of possible substitutions, ranged over by
M,N,...
, may be defined as follow:
M
::=
C, M |
C
::=
false
| t ∈ t
| t ∈
D
R
(
|
true
{t
1
,...,t
n
}
)
where
t, t
,t
1
,...,t
n
are messages (possibly open). Lists of constraints are used
to represents (possibly infinite) sets of substitutions from variables to closed
messages. Let
Substs
be such set of substitutions. The semantics [[
M
]] of list of
constraints
M
is defined as follows:
[[
]]
.
=
Substs,
[[
C, M
]]
.
= [
C
]]
[[
true
]]
.
=
Substs,
[[
false
]]
.
=
∩
[[
M
]]
,
∅
[[
t ∈ t
]]
.
=
{σ | tσ ∈{t
σ}}
))]]
.
=
D
R
(
{σ | tσ ∈D
R
(
[[
t ∈
(
{t
1
,...,t
n
}
{t
1
σ,...,t
n
σ}
)
}
The symbolic semantics for Crypto-CCS is given in Table 2, where
S
M
:
α
−→
s
S
means that
S
may evolve through an action
α
in
S
when the constrains in
M
are satisfied. The function
constr
(
r,
(
m
1
,...,m
n
)
,x
), with
r
.
=
m
1
...m
n
m
0
,
defines the list of constraints imposed by the rule
r
and is defined as:
m
1
∈ m
1
,...,m
n
∈ m
n
,x∈ m
0
where
m
i
=
m
i
σ
and
σ
is a renaming of the variables in the terms
m
i
with
totally fresh ones (we omit here the technical details for the sake of clarity).
As a notation we also use
S
C,γ
→
s
S
if
γ
is a finite sequence of actions
α
i
,
1
≤
is a list of constraints s.t.
S
=
S
0
M
1
:
α
1
...
M
n
:
α
n
i ≤ n
and
C
=
M
1
,...,M
n
−→
s
−→
s
S
n
=
S
.
2.4 Symbolic Analysis
In order to develop a decidable verification theory, we need to compute when
a list of constraints is consistent or not, i.e. there exists a substitution
σ
which
