Fairness Analysis for Multiparty Nonrepudiation Protocols Based on Improved Strand Space
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.
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.
- (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 set A, 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)
If n1, 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)
If n1, 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 term t 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 term t originates on n ∈ N if and only if I = {t′, t⫅t′}.
- (7)
An unsigned term t 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 set A as follows.
Definition 5. The term set A 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 operators Encr: Ks × A → A; Conn A × A → A; and sign P × A → A.
In this paper, we use the notation Ek(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. After Dolev 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.
- (1)
;
- (2)
;
- (3)
.
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 by Znrr 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 receives Znrr 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 the ith 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 receives Znrri 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 receives Znrri, 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.
- (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 of KM Protocol Based on Extended strand Method
5.1. KM Protocol
- (1)
O, T denotes origination party and the trusted third party TTP of protocols;
- (2)
is the subset of R and represents the receiver set which returns the valid evidence to O, ;
- (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 can decrypt and obtain k;
- (11)
Zo = Spo(R, L, C): the evidence of signatured cryptograph C from originator to R;
- (12)
: signatured cryptograph C from originator to Ri receives evidence;
- (13)
: a secret key k is sent to R′ from the signatured O by TTP and the evidence received by R′ from secret key k.
- (1)
O⇒R : R, L, C, Z0;
- (2)
;
- (3)
O⇒T : R′, L, ER(k), Zsk;
- (4)
;
- (5)
.
Firstly, originator O broadcasts C and evidence Z0 to the receiver set R, and R ∈ R′ responses by evidence when it receives the messages, and then O submits k to the trusted third party with group encryption form ; finally, O and R can obtain and evidence Zck from T by obtaining operations.
Nonrepudiation evidence Znrri = (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 in KM 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 entity a 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〉.
KM 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 strand s ∈ ζO[O, R, R′, T, L, m, k], whose traces are , 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 strand s ∈ ζR[O, R, R′, T, L, m, k], whose traces are , 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 strand s ∈ ζT[O, R, R′, T, L, k], whose traces are . 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 the KM Protocol
In order to prove KM protocol that satisfies the fairness, we need to prove the following two propositions.
Proposition 12. Assume the following conditions are true:
- (1)
Σ is a KM 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 and Zck of Znrri;
- (2)
PO ∉ Kρ; ; PT ∉ Kρ (PO, , PT represent the private key of originator party, receiver party, and TTP, 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 a KM strand space, Ω is a bundle in the Σ, and r is a receiver strand in ζR[O, R, R′, T, L, m, k] which includes the compositions ZO and Zck of Znroi;
- (2)
PO ∉ Kρ; PR ∉ Kρ; PT ∉ Kρ ( PO, , PT represents the private key of originator party, receiver party, and TTP, respectively, and Kρ represents a private space known well by penetrator);
- (3)
L ≠ mL, m, k are 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 Proposition 12 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. Term Zck originates from regular node n3.
Proof. As , 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 thus, n3 is not its positive node;
- (2)
〈+k〉, k ∈ K; it follows from the assumption of free encryption that ; 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, . 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 that n3 is in only one penetrator strand. Therefore, n3 is a regular node.
Lemma 15. Assume that n3 is on the regular strand t; then t is a trusted third party of Ω.
Proof. Node n3 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. Term ZRi originates from regular node n2.
Proof. As . 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. As . 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 that n2 is on the regular strand r; then there exists predecessor n1 of n2 in the r and m⫅f(n1).
Proof. Because ZRi⫅n2, , 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 strand r consisting of n1 and n2 is a receiver strand in the bundle of Ω.
Proof. Nodes n1 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 . According to Definition 10, there must exist a node n′ in the receiver strand r to make sure that , which is the third node in the receiver strand while investigating the receiver in bundle Ω.
Lemma 20. Receiver strand r consists of terms Zo and Zck.
Proof. According to the definition of receiver strand in the KM strand space, r obviously contains Zo and Zck.
Summing up the lemmas discussed above, we can derive that Proposition 12 is true.
In order to prove that Proposition 13 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 of KM 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.
Conflict of Interests
The authors declare that there is no conflict of interests regarding the publication of this paper.
Acknowledgments
This work is supported by the 863 Program of China under Grant 2011AA01A201, Technological Brainstorm Project of Henan Province of China under Grant 12B520054, the National Natural Science Foundation of China under Grant 61074016, the Program for Professor of Special Appointment (Eastern Scholar) at Shanghai Institutions of Higher Learning, the Program for New Century Excellent Talents in University under Grant NCET-11-1051, the Leverhulme Trust of the UK, and the Alexander von Humboldt Foundation of Germany.
