Information Technology Reference
In-Depth Information
-
P
!
A
=!
˜
π
(
A
)
.νN
A
.
N
i
(
{A, N
A
}
K
B
)
.
N
o
(
{B, N
A
,N
B
}
K
A
)
.
N
i
(
{N
B
}
K
B
)
.
0.
-
P
!
B
=!
˜
π
(
B
)
.νN
B
.
N
o
(
{A, N
A
}
K
)
.
N
i
(
{B, N
A
,N
B
}
K
A
)
.
N
o
(
{N
B
}
K
B
)
.
0
A, B, K
A
,K
A
,K
B
) and
B, A, K
B
,K
B
,K
A
),
where, as for MSR
P
,
A
=(
B
=(
π
X, Y, K
X
,K
X
,K
Y
) inputs each of the object in ˜
π
X, Y, K
X
,K
X
,K
Y
)
and
˜
(
(
(see A.1). More precisely, it is defined as
X, K
X
)
K
X
,K
X
)
(
X
)
.
PrK
(
.
PbK
(
Y, K
Y
)
.
Kp
(
.
Pr
-
Q
!
π
=
Q
π
(
a,b,k
a
,k
a
,k
b
)
Q
π
(
b,e,k
b
,k
b
,k
e
)
Q
π
(
e,a,k
e
,k
e
,k
a
)
where
Q
π
(
X,Y,K
X
,K
X
,K
Y
)
is the parallel composition of simple replicated pro-
cesses that output each object in ˜
X, Y, K
X
,K
X
,K
Y
) on channel
π
(
π
:
X, K
X
K
X
,K
X
!
(
X
)
.
0
!
(
)
.
0
!
(
Y, K
Y
)
.
0
!
(
)
.
0
.
Pr
PrK
PbK
Kp
k
e
-
Q
I
0
=
I
(
e
)
.
0
I
(
k
e
)
.
0
I
(
)
.
0.