Information Technology Reference
In-Depth Information
r
I
are the standard rules describing the intruder in the style of Dolev-
Yao [13], whose capabilities consist in intercepting, analyzing, synthesizing and
constructing messages, with the ability to access permanent data. Formally:
r
I
1
:
Rules in ˜
π
(
x
)
→I
(
x
)
,π
(
x
)
r
I
2
:
·→∃n.I
(
n
)
r
I
3
:
I
(
x
)
→N
(
x
)
r
I
4
:
N
(
x
)
→I
(
x
)
r
I
5
:
I
(
x
1
,x
2
)
→I
(
x
1
)
,I
(
x
2
)
r
I
6
:
I
(
x
1
)
,I
(
x
2
)
→I
(
x
1
,x
2
)
r
I
7
:
I
(
{x}
k
)
,I
(
k
)
,
Kp
(
k, k
)
→I
(
x
)
,
Kp
(
k, k
)
r
I
8
:
I
(
x
)
,I
(
k
)
→I
(
{x}
k
)
r
I
9
:
I
(
x
)
→·
r
I
10
:
I
(
x
)
→I
(
x
)
,I
(
x
)
where
are variables.
In MSR
P
, a state is a multiset of the form ˜
x
and
k
=(
˜
˜
˜
s
A,
N,
I,
˜
π
), where the com-
ponents collect ground facts of the form
N
(
t
),
A
ρ
i
(
t
),
I
(
t
) and
π
(
t
), respectively.
˜
An
initial state
˜
s
0
=(˜
π,
I
0
) contains only persistent predicates (˜
π
) and initial
intruder knowledge (
˜
I
0
). A pair (˜
r
:˜
s
) consisting of an protocol theory ˜
r
and a
state ˜
s
is called a
configuration
. The initial configuration is (˜
r
:˜
s
0
). An example
specification is given in Appendix A.1.
3.2 Protocols as Processes
A security protocol may be described in a fragment of PA where: (a) every
communications happen through the net (here
P
net
is the process that manages
the net as a public channel where each
P
ρ
sends and receives messages); (b) there
is an intruder, with some initial knowledge able to intercept and forge messages
passing through the net (here
Q
!
I
, with initial knowledge
Q
I
0
); (c) each principal
starts a protocol interpreting a certain role
.
A security protocol, involving a collection of roles
ρ
ρ
, is expressed in PA
P
as
a
security protocol process
Q
, defined as the parallel composition of five com-
P
!
net
ρ
P
!
ρ
Q
!
I
Q
!
π
Q
I
0
where
P
ponents:
denotes the parallel
P
composition of all the processes in
. More precisely:
P
!
net
=!
N
i
(
0
.
describes the behavior of the network. It simply copies
messages from channel
x
)
.
N
o
(
x
)
.
N
o
(output of the net),
implementing an asynchronous form of message transmission.
P
!
ρ
.
Each of these processes represents the sequence of actions that consti-
tute a role, in the sense defined for MSR
P
. These processes have the fol-
lowing form
1
:
N
i
(input of the net) to
P
ρ
is a sequential process that
does input a
nd
output only on the network channels.
.ν
n
.P
ρ
P
ρ
=!˜
π
(
x
)
where
P
ρ
Formally,
::=
.P
ρ
|
.P
ρ
. An example specification is given in Appendix A.2.
Again, this definition does not allows protocols that need remembering en-
crypted messages until they are given the key. This form of specification,
which requires to enrich PA with a pattern matching construct, is analyzed
in [4,5].
Q
!
I
=!
0
|
N
o
(
t
)
N
i
(
t
)
P
I
1
...
!
P
I
10
.
This is the specification of the intruder model in a Dolev-
Yao style. Each
P
I
i
describes one capability of the intruder. The dedicated
1
Here we use ˜
π
(
x
)
.P
as a shortcut for
π
1
(
t
1
(
x
1
))
...π
k
(
t
k
(
x
k
))
.P
, and
ν
n
.P
for
νn
1
....νn
h
.P
.
