Information Technology Reference
In-Depth Information
β
. Since it
usually requires that data cannot be corrupted or at least that any corruption
will always be detected. In other words, the input message should match the
output message.
Integrity also can be easily expressed by the notion of
α
←
Definition 5.
Integrity means that for all
M
,
C
0
|
=[
out
(
M
)]
←
[
in
(
M
)]
.
There is no participant ID before the action for we don't care about who is
the actor.
3.3
Non-repudiation and Fairness
Non-repudiation and fairness mainly concern electronic commerce protocol,
which provides services among participants that don't trust each other
[17].
In [16] Schneider discusses the non-repudiation in his CSP model.
Firstly, we give the definitions of two evidences used in analysis:
NRO
and
NRR
. Non-Repudiation of Origin (
NRO
) is an evidence intended to protect
the receiver from the deliberate denial of the other participant of having sent
a message; Non-Repudiation of Receipt (
NRR
) is another evidence intended to
protect the sender from the deliberate denial of the other participant of having
received a message.
Definition 6.
Let
C
0
be the initial configuration, if for all paths
s
generated
from
C
0
,
(
msg
(
s
)
∪EM
0
∪IM
R
)
NRO
(i.e. the receiver
Id
R
possesses
NRO
),
then the protocol is said to have the sender non-repudiation property;
(
msg
(
s
)
∪
EM
0
∪
NRR
(i.e. the sender
Id
O
possesses
NRR
), then the protocol is
said to have the receiver non-repudiation property.
IM
O
)
Fairness can be seen as the combination of two non-repudiation properties,
for at no point in a protocol's run one participant will have any advantage over
another. In other words, none of the participants can get his or her evidence
while the other cannot.
Definition 7.
Let
C
0
be the initial configuration, if for all paths
s
generated
from
C
0
,
(
msg
(
s
)
∪
EM
0
∪
IM
R
)
NRO
∧
(
msg
(
s
)
∪
EM
0
∪
IM
O
)
NRR
or
((
msg
(
s
)
∪
EM
0
∪
IM
R
)
NRO
)
∧
((
msg
(
s
)
∪
EM
0
∪
IM
O
)
NRR
)always
holds, the protocol is fair.
3.4
Anonymity
Anonymity is another property that mainly concerns electroniccommercepro-
tocol and it seems to have been hardly explored from a formal point of view.
Intuitively a system is anonymous over some set of events
E
means that even
though an observer can deduce that an event from
E
has occurred but he or she
should not be able to identify which.
Definition 8.
Let
C
0
be the initial configuration, if for all paths
s
generated
from
C
0
,
(
msg
(
s
)
∪
EM
0
∪
IM
A
)
m
, we say that the protocol has anonymity
over message
m
for participant
A
.
