Xu GUO

Department of Electronics and Information， Shanghai Dianji University， Shanghai 201306， China E-mail: guox@sdju.edu.cn

Received Aug. 29， 2021; Revision accepted Dec. 17， 2021; Crosschecked Mar. 23， 2022

Abstract: Many traditional applications can be refined thanks to the development of blockchain technology. One of these services is non-repudiation， in which participants in a communication process cannot deny their involvement.Due to the vulnerabilities of the non-repudiation protocols， one of the parties involved in the communication can often avoid non-repudiation rules and obtain the expected information to the detriment of the interests of the other party， resulting in adverse effects. This paper studies the fairness guarantee quantitatively through probabilistic model checking. E-fairness is measured by modeling the protocol in probabilistic timed automata and verifying the appropriate property specified in the probabilistic computation tree logic. Furthermore， our analysis proposes insight for choosing suitable values for different parameters associated with the protocol so that a certain degree of fairness can be obtained. Therefore， the reverse question—for a certain degree of fairness ε， how can the protocol parameters be specified to ensure fairness—is answered.

Key words: Non-repudiation; Fairness analysis; Probabilistic model checking; PRISM

1 Introduction

1.1 Background

With the rapid growth of smart terminals，blockchain technology has been widely studied(Dinh et al.， 2018). This technology not only provides an acentric infrastructure in different fields， including medicine (Griggs et al.， 2018; Christodoulou et al.，2020;Resiere et al.，2020)，Internet of Things(Novo，2018; Hang and Kim， 2019)， economics (Esfahani and Mohammed， 2018; Allen et al.， 2020)， software engineering (Litchfield and Herbert， 2018; Erhan et al.， 2019; Mendiboure et al.， 2020)， and even Covid-19 fighting (Yu et al.， 2021)， but also maintains continuous and tamper-resistant data records in chronological order. Moreover， it has become a hot issue in both academia and industry (Wu et al.，2018;Deng et al.，2019;Feng et al.， 2019). With the wide application of blockchain，fairness requirements have appeared in almost all the application scenarios， such as the issues of double payment and hard fork，which are caused by block conflicts(Pérez-Solà et al.， 2019)， and directly affect the integrity and effectiveness of E-commerce transactions.

Repudiation is defined as the denial by one party of having been involved in the whole or part in a communication process (Fig. 1). For the originator， which is a service provider， repudiation means that it denies having sent a message. For a recipient that acts as a client， repudiation refers to its denial of having received the message. Fairness requires that two parties involved in the communication be treated equally， and that neither of the parties can obtain an advantage over the other. One party can reach a state where it can terminate the communication process to maintain fairness without relying on the actions of the other. To solve the problem， the protocols that can offer non-repudiation services are called non-repudiation protocols. Non-repudiation is one of the vital security services in blockchain technology. It is applied mainly in electronic commerce and message transmission systems(Ruland and Sassmannshausen，2015).

Fig. 1 Communication model

This paper studies the fairness of the nonrepudiation protocol proposed by Markowitch and Roggeman(1999). It offers non-repudiation services without the involvement of a trusted third party(TTP). The fairness property of this protocol is ensured by a given degree of fairness，toleranceε. That is， either both parties receive their expected items，or the probability that a malicious party obtains any valuable information，while the other party achieves nothing，is less thanε，whereε ∈[0，1]. The protocol can guarantee non-repudiation with certain probabilities，where toleranceεis affected by different protocol parameter values. Because different configurations may produce different fairness problems， this paper uses probabilistic model checking to analyze the fairness quantitatively. Specifically， this paper studies the following questions: (1) Does parameter configuration affect the fairness? If so， what is the impact? (2)If the recipient behaves dishonestly，can the fairness be guaranteed? (3) How should the parameters be set to ensure fairness? The participants in the non-repudiation protocol are modeled as two separate units composed of the originator (O) and the recipient(R)in the setting of probabilistic model checking. They are described in the specification of PRISM， which is a probabilistic model checker.

1.2 Related works

The related works summarized in this study fall into four categories:

1. Design of non-repudiation protocols

The ownership of a radio frequency identification (RFID) tags item changes frequently during its lifetime， but few protocols address the nonrepudiation problem. Piramuthu (2017) proposed a non-repudiation protocol for transferring ownership of tagged items. Because blockchain technology can provide an unchangeable data registration system， the services must provide fair， certified notifications that require a fair exchange of values. The data are composed of a message and the proof of non-repudiation origin. Mut-Puigserver et al.(2018)provided two solutions that allow certified notations to be sent when it is necessary to keep secret or register the contents of the notice.

2.Security analysis of non-repudiation protocols

Chatterjee and Raman(2014)studied the automatic synthesis of a fair non-repudiation protocol by applying game-theoretic controller synthesis. In addition to model checking，assume-guarantee strategy can discover the vulnerabilities of a designed protocol using counter-examples in synthesis. The purpose of Chatterjee and Raman(2014)’s work was to use non-repudiation as an example to show that uncertainty methods based on information flow theory are not enough to verify the security of cryptographic protocols.

3. Security assurance of non-repudiation protocols

Sarr et al. (2019) proposed an identification scheme based on a combination of the Rivest–Shamir–Adleman (RSA) algorithm and a strongly unforgeable signature scheme. The scheme is noninteractive， non-repudiation and is shown to be inside secure under the RSA assumption and the random oracle model. Roscoe and Ryan (2017)studied how to approximate fair exchange without a TTP for password authenticated key exchange (PAKE) protocols. They considered two scenarios: in the first scenario，two parties exchanged stochastically and in the second scenario， there was an intruder that can guess the password with probabilityε.

4. Fairness and privacy protection strategies in the context of non-repudiation

Decentralization is a mainstream approach for privacy protection and fair exchange. Li et al.(2021)presented a fair big data exchange scheme，which can guarantee that buyers and sellers can complete transactions fairly and autonomously without a TTP. To enhance security and privacy， Li et al. (2021) also applied anm-out-of-noblivious transfer protocol on the transactions， and applied an Ether cheque system to guarantee fairness and autonomy. Baza et al.(2021)proposed B-Ride，a decentralized ride-sharing service， based on a public blockchain. The aim of B-Ride is to ensure (1) the tradeoffbetween trip information sharing and personal privacy protection，(2)the accountability under anonymity，and(3)fair payment without a TTP.

The above studies can greatly enhance nonrepudiation protocol security， check security problems in the protocol， and balance the tradeoffbetween privacy protection and fair data sharing， but do not provide quantitative fairness analysis of nonrepudiation protocols. The aim of this work is to fill in this gap.

1.3 Contributions

The contributions of this paper can be summarized as follows:

1. Fairness analysis is very important for blockchain technology， but there is little literature on this aspect. To fill in the gap，this paper provides a quantitative analysis of the fairness of Markowitch and Roggeman(1999)’s non-repudiation protocol.

2. Three evolutionary versions of the protocol are considered. That is， both parties’ compliance with the protocol and the recipient’s deception are considered. Moreover， the recipient’s ability to deceive is enhanced with improved processing ability.

3. The protocol’s fairness performance under different parameter configurations is presented and relevant opinions on the protocol design are put forward according to the results of quantitative analysis.

2 Preliminaries

2.1 Related concepts

This subsection focuses on the background techniques to be used in formal verification of the nonrepudiation protocol that follows.

1. Fairness

Fairness is a very important factor because it has nothing to do with network size or complexity.The goal of fairness is to guarantee that benefits are distributed fairly among the participants in an activity(Zhao et al.，2016;Américo et al.，2018;Said and Cristescu， 2020). Informally， fairness means that at each step of the protocol，either both parties receive their expected items，or neither of them receives any valuable information about their expected items.

2. Distribution

For a finite setS， a discrete probability distribution overSis a functionf:S →{0，1}such that Σs∈S f(s)=1. Dist(S)is the set of all distributions over finite subsets ofS. The point distributionfmdenotes the distribution which assigns probability 1 tom. The support offdenoted by supp(f) is the set supp

3. Evaluation

Vis a certain set of variables，and each elementv ∈Vhas a specific domain Dom. The domain of the variables is restricted to integers， Boolean or bounded integers. A valuation ofVis a function val:V →∪v∈VDom， where val(v)∈Dom. The set of expressions over setVis denoted as Exprv. For an expressione ∈Exprvand a valuationv ∈V，the valuation of the expression is denoted by‖e‖v，where each occurrence of variablevis substituted by the value val(v)and the term is evaluated afterward.For a Boolean expression，‖ber‖ ∈{0，1}， where “0”for false and “1” for true. Given a variablexand a Boolean expression ber， denotex |= ber if and only if‖ber‖x= 1.

4. Clock restrictions

Clock restrictions are a special kind of variables that can model real-time behaviors. LetCbe a finite set of variables named clock which take values from R+(non-negative reals). A clock valuation is referred to as a pointv ∈RC. For a clock variablec ∈C，v(c) stands for the value ofvassigned toc.For anyv ∈RCandu ∈R+， the clock valuation defined asv(c)+uis denoted asu+v， which may represent the elapsed time. ForB ?C，letv[B:=0]denote the clock valuation gained fromvby resetting all clocks to 0. Given a finite set of clock variablesV， a clock restrictionτis defined inductively by the following syntax:

whereu，v ∈Vande，f ∈N. The set of all clock restrictions overVis denoted as CR(V). The clock valuationvsatisfies the restriction CR(V)， written asv∝CR(V)， if and only if CR(V) resolves to true after each clock valuev(c) fromvtakes the place of the corresponding clockc ∈C.

2.2 Probabilistic timed automaton (PTA)

Definition 1(Probabilistic timed automaton，PTA) A PTA is defined as a tuple (L，C， inv，PR， Lab)described as follows:

(1)Lis a finite set of locations;

(2)Cis a finite set of clock variables;

(3)inv:L →CR(C) is the invariant condition;

(4) PR?L×CR(C)×Dist(2C ×L) is a finite set of probabilistic edge relations;

(5) Lab:L →2APis a labeling function that assigns atomic propositions to locations， where AP is a finite set of action labels.

A state of a PTA is defined as a pair (l，c)∈L×RC， wherec∝inv(l).

2.3 Probabilistic timed computation tree logic(PTCTL)

The properties of a PTA can be specified by the probabilistic timed computation tree logic(PTCTL). Following timed computation tree logic(TCTL) (Henzinger et al.， 1994)，PTCTL uses a set of formula clocksZ，which are separate from clocksCof the PTA. Formula clocks are assigned values by a formula clock valuationδ ∈RZ. Timing restrictions are expressed using such clocks and the reset operator isz.φ. Similar to probabilistic computation tree logic(PCTL)(Hansson and Jonsson，1994)，PTCTL contains the probabilistic quantifierP～λ[·].

Definition 2(PTCTL) The syntax of PTCTL is defined as follows:φ::=true|a|ζ|z.φ|φ∧φ|?φ|P～p[φ ∪φ]， wherea ∈AP is an atomic proposition，ζ ∈CR(C ∪Z)，z ∈Z， “～”∈{＜，≤，＞，≥}， andp ∈[0，1].

3 Non-repudiation protocol

This section briefly describes the nonrepudiation protocol proposed by Markowitch and Roggeman(1999). As a kind of fair exchange protocol，a non-repudiation protocol guarantees that when the signature exchange over a network is complete，neither party can deny its participation in the process. If the protocol terminates successfully， it can provide each participant with evidence of commitment that cannot be denied by the other party. As illustrated in Fig. 1， this protocol can guarantee a fair exchange between the service provider，the originatorO， the service consumer，and the recipientR.Assume that an authentication process，which is useful in resolving possible disputes， is executed before the protocol.

The protocol starts whenRsends a request toOasking for a message. To prevent reply attacks，Rchooses dateDas time stamp along with the request. The message to be sent byOis divided intonfragments according to a geometric distribution with parameterp. The integernstands for the number of rounds it takes to send the message;i.e.，one fragment is transmitted in each round. In the remainder of this paper， the transmitted message fragment is called “message.” For the sake of fairness，nwill never be revealed to the recipient during the protocol execution.Ocomputesnfunctionsf1，f2，···，fn，which are parts of a function composition. They can help split the requested messageM:

The constitution operator “??” does not satisfy the commutative law to ensure thatRcannot obtain the requested message until the last messagef1(M1)has been received. At stepi， on receiving a request，Osends the encrypted messageMn-i+1toRand waits for the corresponding acknowledgement fromR. To ensure fairness and preventRfrom decoding the message， ifOdoes not receive an acknowledgement within a certain period， it will terminate the protocol and declare thatRis suspected of cheating.The chosen time limit AD must be greater than the time it takes forRto return an acknowledgement，but it ought to be less than the time required forRto decode the message. The messages encrypted by a participantPusing a private key are denoted asEyP(M). The encryption of messageMunder keyKis denoted as{M}K. The execution process of this protocol can be described as follows:

(1)Rselects dateDas the time stamp st;

(2)R →O:EyR(request，R，O， st)， the originator checks st then;

(3)O →R:EyO({M1}K，O，R， st);

(4)R →O:EyR(ack1);

(5)1-p:O →R:EyO({Mi}K，O，R， st);

(6)R →O:EyR(acki);

(7)ifi＜n，then goto step(4);

(8)p:O →R:EyO({Mn}K，O，R， st);

(9)R →O:EyR(ackn).

I tried to be invisible within a sea of faces. I wanted to run away. Disappear. Most of all I wanted no one to guess whose kid I was. I was betrayed by my last name, which began with the letter A, so I was the first graduate on the first row; Being a red-head gave me even more exposure, and the baccalaureate（） speaker, who had never met me, decided6 to use me as his audio-visual aid.

The notion “R →O: msg” means that a message msg is sent byRand received byO. At step(4)，Omakes a probabilistic choice to guaranteep=ε，whereεis a parameter used to maintain the fairness.Orandomly sendsRa piece of message with probability 1-p， wherepis a parameter of a geometric distribution. After receiving an acknowledgement message fromR，Ocontinues to send messages until the last one. At step (7)，Osends the last message encrypted byKwith probabilityp. On receiving the last acknowledgement，Oterminates the protocol correctly. One can assume that each acknowledgement may contain the following content“Rconfirms having received messageMi.” This can be implemented easily because each acknowledgement may contain a hash of messageMi.

According to the above description， the protocol should achieve the following informal nonrepudiation requirements:

1. Fairness

The originator’s non-repudiation is pledged by the messages it sent which are signed with the private key. The recipient’s non-repudiation is represented by the last acknowledgement， ackn. If the protocol can terminate afterOreceives ackn，both parties can obtain the expected information and the protocol is fair. If the protocol terminates because one party achieves the expected information while the other gains nothing， the protocol is unfair. If the protocol terminates afterOreceives acki(i/=n)，then neitherOnorRobtains the expected items and fairness is maintained. In brief， the protocol should guarantee that during execution，each party can obtain the expected information，or the probability that a malicious party can obtain the expected items while the other gains nothing should be no more thanε.

2. Time-limited

The network transmission delay can be ignored.The participants can always reach a point， within a certain period with probability 1， where they can terminate the protocol for the sake of fairness.

3. Determinacy

4. Tasks

The implementation of a non-repudiation service includes evidence generation， signature transmission and storage， authentication， dispute resolution，and a duration for each transaction.

5. Efficiency

This refers to the TTP’s degree of participation.The TTP may be non-existent，off-line，or on-line. In the on-line mode， the TTP fully participates in the execution of the protocol. In this mode， the TTP acts as a message delivery agent; all messages are passed through the TTP， thus creating a potential bottleneck， as proposed in the Zhou–Gollmann protocol (Zhou and Gollman， 1996). As an optimistic approach to fair exchange，proposed by Kremer and Markowitch(2000)and Kremer et al. (2002)， in off-line mode， the TTP simply monitors the execution of the protocol and appears only when there is repudiation to be resolved. As an improved scheme，non-repudiation protocols without TTP have been proposed (Markowitch and Roggeman， 1999; Cederquist et al.， 2005;Piramuthu， 2017).

There are other details about the original protocol that have no direct impact on modeling. Due to space constraints，they are omitted.

4 Modeling

In this section， according to the requirements of probabilistic model checking，the non-repudiation protocol described in Section 3 is modeled to verify the properties of the protocol.

4.1 Discussion

Both parties involved in the non-repudiation protocol exhibit probabilistic and non-deterministic behaviors that are time-related. Hence，the protocol should be modeled as PTA. To this end， we can use the following assumptions:

(1) Encryption scheme: Because the nonrepudiation properties to be verified depend on the number and order of messages that are exchanged，the results will be extracted from the encryption schemes used by the original protocol and the message exchanging process is simply modeled between the two involved parties.

(2) Transmission delay: Although the original protocol does not require communication channel quality of service (QoS)， the transmission delay should also be considered. If a packet is assumed to be delayed by a participant， it will not arrive at the other party’s location. One variable is used to represent the time cost of sending a message.

(3)TTP:The original protocol does not require a TTP. In this situation， the originator and the recipient are in an ad hoc pattern. The two involved parties should be modeled independently and have self-contained clocks.

(4) Shared variables: The involved parties have their own clocks，but some actions should be obeyed globally. To achieve this goal，the model should provide communal variables that represent the corresponding clock restraints， which can be accessed by the involved parties.

(5) The number of transmission rounds: The originator randomly chooses a numberr， which is the number of rounds it will take to send the message. According to the original protocol，robeys a geometric distribution of parameterp. This may lead to infinite steps， so for practical purposes， assume that the originator can set a maximum number of roundsrmax. The actual number of rounds should be min{r，rmax}.

(6) Parametrization: The formal model encapsulates as many behaviors as possible. One of the advantages of the model checking technique is that it can simulate the behaviors of the target system under actual scenarios by building a flexible model.Hence， the model should be flexible by parametrization. The parameters required by the model are summarized in Table 1.

Table 1 Parameter list

4.2 Honest recipient version

This subsection provides the model forOand an honest recipientR.Rstrictly follows the protocol. The originator， as shown in Fig. 2， is ready to send messages after initialization. Upon receiving a request，Obegins to send a message encrypted with keyKand waits for the acknowledgement sent byR.Then， at stateO2， with probability 1-p， it sends another encrypted message，sets the local clockxto zero， and reaches stateO1， and with probabilityp，it sends the last message containingKand reaches stateO3. Because the model does not describe the value that is passed， the actions are simply called“msg.” At stateO2， the expiration of the deadline for receiving an acknowledgement from the recipient is modeled by the action“stop” when the local clockxaffirms a value greater than AD. The protocol terminates fairly whenOreceives the acknowledgement for the last message. An unfair termination of the protocol is reached if and only ifOdoes not receive the acknowledgement within AD time units. In such a case，Oexecutes the action“stop.” The constraint AD is used to represent an estimate of the maximum transmission delay of an acknowledgement. Actions such as “init” in the model are treated as instant actions.

Fig. 2 An originator model

Fig. 3 shows the honest recipient model.Ris a passive participant. It starts the protocol by sending a request. After receiving a message， it reaches stateR2and begins to send an acknowledgement.It resets the local clockyto zero and goes back to stateR1to receive another message. Whenever it receives a message， it returns an acknowledgement.BecauseRbehaves honestly， it can always send an acknowledgement back within AD. The timetthat an acknowledgement requires to be sent back and a new message to be transmitted via the network may hold: ad≤t ＜AD.

The whole model which represents the protocol is defined asO||R， whereOandRsynchronize through the actions listed in the setA={req， msg，ack}. The protocol ends in a correct fair pattern whenOsends out the last message and receives the corresponding acknowledgemen; that is， the system reaches the state{O3，R1}. On one hand，if both parties behave correctly，the unfair case cannot appear.On the other hand， it is possible to find a malicious recipient who has received the expected information and denied that fact.

4.3 Malicious recipient version

This subsection considers two versions of the protocol where the recipient behaves maliciously.One is for a simple malicious recipient (SMR)R，where the recipient tries to guess which is the last message.Rsends an acknowledgement and decodes the received messages at the same time. However，the success condition is limited by whetherOsends the last message; that is， the probability of successful decoding isp. The decoding process needs to be completed within DECODE time units where DECODE＜AD so thatOwill not terminate the protocol or reportR’s malicious behaviors. Fig. 4 shows the model forR. The time necessary to decode a message is within the interval(0，DECODE].Due to its limited ability，Rcan decode the whole message if and only if it receives the last message with probabilityp，i.e.，as shown in Fig. 4，the transition from stateR3to stateR4. StateR4represents the state at whichRcorrectly decodes the whole message. Note that if DECODE＜AD，Rhas enough time to decipher the message. Moreover， it makes no sense forOto terminate the protocol because it did not receive the last acknowledgement when the recipient has already obtained the whole message. IfRfails to decode the last message with probability 1-p， it reaches stateR5and sends an acknowledgement toO. IfOhaskpackages to send， the probability of unfair action isP(x=k)=p(1-p)k-1.

Another version involves a more powerfulRwith a probabilistic encoder that can decode the message with probabilityqbeforeOtimes out. For this version，Rsends an acknowledgement and decodes the received message at the same time. BecauseR’s capability is enhanced，it does not need to wait for the last message to arrive; it can successfully decode a message in DC2with probabilityq. Or， after receiving the last message， it can decode the message correctly in DC1with probabilityp. Fig. 5 shows the model for the more powerful malicious recipient. The time necessary forRto decode the message probabilistically is DC2， which is less than AD. It takes DC1time units for the more powerfulRto decode the message successfully. For the sake of fairness， the protocol should choose a suitable AD so that AD＜DC1. This can guarantee thatRdoes not have enough time to decode the message during the execution of the protocol. To summarize，Rcan decode the message in DC1with probabilityp; it can also decode the message in DC2with probabilityq，where DC2＜DC1.

Fig. 3 An honest recipient model

Fig. 4 A simple malicious recipient (SMR) model

Fig. 5 A more powerful malicious recipient model

5 Fairness analysis

This section discusses， in detail， the fairness analysis of the non-repudiation protocol quantitatively. It provides the model of the protocol described in the PRISM language， discusses the properties described in the PCTL， and resolves the results of an experiment conducted with PRISM. The originator randomly selects the number of rounds according to the geometric distribution with parameterp. This may lead to an infinite loop. As a liveness property，termination indicates that the protocol session terminates as expected. This section first verifies the termination property and then checks the fairness if the protocol sessions can terminate.

5.1 Honest recipient

The behaviors of the originatorOand the honest recipientRare modeled in Figs.2 and 3，respectively.The corresponding PRISM codes for the models are as follows:

As illustrated in Fig. 2， the originator model has five states， represented byOi(i= 0，1，···，4).Similarly， for the recipient， variableRi(i= 0，1，2)indicates its state. Variablesxandyare local clock variables forOandR， respectively.

The invariant structure describes the clock invariants for each module in the PRISM model in terms of an expression. The restrictions imposed on the clock variables regulate the acceptable values， which rely on the other non-clock variable values. The clock invariants are usually used to describe each PTA location separately. The clock references must take the form of conjunctions of simple clock restrictions. That is， the simple expressions are of the formx ～corx ～y， wherexandyare clock variables，cis an integer-valued expression， and “～”∈{＜，≤，＞，≥，=}. In the model shown in Fig. 2，staying at locationO1，the local clockxmust satisfy the conditionx ≤0.

For the above participants，the honest recipient is a passive one，and it executes only a simple action loop of receiving a message and sending an acknowledgement back. The originator is in a dominant position;it can decide whether to terminate the protocol or not. When the protocol ends in a fair correct way，the originator arrives at locationO3. An honest recipient is in a completely passive position during the communication process. The termination of the protocol depends entirely on the originator， but the PTA model checking currently supports onlyPmin=?andPmax=?properties. The termination properties are described as follows:

When the originator sends the last message with probabilityp， the verification results of the termination probability are gathered in Table 2. The experimental results are calculated by PRISM without a rounding operation. The execution and termination are determined entirely by the originator. It can terminate the protocol when it receives the last acknowledgement. Based on the above analysis， the protocol can be terminated with probability 1 when there is no deception on the part of the recipient.For each value ofp，it takes the model checker 0.05 s to calculate the maximum and minimum probabilities. According to the experimental results， if the participants act according to the protocol strictly via a non-lossy channel，the protocol can terminate with probability 1.

Table 2 Termination probabilities

Table 3 The minimum and maximum probabilities for other values of p

As for a lossy channel， assume that the messages transmitted by the channel may be lost with probabilityploss. What impact will the channel QoS have on the protocol termination? The termination probabilities in three cases，whereptakes the values of 0.1，0.5，and 0.9 andplossvaries from 0.01 to 0.10，are shown in Fig. 6.

Fig. 6 Termination probability for a lossy channel

Fig. 7 Termination probability within T time units

The termination probability of a lossy channel is affected by two factors:pandploss. When the originator sends the last message with a lower probabilityp， the communication time will be prolonged compared with that in the case with a high probabilityp， because the protocol will not terminate until the originator receives the last acknowledgement.The actual situation caused by the decrease inpis that more packets are sent. Whenplossis certain and more packets are sent， more packets are lost. In this way， for the sameploss， the decrease inpleads to a decrease in the termination probability. Similarly，for the samep， with an increase inploss， the termination probability decreases. That is， the lower the value ofp， the longer the communication time and the lower the termination probability.

As can be concluded from the previous experiments， the protocol can terminate with probability 1 in an ideal case， but the duration of the termination changes with the change of probabilityp. As a further step， it is necessary to consider whether the protocol can terminate in a bounded period. The property that the protocol can successfully terminate withinTtime units can be described in PCTL specification as follows:

The trends of the minimum and maximum termination probabilities are plotted in Fig. 7，whereptakes the values of 0.01，0.05，and 0.10. Other experimental results about the minimum and maximum probabilities are listed in Table 3. Obviously，regardless of the maximum or minimum value， the termination probability increases with an increase in the protocol execution time. If the execution time is long enough， the difference between the maximum and minimum probabilities becomes smaller and smaller until it disappears completely. This is further confirmed by the experimental results. Moreover， the maximum and minimum termination probabilities increase with the increment ofp. The same conclusion is confirmed by the results in Table 3. An efficient way to reduce execution time is to increase the value ofp. If the originator splits the origin message intonpieces， the probabilitypthat a message is the last one isp= 1/n. That is， to increase the value ofp，the value ofnshould be reasonable.

For the lossy channel， as shown in Fig. 6， the termination probability is affected bypandploss. To study the influence of these two parameters on termination probability，it is assumed that parameterpis constant and thatplosschanges，and vice versa. The minimum and maximum termination probabilities inTtime units are shown in Fig. 8， whereploss=0.02，0.06，and 0.10 andp=0.25. The minimum termination probabilities in other circumstances are listed in Table 4. As the results show， with the increment of time， the termination probability slightly increases.Ifploss= 0.10， the termination probability cannot even exceed 0.3 within 100 time units whenp=0.10.As shown in Fig. 8， the termination probability， either the minimum or the maximum，increases asplossdecreases. Whenplossis lower than 0.05， the increment is more obvious. This shows that the protocol’s running time can be reduced by improving QoS of the communication channel. Moreover， as the existing experimental results show， both the maximum and the minimum probabilities increase rapidly within 40 time units， and then tend to be stable. One can therefore consider that the median execution time of the protocol is 40 time units.

Table 4 Minimum termination probability for other values of p and ploss

The situation wherepchanges whileplossis constant is also considered，and the experimental results are shown in Fig. 9， whereploss=0.01 andp=0.01，0.03， 0.05， and 0.10. Whenplossis invariant， the termination probability increases with the increase inp. In other words， for a certain period， improving the termination probability can be achieved by increasing the value ofp. This is consistent with the previous experimental conclusion of improving the termination probability for a non-lossy channel.In summary，to improve the termination probability in a limited execution period， one can increase the value of probabilitypor improve QoS of the communication channel.

5.2 Simple malicious recipient(SMR)

In addition to the termination property，a more important issue is to discover the probability that will allow the recipient to cheat the originator in different situations， or conversely， to determine the best originator strategy to maintain fairness. This subsection begins to consider fairness analysis for two versions of the protocol，where the recipient acts maliciously. In the first version， an SMR tries to decode the message on receiving it and sends an acknowledgement within AD time units. The behavior of the SMR is shown in Fig. 4 and the PRISM codes are as follows:

Fig. 8 Termination probability within T time units for lossy channels (p=0.25)

Fig. 9 Termination probability within T time units for lossy channels (ploss=0.01)

As illustrated in Fig. 4， SMR has six states.VariableRi(i= 0，1，···，5) stands for the SMR state. Variableyserves as the SMR’s local clock.At stateR2， the recipient tries to decode the message on receiving it and sends an acknowledgement to the originator within AD time units. Due to the limitation of the protocol， it is possible for the recipient to decode the message successfully only when it receives the last message. That is， the probability that it can decode the message isp， where DECODE=8＞AD=5.

The first property is to verify the maximum probability that the recipient can decode the message successfully. This means that in the SMR model， as shown in Fig. 4， there exists a path， starting from stateR0，by which the PTA can reach stateR4eventually. The property can be described in PCTL as

The recipient can decode the message only when it receives the last message with probabilityp， and the experimental results prove this fact， as shown in Fig. 10. The experimental results also demonstrate that the protocol isε-fair，whereε=p. To maintainε-fairness，the originator should allocate the number of packets reasonably and keep the number of packets secret. In essence， the recipient can decode the message and gain information by guessing whether the message is the last one. As can be expected， after calculation，the minimum probability is zero. So，only the maximum probability is discussed.

Fig. 10 Maximum probability

In practical applications， the actual situations are not always optimistic for the recipient. The recipient benefits from the fact that it can decode the message within a certain period， so the property is to verify the probability that the malicious recipient can decode the message withinTtime units. It can be described in the form of PCTL as follows:

For this version， whether the recipient can successfully decode the message totally depends on whether it has received the last message. The action of the recipient is just like extracting a specific fragment fromnfragments. This can be viewed as non-replacement sampling of finite samples in probability theory，which obeys hypergeometric distribution. Assume that there arenfragments to be sent;n-1 of them are normal fragments， and one is the last fragment. The probability that the last fragment is selected in theithround is 1/n. As shown in Fig. 11， the maximum probability of decoding a message remains constant after the arrival of the first message， because each message may be the last one and nothing can be achieved by waiting for a long time.

In the above experiments， it takes the recipient DECODE(＞AD)time units to decode the message.It seems that the probability of success totally depends on probabilityp. One may assume that the recipient is more powerful， which means that less time is required to decode the message. In the following experiment， DECODE is set to 4， which is less than AD.That is，the recipient has enough time to decode the message before sending an acknowledgement. Thus， fairness will be greatly damaged.It is necessary to verify the impact on the fairness of the protocol when the value of DECODE becomes smaller， where it reduces from 8 to 4. The experiment compares the maximum probabilities that the receiver can successfully decipher a message in DECODE time units whenp= 0.01 and 0.10. Fig. 12 shows the experimental results.

Fig. 11 Maximum probability that the message can be deciphered within T time units

Fig. 12 Maximum probability that the recipient can decipher the message in DECODE time units

DECODE is reduced from 8 to 4， while AD remains at 5，which means that the recipient has more time to decode a message. That is， the probability that the recipient can decode the message and obtain information increases sharply. This gives us an important insight; that is， to maintain fairness， one should fully consider the value of AD， to not only leave enough time for the recipient to send acknowledgements，but also prevent the recipient from being idle for a long time.

5.3 More powerful malicious recipient

This subsection considers a more powerful malicious recipient， which can invoke a method with probabilityqthat it can decode the message within DC2(DC2＜AD) time units. Moreover， it can decode the message correctly within DC1time units(DC1＞AD). The behaviors of this kind of recipient are shown in Fig.5 and the formal description in PRISM specification is as follows:

Because the recipient has become more powerful， the first property is to verify the maximum probability that the recipient can decode the message. This can be described in terms of PCTL as follows:

Fig. 13 shows the trends of the maximum probability that the recipient can decipher the message.The variation ofqfrom 0 to 1.0 represents the fact that the decoding ability of the recipient gradually improves. The probabilities for other cases are listed in Table 5. As the experimental results show， even if the recipient can decode the message within DC2time units， the probability is still subjected to parameterp.

With the incremental ability of the malicious recipient，can fairness be guaranteed? The probability that the recipient can decode the message withinTtime units can answer this question. To maintain consistency with the previous experiments(Fig.13)，the values ofpandqremain. Fig.14 shows the maximum probability that the recipient can decode the message withinTtime units.

As shown in Fig.14，the growth of the maximum probability is generally rapid within the interval[10，20]，while the growth tends to be steady in the interval [20， 100]. The time it takes to decipher the message probabilistically is DC2， which is far less than 20. Even after a longer period，the probability is still steady. Hence，one can draw a conclusion that if the recipient decodes a message successfully，the median time cost is 20 time units. According to the analysis of the experimental results in Fig. 13 and Table 5，the probability of successful decoding increases with the increase ofpand/orq. It is necessary to study the trend for the first 10 time units. The maximum probability whereT ∈[1，10]is shown in Fig.15. The maximum probability that the recipient can decode the message withinTtime units for other cases is listed in Table 6.

Fig. 13 Maximum probability that the recipient can decode the message as q varies

Based on the above experimental results shown in Fig. 14 and Table 6， one can conclude that whenT ∈[DC2， DC1)， the maximum probability is approximately equal top×q. To guarantee fairness，the most direct means is to reduce the probability.

Fig. 14 Trends of the maximum probability where T ∈[10， 100]

Fig. 15 Trends of the maximum probability whereT ∈[1， 10]

Table 5 Maximum probability for other certain cases

Table 6 Maximum termination probability for other cases of p

When the capacity of the receiver cannot be limited，the value ofpcan be reduced. Another way to guarantee fairness is to reduce the value of AD. If AD is far samller than DC2， it is almost impossible for the recipient to decode the message. Another important issue to be noted is that，as listed in Table 6，the maximum probability varies sharply whenTchanges from 7 to 10，no matter what valueqtakes. This fact shows that if AD is within 7， the probability that the recipient can decipher the message is reduced significantly.

5.4 Other issues

The parameterpused in the original protocol is the parameter of a geometric distribution. Some research， such as Aldini and Gorrieri (2002)， assumed that the originator can split the transmitted message following a Bernoulli distribution with parameterp.I do not think this is appropriate，because a Bernoulli distribution is a discrete probability distribution. It describes a random event that happens only once and may randomly yield two results. While the originator in the protocol is constantly sending messages， Bernoulli distribution describes only whether the message being sent is the last one or not， but cannot describe the sending behavior continuously.Moreover， the behavior cannot be described by then-fold Bernoulli distribution， that is， a binomial experiment， because if the originator sends the last message with probabilityp， it means the termination of the sending process. However， then-fold Bernoulli experiment allows the event to continue to occur with probability 1-p， which is obviously inconsistent with the actual behavior of the originator.The behavior of the originator is exactly consistent with the behavior described by the geometric distribution; that is， the firstk -1 experiments fail(sending normal messages)， and thekth(the last)experiment succeeds(sending the last message).

6 Conclusions

The non-repudiation protocol proposed by Markowitch and Roggeman (1999) provides a security solution for fair message exchange mechanisms.Related research focuses mainly on the design of nonrepudiation protocols，security analysis，and security guarantees. This paper focuses on a fairness analysis of this protocol. In the context of non-repudiation protocols， fairness means that during the execution of the protocol， either the participants obtain their excepted items， or the probability that one of the parties can obtain its expected items while the other gains nothing is smaller than a negligible thresholdε.

The non-repudiation protocol is probabilistic.Therefore，this paper uses probabilistic model checking to verify the fairness properties quantitatively using the PRISM model checker. I consider three versions of this protocol. The originator is considered honest and will always abide by the protocol.In the first version， both parties obey the protocol strictly. The second version involves a simple malicious recipient that guesses whether it has received the last message and tries to decipher the message.The last version involves a more powerful recipient that can decode the message probabilistically within the deadline for sending an acknowledgement， but also deciphers the message correctly within a certain period. The three versions are modeled as PTAs and translated into PRISM specifications.

In the first version， both parties abide by the protocol strictly and fairness can be guaranteed. Because the original protocol specifies that the parameterpobeys a geometric distribution， this may lead to an infinite loop. Therefore， this paper proposes to limit the number of transmitted messages in a reasonable range and focuses on verification of the termination property. Termination over a period is affected mainly by two factors: one is the probabilityp，and the other is the QoS of the communication channel. Experimental results show that the higher the value ofp，the higher the termination probability withinTtime units， and the better the QoS， the higher the termination probability.

For the malicious recipient version， when the recipient can decode the message by only guessing whether it is the last message， the probability of unfairness is determined by parameterp. We can further restrict the recipient’s idle time by setting the value of AD to ensure the fairness. The more powerful recipient can both decipher the message probabilistically within DC2with probabilityqand decode the message correctly in DC1. The maximum probability that the recipient can decode the message is approximately equal top×qduring the periodT ∈[DC2，DC1). When the computing power of the recipient cannot be limited and the probabilitypis not changed，we can maintain fairness by setting the value of AD so that it cannot exceed 7 and is far smaller than DC2.

With the increase of computing power，both the originator and the recipient may infer the possible behaviors of the other party based on historical data and make corresponding decisions accordingly. Because both the originator and the recipient have the ability to think， modeling for both parties and analyzing relevant attributes are possible future work.

To prevent an infinite execution loop，this paper assumes that the upper bound of message transmission cannot exceedrmax. This is a safety hazard. If the maximum number of steps is known or deduced by the recipient， it knows the information when the maximum number of steps is reached during an execution of the protocol. Therefore， it can refuse to acknowledge receipt of the encrypted message and break fairness with probability 1. In the future work a better scheme will be discussed for the originator to determine the number of steps in the protocol.

Compliance with ethics guidelines

Xu GUO declares that he has no conflict of interest.