Information Technology Reference
In-Depth Information
α
−→
s
,A
s, A
(external par)
α
−→
s, A
B
s
,A
B
The symmetric rules have all been omitted.
3
Properties of Security Protocols
Properties of security protocols, such as confidentiality and authenticity, are
the very objects which security protocols want to guarantee. GSPM provides a
suitable language in which they can be formally addressed and it is easy to verify
whether a security protocol has them as it is supposed to.
3.1
Confidentiality
Confidentiality means that a secret will not leak to those who are not designed
to know it while the protocol is running. Since we use message base to describe a
participant's knowledge, it is natural for us to use
M
m
to express the meaning
“knows”
m
. Usually the secret is shared
between proper participants of the protocol, so a violation of confidentiality can
be seen as the leakage of a secret to the active environment, which leads to the
following definition:
M
that a participant with message base
Definition 1.
Let
C
0
be the initial configuration, if for all paths
s
generated
from
C
0
,
s
m
, then the system satisfies the confidentiality of m.
3.2
Authenticity and Integrity
What authenticity guarantees is that a message supposed to be from a certain
participant is indeed originated by that participant. According to correspondence
assertion, participant
A
has sent a relevant message desired by participant
B
before
B
receives it, we say that
B
authenticates
A
. In order to define it more
precisely, we need some auxiliary definitions:
Definition 2.
Let
α
and
β
be two actions and
s
a path. We say that
α
occurs
prior to
β
in
s
if we have
α
∈
act
(
s
1
)
whenever
s
=
s
1
·
β
·
s
2
, and denote it by
s
|
=
α
←
β
.
Definition 3.
Let
C
0
be the initial configuration, if all paths
s
generated from
C
0
, we have
α
←
β
, then we say that the configuration
C
0
satisfies
s
|
=
α
←
β
,
and denote it by
C
0
|
=
α
←
β
.
Now we can express authenticity as follows: (note that
out
(
Bauth.Abym
)
is an auxiliary action for
B
to make authenticity more explicit)
Definition 4.
If
C
0
B
[
out
(
Bauth.Abym
)]
(here
F
(
m
)
is a composite message generated by A who is the only one to know
m
), then
B
authenticates
A
.
|
=
A
[
out
(
F
(
m
))]
←
