# Fairness Analysis for Multiparty Nonrepudiation Protocols Based on Improved Strand Space

Authors: Lei Li; Licheng Wang; Jing Chen; Ruiming Wang; Zhihong Zhang
Journal: Discrete Dynamics in Nature and Society
 (2014)

---

## Abstract

Aimed at the problem of the fairness analysis for multiparty nonrepudiation protocols, a new formal analysis method based on improved strand space is presented. Based on the strand space theory, signature operation is added; the set of terms, the subterm relation and the set of penetrator traces are redefined and the assumption of free encryption is extended in the new method. The formal definition of fairness in multi-party non-repudiation protocols is given and the guideline to verify it based on improved strand space is presented. Finally, the fairness of multi-party non-repudiation protocols is verified with an example of Kremer-Markowitch protocol, which indicates that the new method is suitable for analyzing the fairness of multiparty nonrepudiation protocols.


---

## Body

## 1. Introduction

As a crucial foundation of the realization of electronic commerce, nonrepudiation protocols provide the nonrepudiation services for the interbehavior between the network entities. Generally speaking, some security properties of the nonrepudiation protocols should be equipped with such as nonrepudiation, fairness, and timeliness, among which the fairness acts as the most important one. The nonrepudiation protocols are usually the ones being of one sender and multireceptors.Formal methods, theory, and supporting tools paly an important role in the design, analysis, and verification of the security-related and cryptographic protocols [1]. There are numbers of approaches for analyzing the security protocol; however, it turns out to be that each one is subjected to its own limitations since it can only analyze a certain class of protocols or security properties. During the period of designing the security protocols, it is required to guarantee the security properties of security protocol as much as possible by applying multikinds of formal analysis methods. Currently, the formal analysis methods based on nonrepudiation protocols can be divided into two classes.(1)
Belief logic method: in [2], Kailar firstly extended the BAN logic and applied it to the analysis of fairness of the nonrepudiation protocols; the authors in [3, 4] analyzed the fairness and timeliness of the nonrepudiation protocols by using belief logic, respectively. In [5, 6], the authors introduced the alternating-time temporal logic analyzing the fairness of the nonrepudiation protocols. However, the formal analysis based on the belief logic method only works under a lot of assumptions.(2)
State space method: the automatic analysis method with a protocol checker adopted in [7] and Petri net method proposed in [8] both need to search the state space; while analyzing the complex space, human intervention is indispensable to both the two methods in case of the blast of state space.In the recent years, some formal methods have been developed which are suitable for the analysis of nonrepudiation protocols; see, for example, [9–11]. However, fairness analysis for multi-party nonrepudiation protocols seems to be more complex, and only nonformal analysis for fairness, and so on, has been done by utilizing various typical kinds of nonrepudiation protocols in [12–14].The theory of strand space is a proof technique which is based on induction and free encryption assumption; furthermore, this theorem can analyze any protocol for any size neither constrained from the amounts of participative entities nor dependent on the state space searching. Nevertheless, in the strand space theory, some cryptographic primitives are lack of definition, such as signature; therefore, it is not suitable for the analysis of the fairness for multi-party nonrepudiation protocols.In this paper, the operation for signature in the strand space theorem is added and the set of terms, subterm relation, and the set of penetrator traces are redefined. The assumption of free encryption is extended in the new method. The formal definition of fairness in multi-party nonrepudiation protocols is given and the guideline to verify it based on improved strand space is presented. Finally, the fairness of multi-party nonrepudiation protocols is verified with an example of Kremer-Markowitch protocol, which indicates that the new method is suitable for analyzing the fairness of multi-party nonrepudiation protocols.


## 2. The Basic Notions of Strand Space [15]

A strand is a sequence of events that a single principal may engage in. Each individual strand is a sequence of message transmissions and receptions, with specific values of all data such as keys and nonces. One may think of a strand space as containing all the legitimate executions of the protocol expected within its useful lifetime, together with all the actions that a penetrator might apply to the messages contained in those executions, together with penetrator part strands. The basic notions of a strand space, as follows.Consider a setA, the elements of which are the possible messages that can be exchanged between principals in a protocol, and we will refer to the elements of A as terms.A strand space is a pair(Σ,tr) with a trace mapping tr:Σ→A, in which Σ is the set of a strand; here, the strand can represent any sequences and be denoted by ζ.Subterm:t1⫅t1 means that t1 is a subterm of t2.Definition 1.
A signed term is a pair〈σ,a〉 with a∈A and σ one of the symbols +,-. One will write a signed term as +t or -t; (±A) is the set of finite sequences of signed terms.Definition 2.
A strand space is a setΣ with a trace mapping tr:Σ→(±A).Definition 3.
Fix a strand space with the following steps.(1)
A node is a pair〈ζ,i〉, with s∈Σ and i an integer satisfying 1≤i≤length(tr(s)). The set of nodes is denoted by N. One will say that the node 〈ζ,i〉 belongs to the strand s. Clearly, every node belongs to a unique strand.(2)
Ifn1,n2∈N, n1→n2 means that term (n1)=+a and term (n2)=-a. It means that node n1 sends the message a, which is received by n2, creating a causal link between their strands.(3)
Ifn1,n2∈N, then n1⇒n2 means that n1,n2 occur on the same strand. It expresses that n1 is an immediate causal predecessor of n2 in the strand.(4)
An unsigned termt occurs in n∈N if and only if t⫅ term (n).(5)
I is an unsigned term set, node n∈N is an entry point of I, if and only if (n)=+t, and whenever n′ precedes n on the same strand, t⫅ term (n).(6)
An unsigned termt originates on n∈N if and only if I={t′,t⫅t′}.(7)
An unsigned termt is uniquely originating if and only if t originates on a unique n∈N.A bundle is a portion of a strand space. It consists of a number of strands legitimate or otherwise hooked together where one strand sends a message and another strand receives that same message. Typically, for a protocol to be correct, each such bundle must contain one strand for each of the legitimate principals apparently participating in this session, all agreeing on the principals, nonces, and session keys. Penetrator strands or stray legitimate strands may also be entangled in a bundle, even in a correct protocol, but they should not prevent the legitimate parties from agreeing on the data values or from maintaining the secrecy of the values chosen.Definition 4.
If→Ω⊂→; ⇒Ω⊂⇒; and Ω=〈NΩ,(→Ω∪⇒Ω)〉 is the subgraph of Ω=〈N,(→∪⇒)〉, then Ω is a bundle if and only if(1)
Ω is a finite acyclic graph;(2)
n2∈NΩ and term N2 is negative; thus, there exists a unique node n1, so that n1→Ωn2;(3)
n2∈NΩ and n1⇒n1, then n1⇒Ωn2.


## 3. The Improved Strand Space

In the basic theorem of strand space, only encryption and connection operation are defined for term set; however, neither the symmetric and asymmetric keys are distinguished nor the signature operation is defined. Nonrepudiation protocols are dependent on the cryptographic primitives of encryption and signature. Therefore, the basic strand space theorem is not suitable for analyzing the fairness of multi-party nonrepudiation protocols. In this paper, we redefine the term setA as follows.Definition 5.
The term setA satisfies the following conditions.(1)
W⊆A is a set of atomic messages.(2)
Wname⊆A is the set of identifiers, ORT are used to denote origination party, receiving party and the trusted third party in our following discussions.(3)
K⊆A is the set of keys; K and W are nonintersect and inv:K→K is a monadic operator mapping one key of the key pair in the asymmetric cryptosystem to another and mapping the symmetric key to itself.(4)
P⊆K, P-1⊆K is the set of asymmetric keys; one denotes the private key set as K and public key as P-1.(5)
Ks⊂K is the set of symmetric keys; Ks and P are nonintersect and also nonintersect with P-1.(6)
Three binary operatorsEncr:Ks×A→A; ConnA×A→A; and signP×A→A.In this paper, we use the notationEk(m), gh, and Sp(m) to denote the encryption of message m by key k, connection between g and h, and the signature of message m by private key P, respectively.Due to the addition of the operation signature, relations of subterms are redefined as follows.Definition 6.
The recursion of subterm relations is defined as the minimum relation which satisfies the following relations:(1)
a⫅a;(2)
a⫅Ek(g) if a⫅g;(3)
a⫅Sp(g) if a⫅g;(4)
a⫅gh if a⫅g∨a⫅h.The stand space theorem builds the model of actions by a penetrator and gives some formal descriptions about the basic penetrations of a penetrator; the penetrator’s powers are mainly depicted by two ingredients, namely, a set of keys known initially to the penetrator and the capabilities to generate new messages from messages he receives.The basic actions of the penetrator are characterized by a set of penetrator traces which are composed of the available atomic actions. Owing to the additions of operations such as signature, the penetrator traces are required to consist of some atomic operations including signature and verification. The penetrator traces are redefined with the following forms.Definition 7.
The penetrator traces include(1)
text message:〈+w〉, w∈W;(2)
key: 〈+k〉, k∈K;(3)
concatenation:〈-g,-h,+gh〉;(4)
separation into components:〈-gh,+g,+gh〉;(5)
encryption:〈-k,-h,+Ek(h)〉;(6)
decryption:〈-k-1,-Ek(h),+h〉;(7)
signature:〈-p,-h,-Sp(h)〉, p∈P;(8)
verification:〈-p-1,-Sp(h),+h〉.In the assumption of free encryption, it stipulates that a ciphertext can be regarded as a ciphertext in just one way. AfterDolev and Yao, the assumption of free encryption has been fully applied to different kinds of formal analysis methods.In the basic strand space theorem,A is the algebra freely generated from K and W by the two operators’ encryption and join. The following are some extensions of the assumption of free encryption due to the addition of signature operation.Axiom. For m′,m′∈A, k,k′∈Ks, Pa,Pb,Pc∈P, a,b,c∈Wname,(1)
SPa(m)=SPb(m′)⇔m=m′∧Pa=Pb∧a=b;(2)
mm′≠Ek′(m)≠SPc(m′);(3)
SPc(m)≠W∪K.The improved strand space method is a formal analysis method consisting of some key concepts, for example, the redefined term set, relations between subterms, penetrator traces, extended assumption of free encryption, and the bundles in the basic strand space, and also combining with protocol traces and theorem proof.


## 4. Definition of Fairness and Proof Line

Among numbers’ properties of the nonrepudiation protocols possess, fairness is the most important one which includes two aspects; first, when the protocols are completed, the origination party received the evidence of nonrepudiation protocols from receiving party and denoted byZnrr was well as receiving party received the evidence of nonrepudiation protocols from origination party and is denoted by Znro; second, when the protocols are terminated abruptly, it should have the capability to keep both sides of communication equal and neither sides in a dominant position. Hence, we make a formal definition as the following form about fairness.Definition 8.
If the origination party receivesZnrr if and only if the receiving party receives Znor, then we say that the nonrepudiation protocols satisfy the fairness.
In the multi-party nonrepudiation protocols, there exists one origination party and multireceiving parties, and in the process of protocol running, it is allowable that some receiving parties complete the protocols and the others terminate the protocols. If we denote theith receiver as Ri, the ith nonrepudiation evidence of receiving party as Znrri, and the ith nonrepudiation evidence of origination party as Znroi, then the fairness is defined as follows.Definition 9.
If the origination party receivesZnrri if and only if the receiving party receives Znroi, then one says that the nonrepudiation protocols satisfy the fairness.
We can consider the proof of fairness from two aspects: firstly, when origination party receivesZnrri, it is sure that the receiving party receives Znroi; secondly, when origination party O receives Znroi, then the receiving party R certainly receives Znrri. Hence, the conditions in Definition 9 are satisfied and the protocols are guaranteed to meet the fairness.The proof steps of the fairness of multi-party nonrepudiation protocols by using the improved strand model are listed as follows.(1)
Build the strand model for multi-party nonrepudiation protocols.(2)
Prove that if there exists originator strand in bundleΩ and the nodes in the stand contain term Znrri, then there must exist receiver strand as well as the nodes in this strand contain term Znroi.(3)
Prove that if there exists receiver strand in bundleΩ and the nodes in the strand contain term Znroi, then there must exist originator strand as well as the nodes in this stand contain term Znrri.


## 5. Prove the Fairness ofKM Protocol Based on Extended strand Method

### 5.1.KM Protocol

K
M protocol is a typical multi-party nonrepudiation protocol, and we denote the notation in the protocol as follows:(1)
O, T denotes origination party and the trusted third party TTP of protocols;(2)
R=PR1′(R1′),PR2′(R1′),…:R′ is the subset of R and represents the receiver set which returns the valid evidence to O, Ri′∈R′;(3)
l represents the unique identifier of the current running protocol;(4)
m: message from O to R;(5)
k: a symmetric secret key used when O encrypts M;(6)
C=Ek(m): cryptograph of message M from O to R;(7)
A→B: customer A sends a message to customer B;(8)
A⇒B: customer A broadcasts a message to customer B;(9)
A↔B: the obtained operations of A to B, namely, A can always get messages from B;(10)
ER(m) encrypts secret key k by utilizing the group encryption mechanism, and only Ri′∈R′ can decrypt and obtain k;(11)
Zo=Spo(R,L,C): the evidence of signatured cryptograph C from originator to R;(12)
Zri=Sri(O,L,C): signatured cryptograph C from originator to Ri receives evidence;(13)
Zsk=SPo(R′,L,ER′(k)): a secret key k is sent to R′ from the signatured O by TTP and the evidence received by R′ from secret key k.TheKM protocol can be described as follows:(1)
O⇒R:R,L,C,Z0;(2)
Ri⇒O:O,L,ZRi;(3)
O⇒T:R′,L,ER(k),Zsk;(4)
R↔T:O,R′,L,ER′(k),Zck;(5)
O↔T:O,R′,L,ER′(k),Zck.Firstly, originatorO broadcasts C and evidence Z0 to the receiver set R, and R∈R′ responses by evidence ZRi when it receives the messages, and then O submits k to the trusted third party with group encryption form ER′(k); finally, O and R can obtain ER′(k) and evidence Zck from T by obtaining operations.Nonrepudiation evidenceZnrri=(Zri,Zck); Znroi=(Zo,Zck) for all Ri∈R′. If there exists any argument, O can submit Znroi to arbitration agency for arbitration.


### 5.2.KM Strand Space

The obtained operations inKM protocol can be regarded as the message m can be always received by O and R from T. Denote f(n) as the sign term of node n and f′(n) as the unsigned parts of f(n). The obtained operation can be defined as follows in the improved strand space.Definition 10.
If entitya obtains message m from T by obtained operation, then strand ζT satisfies ∃i·f(〈ζT,i〉). Denoting bundle Ω as an arbitrary bundle satisfying ζT∈Ω, there always exists ζa∈Ω satisfying ∃j·f(〈ζa,j〉)=-m and 〈ζT,i〉≺〈ζa,j〉.K
M strand space can be depicted with the following form.Definition 11.
Assuming that(Σ,ρ) is a penetrator strand space, if Σ is comprised of the following four kinds of strands, then one says that Σ is a KM strand space. (1)
The penetrator strand:s∈ρ.(2)
The originator strands∈ζO[O,R,R′,T,L,m,k], whose traces are 〈+RLEk(m)Zo,-OLZRi,+R′LER′(K)Zsk,-OR′LER′(k)Zck〉, O,R,R′,T∈Wname; L,m∈W, and L,m∉Wname; k∈Ks. Here, ζO[O,R,R′,Lm,k] is a trace set whose elements are the traces discussed above and the corresponding entity is originator O.(3)
The receiver strands∈ζR[O,R,R′,T,L,m,k], whose traces are 〈-RLEk(m)Zo,+OLZRi,-OR′LER′(k)Zck〉, O,R,R′,T∈Wname; L,m∈W and L,m∉Wname; k∈Ks. Here, ζO[O,R,R′,Lm,k] is a trace set whose elements are the traces discussed above and the corresponding entity is receiver Ri.(4)
The trusted third strands∈ζT[O,R,R′,T,L,k], whose traces are 〈-R′LER′(k)Zsk,+ORLER′Zck,+ORLER′Zck〉. Here, ζT[O,R,T,L,k] is a trace set whose elements are the traces discussed above and the corresponding entity is the trusted third part T.We say that the originator strand, receiver strand, and trusted third strand are all regular strands whose nodes are called regular nodes. Given a strand in theΣ, we can confirm that whether it belongs to penetrator strand, originator strand, receiver strand, or the trusted third part strand uniquely form its formal. Therefore, there is no confusion for omitting ρ of the KM strand space (Σ,ρ).


### 5.3. Analysis of Fairness of theKM Protocol

In order to proveKM protocol that satisfies the fairness, we need to prove the following two propositions.Proposition 12.
Assume the following conditions are true:
(1)
Σ
is a
K
M
strand space,
Ω
is a bundle in the
Σ
, and
s
is an originator strand in
ζ
0
[
O
,
R
,
R
′
,
T
,
L
,
m
,
k
]
which includes the compositions
Z
R
i
and
Z
c
k
of
Z
n
r
r
i
;
(2)
P
O
∉
K
ρ
;
P
R
i
∉
K
ρ
;
P
T
∉
K
ρ
(
P
O
,
P
R
i
,
P
T
represent the private key of originator party, receiver party, and
T
T
P
, respectively, and
K
ρ
represents a private space known well by penetrator);
(3)
L
≠
m
;
L
,
m
,
k
are the only original terms in
Σ
;
then the bundleΩ consists of a receiver strand r∈ζR[O,R,R′,T,L,m,k] as well as r consists of the compositions Zo and Zck of Znroi.Proposition 13.
Assume the following conditions are true:(1)
Σis aKMstrand space,Ωis a bundle in theΣ, andris a receiver strand inζR[O,R,R′,T,L,m,k]which includes the compositionsZOandZckofZnroi;(2)
PO∉Kρ;PR∉Kρ;PT∉Kρ(PO,PRi,PTrepresents the private key of originator party, receiver party, andTTP, respectively, andKρrepresents a private space known well by penetrator);(3)
L≠mL,m,kare the only original terms inΣ;
then the bundleΩ consists of an originator strand r∈ζO[O,R,R′,T,L,m,k] as well as s consists of the compositions ZRi and Zck of Znrri.In the following section, we focus our attention on the proof of Proposition12 in terms of a series of lemmas. Choose Σ, Ω, s, O, R, T, L, m, k arbitrarily which satisfy the assumptions in Proposition 12. It is obvious that terms ZRi and Zck are included in s. The output value RLEk(m)ZO of node 〈s,1〉 is denoted by n0 whose term is denoted by v0.Lemma 14.
TermZck originates from regular node n3.Proof.
AsZck=SPT(O,R′,L,ER′(k)), we assume that term Zck originates from regular node n3, and then we investigate the probability of positive node in the penetrator traces, respectively:(1)
〈+w〉, w∈W; it follows from the assumption of free encryption that Zck⫅w thus, n3 is not its positive node;(2)
〈+k〉, k∈K; it follows from the assumption of free encryption that Zck⫅k; thus, n3 is not its positive node;(3)
〈-g,-h,+gh〉; if n3 is its positive node, then Zck⫅gh and we can confirm that Zck⫅g∨Zck⫅h. Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(4)
〈-gh,+g,+h〉; if n3 is its positive node, then Zck⫅g∨Zck⫅h and we can confirm that Zck⫅gh. Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(5)
〈-k,-h,+Ek(h)〉; if n3 is its positive node, we can confirm that Zck⫅h since Ek(h)≠Zck. Therefore, there obviously exsits positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(6)
〈-k-1,-Ek(h),+h〉; if n3 is its positive node, then Zck⫅h and we can confirm that Zck⫅Ek(h). Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(7)
〈-p,-h,+Sp(h)〉; Sp(h)≠Zck since p∈Kp, PT⫅Kp. Hence, if n3 is its positive node, then Zck⫅Sp(h) and we can confirm that Zck⫅h. Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(8)
〈-p-1,-Sp(h),+h〉; if n3 is its positive node, then Zck⫅h and we can confirm that Zck⫅Sp(h). Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node.
Summing up the above discussions, it is impossible thatn3 is in only one penetrator strand. Therefore, n3 is a regular node.Lemma 15.
Assume thatn3 is on the regular strand t; then t is a trusted third party of Ω.Proof.
Noden3 is a positive regular node containing terms with the form of Sp(a,b,c,d). Among the whole regular nodes, only the second and third nodes of the trusted third strand consist of such terms; furthermore, n3 is the original node of Zck; hence, n3 is the second node of the trusted third party strand. It follows from the creditability of the trusted third party that there must exist the third strand of this strand; therefore, t is the trusted third party strand of bundle Ω.Lemma 16.
TermZRi originates from regular node n2.Proof.
AsZRi=SPRi(O,L,EK(m)). Assuming that term ZRi originates from n2, we investigate the penetrator traces successively. With the similar proof of Lemma 14, we can conclude that n2 is the regular node.Lemma 17.
m originates from regular node n0.Proof.
AsZRi=SPRi(O,L,EK(m)). It follows from the assumption that m⫅n0 and n0 is positive. Since there is no predecessor in the strand which n0 locates, we can derive that m originates from n0.Lemma 18.
It is assumed thatn2 is on the regular strand r; then there exists predecessor n1 of n2 in the r and m⫅f(n1).Proof.
BecauseZRi⫅n2, ZRi⫅n0, we have n2≠n0. It can be seen that m originates from n0; together with condition (3) of Proposition 12, we have only m original in the Σ; hence, m does not originate from n2. Furthermore, m⫅ZRi⫅f(n2), then there must exist predecessor n1 of n2 in the strand r to guarantee m⫅f(n1).Lemma 19.
Regular strandr consisting of n1 and n2 is a receiver strand in the bundle of Ω.Proof.
Nodesn1 and n2 in the regular strand r satisfy the following properties: (1)  n2 is a positive regular node; (2)  n2 consists of a subterm with form of Sp(a,b,Ek(c)); (3)  n1 and n2 are predecessors in the strand r; and (4)  m⫅f(n1). Investigating the whole regular strands in the bundle of Ω, we found that only the first and the second nodes of the receiver strand satisfy the conditions listed above. Regular strand r consisting of n1 and n2 is a receiver strand in the bundle of Ω. In addition, from Lemma 15 we can see that there exists a trusted third party t to guarantee f(〈t,3〉)=+OR′LER′(k)Zck. According to Definition 10, there must exist a node n′ in the receiver strand r to make sure that f(n′)=-OR′LER′(k)Zck, which is the third node in the receiver strand while investigating the receiver in bundle Ω.Lemma 20.
Receiver strandr consists of terms Zo and Zck.Proof.
According to the definition of receiver strand in theKM strand space, r obviously contains Zo and Zck.Summing up the lemmas discussed above, we can derive that Proposition12 is true.In order to prove that Proposition13 along the similar proof line, we can firstly prove there exists a trusted third party in the bundle Ω in terms of the original of Zck, and then prove that there exists originator strand in bundle Ω by using the original of m,k,Zo.


## 5.1.KM Protocol

K
M protocol is a typical multi-party nonrepudiation protocol, and we denote the notation in the protocol as follows:(1)
O, T denotes origination party and the trusted third party TTP of protocols;(2)
R=PR1′(R1′),PR2′(R1′),…:R′ is the subset of R and represents the receiver set which returns the valid evidence to O, Ri′∈R′;(3)
l represents the unique identifier of the current running protocol;(4)
m: message from O to R;(5)
k: a symmetric secret key used when O encrypts M;(6)
C=Ek(m): cryptograph of message M from O to R;(7)
A→B: customer A sends a message to customer B;(8)
A⇒B: customer A broadcasts a message to customer B;(9)
A↔B: the obtained operations of A to B, namely, A can always get messages from B;(10)
ER(m) encrypts secret key k by utilizing the group encryption mechanism, and only Ri′∈R′ can decrypt and obtain k;(11)
Zo=Spo(R,L,C): the evidence of signatured cryptograph C from originator to R;(12)
Zri=Sri(O,L,C): signatured cryptograph C from originator to Ri receives evidence;(13)
Zsk=SPo(R′,L,ER′(k)): a secret key k is sent to R′ from the signatured O by TTP and the evidence received by R′ from secret key k.TheKM protocol can be described as follows:(1)
O⇒R:R,L,C,Z0;(2)
Ri⇒O:O,L,ZRi;(3)
O⇒T:R′,L,ER(k),Zsk;(4)
R↔T:O,R′,L,ER′(k),Zck;(5)
O↔T:O,R′,L,ER′(k),Zck.Firstly, originatorO broadcasts C and evidence Z0 to the receiver set R, and R∈R′ responses by evidence ZRi when it receives the messages, and then O submits k to the trusted third party with group encryption form ER′(k); finally, O and R can obtain ER′(k) and evidence Zck from T by obtaining operations.Nonrepudiation evidenceZnrri=(Zri,Zck); Znroi=(Zo,Zck) for all Ri∈R′. If there exists any argument, O can submit Znroi to arbitration agency for arbitration.


## 5.2.KM Strand Space

The obtained operations inKM protocol can be regarded as the message m can be always received by O and R from T. Denote f(n) as the sign term of node n and f′(n) as the unsigned parts of f(n). The obtained operation can be defined as follows in the improved strand space.Definition 10.
If entitya obtains message m from T by obtained operation, then strand ζT satisfies ∃i·f(〈ζT,i〉). Denoting bundle Ω as an arbitrary bundle satisfying ζT∈Ω, there always exists ζa∈Ω satisfying ∃j·f(〈ζa,j〉)=-m and 〈ζT,i〉≺〈ζa,j〉.K
M strand space can be depicted with the following form.Definition 11.
Assuming that(Σ,ρ) is a penetrator strand space, if Σ is comprised of the following four kinds of strands, then one says that Σ is a KM strand space. (1)
The penetrator strand:s∈ρ.(2)
The originator strands∈ζO[O,R,R′,T,L,m,k], whose traces are 〈+RLEk(m)Zo,-OLZRi,+R′LER′(K)Zsk,-OR′LER′(k)Zck〉, O,R,R′,T∈Wname; L,m∈W, and L,m∉Wname; k∈Ks. Here, ζO[O,R,R′,Lm,k] is a trace set whose elements are the traces discussed above and the corresponding entity is originator O.(3)
The receiver strands∈ζR[O,R,R′,T,L,m,k], whose traces are 〈-RLEk(m)Zo,+OLZRi,-OR′LER′(k)Zck〉, O,R,R′,T∈Wname; L,m∈W and L,m∉Wname; k∈Ks. Here, ζO[O,R,R′,Lm,k] is a trace set whose elements are the traces discussed above and the corresponding entity is receiver Ri.(4)
The trusted third strands∈ζT[O,R,R′,T,L,k], whose traces are 〈-R′LER′(k)Zsk,+ORLER′Zck,+ORLER′Zck〉. Here, ζT[O,R,T,L,k] is a trace set whose elements are the traces discussed above and the corresponding entity is the trusted third part T.We say that the originator strand, receiver strand, and trusted third strand are all regular strands whose nodes are called regular nodes. Given a strand in theΣ, we can confirm that whether it belongs to penetrator strand, originator strand, receiver strand, or the trusted third part strand uniquely form its formal. Therefore, there is no confusion for omitting ρ of the KM strand space (Σ,ρ).


## 5.3. Analysis of Fairness of theKM Protocol

In order to proveKM protocol that satisfies the fairness, we need to prove the following two propositions.Proposition 12.
Assume the following conditions are true:
(1)
Σ
is a
K
M
strand space,
Ω
is a bundle in the
Σ
, and
s
is an originator strand in
ζ
0
[
O
,
R
,
R
′
,
T
,
L
,
m
,
k
]
which includes the compositions
Z
R
i
and
Z
c
k
of
Z
n
r
r
i
;
(2)
P
O
∉
K
ρ
;
P
R
i
∉
K
ρ
;
P
T
∉
K
ρ
(
P
O
,
P
R
i
,
P
T
represent the private key of originator party, receiver party, and
T
T
P
, respectively, and
K
ρ
represents a private space known well by penetrator);
(3)
L
≠
m
;
L
,
m
,
k
are the only original terms in
Σ
;
then the bundleΩ consists of a receiver strand r∈ζR[O,R,R′,T,L,m,k] as well as r consists of the compositions Zo and Zck of Znroi.Proposition 13.
Assume the following conditions are true:(1)
Σis aKMstrand space,Ωis a bundle in theΣ, andris a receiver strand inζR[O,R,R′,T,L,m,k]which includes the compositionsZOandZckofZnroi;(2)
PO∉Kρ;PR∉Kρ;PT∉Kρ(PO,PRi,PTrepresents the private key of originator party, receiver party, andTTP, respectively, andKρrepresents a private space known well by penetrator);(3)
L≠mL,m,kare the only original terms inΣ;
then the bundleΩ consists of an originator strand r∈ζO[O,R,R′,T,L,m,k] as well as s consists of the compositions ZRi and Zck of Znrri.In the following section, we focus our attention on the proof of Proposition12 in terms of a series of lemmas. Choose Σ, Ω, s, O, R, T, L, m, k arbitrarily which satisfy the assumptions in Proposition 12. It is obvious that terms ZRi and Zck are included in s. The output value RLEk(m)ZO of node 〈s,1〉 is denoted by n0 whose term is denoted by v0.Lemma 14.
TermZck originates from regular node n3.Proof.
AsZck=SPT(O,R′,L,ER′(k)), we assume that term Zck originates from regular node n3, and then we investigate the probability of positive node in the penetrator traces, respectively:(1)
〈+w〉, w∈W; it follows from the assumption of free encryption that Zck⫅w thus, n3 is not its positive node;(2)
〈+k〉, k∈K; it follows from the assumption of free encryption that Zck⫅k; thus, n3 is not its positive node;(3)
〈-g,-h,+gh〉; if n3 is its positive node, then Zck⫅gh and we can confirm that Zck⫅g∨Zck⫅h. Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(4)
〈-gh,+g,+h〉; if n3 is its positive node, then Zck⫅g∨Zck⫅h and we can confirm that Zck⫅gh. Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(5)
〈-k,-h,+Ek(h)〉; if n3 is its positive node, we can confirm that Zck⫅h since Ek(h)≠Zck. Therefore, there obviously exsits positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(6)
〈-k-1,-Ek(h),+h〉; if n3 is its positive node, then Zck⫅h and we can confirm that Zck⫅Ek(h). Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(7)
〈-p,-h,+Sp(h)〉; Sp(h)≠Zck since p∈Kp, PT⫅Kp. Hence, if n3 is its positive node, then Zck⫅Sp(h) and we can confirm that Zck⫅h. Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node;(8)
〈-p-1,-Sp(h),+h〉; if n3 is its positive node, then Zck⫅h and we can confirm that Zck⫅Sp(h). Therefore, there obviously exists positive node n′ to make sure that Zck⫅f(n′)∧n′≺n3, which is in contradiction with that n is the original node.
Summing up the above discussions, it is impossible thatn3 is in only one penetrator strand. Therefore, n3 is a regular node.Lemma 15.
Assume thatn3 is on the regular strand t; then t is a trusted third party of Ω.Proof.
Noden3 is a positive regular node containing terms with the form of Sp(a,b,c,d). Among the whole regular nodes, only the second and third nodes of the trusted third strand consist of such terms; furthermore, n3 is the original node of Zck; hence, n3 is the second node of the trusted third party strand. It follows from the creditability of the trusted third party that there must exist the third strand of this strand; therefore, t is the trusted third party strand of bundle Ω.Lemma 16.
TermZRi originates from regular node n2.Proof.
AsZRi=SPRi(O,L,EK(m)). Assuming that term ZRi originates from n2, we investigate the penetrator traces successively. With the similar proof of Lemma 14, we can conclude that n2 is the regular node.Lemma 17.
m originates from regular node n0.Proof.
AsZRi=SPRi(O,L,EK(m)). It follows from the assumption that m⫅n0 and n0 is positive. Since there is no predecessor in the strand which n0 locates, we can derive that m originates from n0.Lemma 18.
It is assumed thatn2 is on the regular strand r; then there exists predecessor n1 of n2 in the r and m⫅f(n1).Proof.
BecauseZRi⫅n2, ZRi⫅n0, we have n2≠n0. It can be seen that m originates from n0; together with condition (3) of Proposition 12, we have only m original in the Σ; hence, m does not originate from n2. Furthermore, m⫅ZRi⫅f(n2), then there must exist predecessor n1 of n2 in the strand r to guarantee m⫅f(n1).Lemma 19.
Regular strandr consisting of n1 and n2 is a receiver strand in the bundle of Ω.Proof.
Nodesn1 and n2 in the regular strand r satisfy the following properties: (1)  n2 is a positive regular node; (2)  n2 consists of a subterm with form of Sp(a,b,Ek(c)); (3)  n1 and n2 are predecessors in the strand r; and (4)  m⫅f(n1). Investigating the whole regular strands in the bundle of Ω, we found that only the first and the second nodes of the receiver strand satisfy the conditions listed above. Regular strand r consisting of n1 and n2 is a receiver strand in the bundle of Ω. In addition, from Lemma 15 we can see that there exists a trusted third party t to guarantee f(〈t,3〉)=+OR′LER′(k)Zck. According to Definition 10, there must exist a node n′ in the receiver strand r to make sure that f(n′)=-OR′LER′(k)Zck, which is the third node in the receiver strand while investigating the receiver in bundle Ω.Lemma 20.
Receiver strandr consists of terms Zo and Zck.Proof.
According to the definition of receiver strand in theKM strand space, r obviously contains Zo and Zck.Summing up the lemmas discussed above, we can derive that Proposition12 is true.In order to prove that Proposition13 along the similar proof line, we can firstly prove there exists a trusted third party in the bundle Ω in terms of the original of Zck, and then prove that there exists originator strand in bundle Ω by using the original of m,k,Zo.


## 6. Conclusions

It can be seen that some operations have not been defined in the basic strand space theorem such as signature. In this paper, we add the signature operation and redefine the term set, relations between subterms, and penetrator traces as well as extend the assumption of free encryption. Furthermore, the formal definition of fairness of multiparty nonrepudiation protocols is put forward. Idea and method of fairness analysis for multi-party nonrepudiation protocols based on improved strand space have been discussed in detail. Analyzing the fairness ofKM protocol by using the analysis method based on improved strand space, we can conclude that KM protocol satisfies the fairness property, which shows that our improved strand space method is suitable for fairness analysis for multi-party nonrepudiation protocols. Kim’s work [16] has revealed that ZG protocol in [17] cannot meet the timeliness. Our further research topic would be to investigate the corresponding other properties for multi-party nonrepudiation protocols, such as nonrepudiation and/or timeliness. Consequently, it is an extension of our results and seems to be much more interesting and challenging.



---

*Source: 904717-2014-01-02.xml*