Information Technology Reference
In-Depth Information
Inference System.
Agents are able to obtain new messages from the set of mes-
sages produced or received through an inference system. This system consists in
a set of inference schemata. An inference schema can be written as:
r
=
m
1
...
m
n
m
0
where
m
1
,...,m
n
is a set of premises (possibly empty) and
m
0
is the conclusion.
Consider a substitution
ρ
then let
mρ
be the message
m
where each variable
x
is
replaced with
ρ
(
x
). Given a sequence of closed messages
m
1
,...,m
n
, we say that
a closed message
m
can be inferred from
m
1
,...,m
n
through the application of
the schema
r
(written as
m
1
,...,m
n
r
m
) if there exists a substitution
ρ
s.t.
m
0
ρ
=
m
and
m
i
ρ
=
m
i
, for
i
∈{
1
,...,n}
. Given an inference system, we
can define an inference function
D
s.t. if
φ
is a finite set of closed messages,
D
R
(
φ
) is the set of closed messages that can be deduced starting from
φ
by applying only rules in
R
. In Table 1, we present the usual inference system
for modeling shared-key encryption within process algebras (e.g., see [5,14,15]).
Rule (
pair
) is used to construct
pairs
while Rules (
fst
) and (
snd
) are used to
split pairs; Rule (
enc
) is used to construct encryptions and Rule (
dec
) is used to
decrypt messages.
then
Table 1.
A simple inference system
(
x, y
)
x
(
x, y
)
y
xy
(
x, y
)
(
pair
)
(
fst
)
(
snd
)
xy
{x}
y
{x}
y
y
(
end
)
(
dec
)
x
2.2 Agents and Systems
We define the control part of our language for the description of cryptographic
protocols. Basically, we consider (compound) systems which consist of sequential
agents running in parallel. The terms of our language are generated by the
following grammar:
(Compound systems:)
S
::=
S \ L | S
1
| S
2
| A
φ
(Sequential agents:)
A
::=
0
[
m
1
...m
n
r
x
]
A
1
(Prefix constructs:)
p
::=
c
!
m | c
?
x
| p.A |
where
m, m
1
,...,m
n
are
closed
messages or variables,
x
is a variable,
C
is a
finite set of channels with
c ∈ C
,
φ
is a finite set of messages,
L
is a subset of
C
.
We briefly give the informal semantics of sequential agents and compound
system as well as some static constraints on the terms of the language.
-0
is the process that does nothing.
-
p.A
is the process that can perform an action according to the particular
prefix construct
p
and then behaves as
A
:
