1
Novel Logical Method for Security Analysis of Electronic Payment Protocols
Yi Liu
a
, Xingtong Liu
a
, Lei Zhang
a
, Jian Wang
a
and Chaojing Tang
a
a
College of Electronic Science and Engineering, National University of Defense
Technology, No.47, Yanwachi street, 410073 Changsha, Hunan, China
Abstract
Electronic payment protocols play a vital role in electronic commerce security, which
is essential for secure operation of electronic commerce activities. Formal method is an
effective way to verify the security of protocols. But current formal method lacks the
description and analysis of timeliness in electronic payment protocols. In order to
improve analysis ability, a novel approach to analyze security properties such as
accountability, fairness and timeliness in electronic payment protocols is proposed in
this paper. This approach extends an existing logical method by adding a concise time
expression and analysis method. It enables to describe the event time, and extends the
time characteristics of logical inference rules. We analyzed the Netbill protocol with the
new approach and found that the fairness of the protocol is not satisfied, due to
timeliness problem. The result illustrates the new approach is able to analyze the key
properties of electronic payment protocols. Furthermore, the new approach can be
introduced to analyze other time properties of cryptographic protocols.
Keywords: electronic payment protocol; formal analysis; accountability; fairness;
timeliness; logic reasoning;
2
1. Introduction
In recent years, an explosion of services provided over the Internet has a great
importance of human daily life. These services are increasingly transferring customers’
private and financial information over the network. A novel proof methodology to
verify secure routing protocols has been proposed by Chen (Chen et al. 2015). Another
category of network protocols to protect legitimate interests between traders also need
to be verified with additional security properties. Electronic payment protocols provide
technical assurance for security of electronic commerce. Sensitive information such as
credit card numbers and password depends on the security of electronic payment
protocols. The analysis and research on the security of electronic payment protocols has
become an important issue in the field of information security (Patrick et al. 2016).
Compared with other security protocols, accountability, fairness and timeliness are
additional security properties in electronic payment protocols. Accountability can
provide sufficient evidence to resolve possible future disputes after the execution of
protocol. It means that all parties cannot repudiate what they have done. Fairness
ensures that no one can gain an advantage over other participants by misbehaving,
which means either both the participants receive what they expect or nothing.
Timeliness provides constraint of intervals during every step in protocol regulation to
avoid the time difference utilizing by attackers.
Formal analysis is an effective method to verify electronic payment protocols thanks
to its strict and effective characteristics. But current formal methods for analysis of
electronic payment protocols lack the description and analysis of timeliness. Our
approach focuses on the description and analysis of three security properties above. We
add concise time expression and analysis method to existing logical method. The logic
3
reasoning part in the process of the objective proof is based on Qin-Zhou logic method
(Qing 2005; Zhou et al. 2001), and the time calculus part utilizes the method of algebra
and set theory. The logical method and the algebraic method are two independent parts.
They will not interfere with each other or undermine the correctness of the original
method. The Netbill protocol is analysed with the our method, and the result shows that
the protocol does not satisfy fairness due to timeliness problem. Then we elaborated that
the defect can be fixed with careful specification of event time and waiting time.
The rest of this paper is organized as follows. Section 2 introduces related work in
this area. Section 3 describes the concepts and definitions of the novel logical method.
The logic analysis procedure is introduced in Section 4. The analysis process of the
Netbill protocol is illustrated in Section 5. Section 6 concludes this paper and outlines
our future studies.
2. Related work
Formal methods have already been used for security analysis of electronic payment
protocols for decades (Kailar 1996). They can be divided into three categories as logic
reasoning, model checking and theorem proving.
2.1 Logic reasoning
Logic reasoning is an important formal analysis method of electronic payment
protocols up to present. Kailar logic (Kailar 1996) is the first analysis method designed
for electronic payment protocols, which is mainly used to analyse accountability. But it
ignored fairness in electronic payment protocols. Volker extended Autlog logic to be
able to analyse accountability (Volker and Heike 1998). The famous Payword and SET
protocol are analysed as examples. Qing-Zhou logic was proposed for the analysis of
accountability and fairness together (Qing 2005; Zhou et al. 2001). Li added the time
4
factor in SVO logic to make it able to analyse the timeliness of protocols (Li and Luo
2006). Wen put forward a modeling and analysis method of electronic payment
protocols based on game logic (Wen et al. 2007). Chen combined logic reasoning with
strand space model, introducing a new logic analysis method of electronic payment
protocols (Chen 2010). A method applying Kailar logic in compositional analysis is
presented by Gao for analysing the accountability and fairness of electronic payment
protocols (Gao et al. 2013).
2.2 Model checking
The characteristic of model checking is easy to manipulate. Kremer apply model-
checker MOCHA which supports the alternating transition systems and the alternating
temporal logic to analyse accountability (Steve 2004). Xie utilized finite automaton to
analyse ISI protocol and IBS protocol (Xie and Zhang 2004). Guo combined
communication finite state machine with some new logic rules based on Qing-Zhou
logic to analyse security properties of electronic payment protocols (Guo et al. 2010).
Liu proposed an extended deterministic finite automaton which can also analyse
security properties such as accountability and fairness (Liu et al. 2013). Nevertheless,
due to the state space of the model checking method is limited, even if no attack method
has been found, it does not mean the correctness of protocols.
2.3 Theorem proving
Theorem proving is regarded as an accurate method for security of cryptographic
protocols. Papa integrated logic with process calculi for analysing electronic payment
protocols (Papa et al. 2001). Chun used Coloured Petri Nets to analyze the Internet
Open Trading Protocol (Chun and Jonathan 2004). Bella analysed the purchase protocol
of SET with Isabelle and the inductive method (Giampaolo et al. 2006). Guttman
5
applied strand space method to analyse the fairness of fair exchange protocols (Guttman
2012). Guo proposed a technique for modelling and verifying fair-change electronic
payment protocols (Guo et al. 2009). On the other hand, theorem proving method is
complicated and difficult to verify complex protocols.
3. Concepts and definitions
The definitions and symbols used in the new approach are denoted as follows:
Table 1. Basic symbols
A,B
Parties participate in protocol.
{}
K
m
Ciphertext of message m
encrypted with secret key K.
TTP
Trusted third party.
K
Dual key of K.
m
Message transferred in protocol.
(m, n)
Message m is combined with
message n.
a
K
The public key of party A, which
is used to verify the digital
signature of A.
1
a
K
The private key corresponding to
a
K
.
EOO
The non-repudiation evidence that
is provided to the receiver in
electronic payment protocols,
which is used to prove that the
sender has sent the message.
EOR
The non-repudiation evidence
that is provided to the sender in
electronic payment protocols,
which is used to prove that the
receiver has received the
message.
T
Time of event.
3.1 Time system
We denote the time when event occurs by adding a condition in the formula language,
like
Am
at T. T is a time expression. This definition introduced the description of
the occurrence time of sending and receiving message.
The time expression is defined as follows:
1. x stands for a constant time element.
2. X stands for a variable time element.
3. X|TS means a time binding expression, while TS is the scope of X.
4. [T] is time expression, while T is a time binding expression.
6
The constant time element is represented by a lower case t, and the variant time
element is represented by a capital letter T. Time binding expression is a variable time
element X with a certain value of constant time element as
()t t TS
. In logical formula,
the time expression [X|I] can be abbreviated to [X], and [X|{x}] can be abbreviated to [x],
where x is a constant time element or a variable time element with bound value. The
value of a variable time element is bound to the first operation in its formula.
3.2 Protocol and environment
TTP(Trusted third party) is a special party, which is regarded as a fair trusted third
party. The bank or the arbitration organization can act as TTP. In general, we assume
that all parties are dishonest except for TTP. They may interrupt the execution of
protocols arbitrarily.
Communication channel is either reliable or unreliable, depending on the specific
operating environment. Usually, the communication channel between general parties is
unreliable, while it between the TTP and other parties is recoverable which means the
message will be transmitted eventually.
Protocol statement defines what message should be sent and received by parties in the
current round as follows:
:A B m
at T means A sent message m to B at T.
3.3 Possession set
a
O
stands for the possession set of party A participating in protocol. Assuming the
protocol begins from
0
T
, the initial possession set of A is
0
()
a
OT
. When protocol runs to
x
T
, the possession set of A becomes
()
ax
OT
. Besides, we define
()
ae
OT
is the final
possession set of A at the end of protocol. The possession set of A contains the
7
information inherited from last step and the message which is received or generated at
present. It varies consecutively with the execution of protocol until
()
a a e
O O T
.
The possession set of A changes from
()
ay
OT
to
()
ax
OT
∩
x
()
y
TT
, which means
y
T
is the moment before
x
T
. It follows the following rules:
(1) When the execution of protocol statement is
:A B m
at
x
T
,
( ) ( ) { }
a x a y
O T O T m
if m is a new message generated by A, which means
()
ay
m O T
.
Otherwise,
( ) ( )
a x a y
O T O T
if m is not a new message generated by A and
()
ay
m O T
.
(2) When the execution of protocol statement is
:B A m
at
x
T
while
()
ay
m O T
,
( ) ( ) { }
a x a y
O T O T m
. Otherwise,
( ) ( )
a x a y
O T O T
.
4. Logic analysis method
4.1 Logic component
Our method consists of the following five logic components:
(1)
Ax
. A can make others believe in formula x by performing a series of
operations without leaking any secret;
(2)
Am
at T. A sends message m at T. The following implication is established in
the process of analysis:
( , )A m n
at T =>
Am
at T (1)
It means, A sends message m at T while A sends message (m, n) at T.
(3)
Am
. A possesses message m.
(4)
Am
at T. A received message m at T. The following implication is established
as the second component:
( , )A m n
at T =>
Am
at T (2)
8
(5)
a
K
A
.
a
K
is the public key of A, which is used to verify the message signed
by its private key
1
a
K
.
4.2 Axiom system
The axiom system consists of 1 inference rule and 6 axioms. The inference rule is as
follows:
(├
)∩ (├
()
) =>├
(3)
It illustrates ├
can be obtained from ├
and ├
()
.
├
represents
can
be deduced from the formula sets
. ├
indicates
is a theorem, which means
is
established all the time. The inference rule above indicates that
is theorem if
is
theorem and
contains
.
The 6 axioms are as follows:
A1.
Ax
∩
Ay
=>
()A x y
A2.
Ax
∩(x=>y) =>
Ay
A3.
1
{}
b
K
Am
at
x
T
∩
b
K
AB
at
x
T
=>
A B m
at
[ | ]
Y Y X
T T T
A4.
{}
k
A B m
at
x
T
∩
A B k
at
Y
T
=>
A B m
at
max( , )
XY
TT
A5.
Am
at T =>
Am
at T
A6.
{}
K
Am
at T∩
AK
=>
Am
at T
The proof procedure of protocol properties is divided into two parts. The first part is
called logical reasoning and the second part is called time calculus. The purpose of this
procedure is to prove that the result obtained from logic reasoning satisfies the time
constraints specified in time calculus.
4.3 Protocol analysis procedure
Protocol analysis consists of 5 steps as shown in Figure 1.
9
（1）List the initial possession sets of each party in protocol.
（2）List the initial Assumptions of the protocol.
（3）List EOO and EOR, and analyse whether they meet the
requirement of accountability.
（4）Analyse whether ∩ is set
up at the end of protocol.
()
be
EOO O T
()
ae
EOR O T
（5）Analyse whether if and only if
at the end .
()
be
EOO O T
()
ae
EOR O T
e
T
Figure 1. Procedure of protocol analysis
5. The Netbill Protocol analysis
The Netbill protocol is an electronic payment protocol proposed by Professor
J.D.Tygar in Carnegie Mellon University for trading digital goods, including three
participants: customer, merchant and the Netbill server (Sirbu and Tygar 1995). Its main
steps are as follows:
(1)
: ( ),{ , }
CM
CM K
C M T C PRD TID
at
1
T
(2)
:{ , , }
CM
K
M C ProductID Price TID
at
2
T
(3)
: ( ),{ }
CM
CM K
C M T C TID
at
3
T
(4)
:{ } ,{ ({ } ), }
CM
k k K
M C Goods h Goods EPOID
at
4
T
(5)
1
: ( ),{{ } }
CM
C
CM K
K
C M T C EPO
at
5
T
(6)
11
: ( ),{{{ } , , } }
MN
CM
MN K
KK
M N T M EPO MAcct k
at
6
T
(7)
1
:{{ } ,{ , } }
CN MN
N
KK
K
N M Receipt EPOID CAcct
at
7
T
(8)
1
:{{ } ,{ , } }
CN CM
N
KK
K
M C Receipt EPOID CAcct
at
8
T
10
C, M and N represent the customer, the merchant and the Netbill server respectively.
()
CM
TC
is used to prove C to M, and to establish a shared session key
CM
K
. The
function of
()
MN
TM
is similar to
()
CM
TC
. PRD(Product Request Data) is product
request data. TID is transaction’s ID and ProductID is product’s ID. Price stands for the
price the merchant required. Goods is the specific content of transmitted goods. EPO is
a electronic purchase order, the plain part of which comprises customer identification
identity, ProductID, Price, M,
({ } )
k
h Goods
and h(PRD). h(m) stands for the hash value of
m. The encryption part includes a payment instruction which can only be read by the
Netbill server such as the customer account. EPOID is electronic payment ID, which is
the globally unique identifier and will be used to uniquely identify the transaction in the
database of Netbill. CAcct and MAcct stand for the customer and merchant’s account
respectively. Receipt includes the Result whether to accept this payment or not, which is
returned from the Netbill server.
The analysis procedure of the Netbill protocol is detailed in the next subsection.
5.1 List the initial possession sets.
At the initial time of protocol operation, the initial states of C and M are
1
0
( ) { , , , , , }
C C C M N CM CN
O T K K K K K K
1
0
( ) { , , , , , }
M M M C N CM MN
O T K K K K K K
( , , , )
N CM CN
M
K K K
K
C M N C M C N
( , , , )
C N CM MN
K K K K
M C N C M M N
5.2 List the credible assumptions
T1:
A N k A B k
Assume that the Netbill server is fully in accordance with the protocol regulation and
will not do anything harmful to any party. If A can prove that N has sent k to him, he
can prove that the other party B has sent k.
11
T2:
()A B h m A B m
According to the protocol, the sender sends h(m) for the checksum of message m. The
sender is able to calculate the checksum only when the sender owns the message m. So
if A can prove that B has sent h(m), then A can prove that B has sent message m.
5.3 List EOO and EOR:
1
= { ({ } )} { }
CM
N
kK
K
EOO h Goods k
（ ， ）
11
= { ({ } )} { }
CN
k
KK
EOR h Goods k
（ ， ）
Assume that
()
Ce
EOO O T
is established at the end of protocol. Then
1
{ ({ } )} { } ( )
CM
N
k K C e
K
h Goods k O T
（ ， ）
is satisfied, which means
{ ({ } )}
CM
kK
C h Goods
at
e
T
and
1
{}
N
K
Ck
at
e
T
.
Since
{ ({ } )}
CM
kK
C h Goods
at
e
T
,
CM
K
C C M
and axiom A3, then
({ } )
k
C M h Goods
at
[ | ]
e
T T T
. According to T2, we obtain
{}
k
C M Goods
at
[ | ]
e
T T T
(4)
Since
1
{}
N
K
Ck
at
e
T
,
N
K
CN
and axiom A3,then
C N k
at
[ | ]
e
T T T
.
According to the credible assumption T1, we obtain
C M k
at
[ | ]
e
T T T
(5)
Due to formula (4), (5) and axiom A4, we will get
C M Goods
at
max( , )TT
∩
[ | ]
e
T T T
∩
[ | ]
e
T T T
(6)
Assume that
()
Me
EOR O T
is satisfied at the end of the protocol, which means
1
{ ({ } )}
C
k
K
M h Goods
at
e
T
and
1
{}
N
K
Mk
at
e
T
are satisfied. Then according to
N
K
MN
, axiom A3 and credible assumption T1, we obtain
12
M C k
at
[ | ]
e
T T T
(7)
Since
C
K
MC
, axiom A3 and credible assumption T2, we will get
{}
k
M C Goods
at
[ | ]
e
T T T
. Due to formula (7) and axiom A6, we will get
M C Goods
at
max( , )TT
∩
[ | ]
e
T T T
∩
[ | ]
e
T T T
(8)
Therefore, the design of EOO and EOR in the Netbill protocol can meet the
requirement of accountability.
5.4 Analysis of accountability
Verify whether C and M can obtain the appropriate evidence at the end of protocol.
After the fourth step of the protocol,
43
( ) ( ) { ({ } )}
CM
C C k K
O T O T h Goods
∩
44
[ | ]
e
T T T
, then
{ ({ } )} ( )
CM
k K C e
h Goods O T
.
When the last step of the protocol is finished,
1
87
( ) ( ) {{ } }
CM
N
C C K
K
O T O T Receipt
∩
88
[ | ]
e
T T T
. Because of
CM
CK
, we obtain
1
{ } ( )
N
Ce
K
Receipt O T
, and
1
{ } ( )
N
Ce
K
k O T
. Then
()
Ce
EOO O T
is satisfied.
Similarly, according to the fifth step of the protocol, we will get
1
{ ({ } )} ( )
C
k M e
K
h Goods O T
. And
1
{ } ( )
N
Me
K
k O T
will be obtained after the seventh
step. Then we will get
()
Me
EOR O T
.
Therefore,
()
Ce
EOO O T
∩
()
Me
EOR O T
is satisfied when the protocol finishes.
(5)Analysis of fairness
The fairness objective is:
()
Ck
EOO O T
if and only if
()
Mk
EOR O T
All parties in protocol will wait for the next step after the last one. If there is no
response, the protocol will terminate after a certain period of time t and clear the
13
protocol records before. For achieving fairness, the following conditions have to be
satisfied:
1
{{ } }
MN
M
K
K
Mk
at
x
T
∩
1
{}
N
K
Mk
at
y
T
∩
x y x M
T T T t （ ）
(9)
1
{ ({ } )}
C
k
K
C h Goods
at
x
T
∩
1
{}
N
K
Ck
at
y
T
∩
x y x C
T T T t （ ）
(10)
M
t
is the waiting time after the M executes the 6th step of the protocol.
C
t
is the
waiting time after C executes the 5th step. Since N is in full accordance with the
regulation of protocol, formula (9) must be established.
In formula (10),
5
=
x
TT
,
7 5 5 6
=
y
T T T t t
,
5
t
and
6
t
are the time delay after the 5th
step and the 6th step. So we must make
56C
t t t
to make formula (10) established.
But there is no restrict about the relationship among
5
t
,
6
t
and
C
t
. There is a possibility
to make
56 C
t t t
no matter what the constant
C
t
is specified. For example, if C
performs the 5th step in accordance with the regulation, M could send
1
{{ } }
MN
C
K
K
EPO
to
N after it is timeout and acquire the evidence to prove C has received the product Goods.
But C has deleted
{}
k
Goods
because of timeout. Even though C has received Receipt
and the key k, he couldn’t decrypt the ciphertext to obtain the product Goods.
Then the fomula (10) can’t be established, which means the protocol can’t achieve
the fairness objective. The main reason is that the implementation of the protocol does
not have specific constraints on the relevant event time in the process. In order to make
up for the defect, we should carefully regulate the event time and the waiting time of the
execution of protocol.
5 Conclusion
The analysis result of Netbill protocol show that the protocol does not satisfy fairness
because of timeliness problem. The process illustrates how the new approach is applied
14
to analyse the temporal relation between events in electronic payment protocols. It is not
a simple logic method, but an integrated approach. The new approach is appropriate to
guide the design of electronic payment protocols and fix the defects of original
protocols.
The next step of our research is to analyse other electronic payment protocols with
our method which are widely used in electronic commerce. At the same time, we will
further study automated analysis tools to make it convenient for design and analysis of
electronic payment protocols.
Acknowledgements
This work was sponsored by the National Natural Science Foundation of China
(Project No. 61601476).
References
Chun, O., Jonathan, B., 2004. An Improved Formal Specification of the Internet Open
Trading Protocol. In: Proceedings of the 2004 ACM symposium on Applied
computing. Nicosia, Cyprus. 779-783.
Chen, L., 2010. New Logic of Analyzing Electronic Commerce Security Protocols.
Computer Science 37 (10), 110-115.
Chen, C., Jia, L., Xu, Hao., Luo, C., Zhou, W., Loo, B., 2015. A Program Logic for
Verifying Secure Routing Protocols. Logical Methods in Computer Science 11 (4),
1-34.
Giampaolo, B., Fabio, M., Lawrence, C.P., 2006. Verifying the SET Purchase Protocols.
Journal of Automated Reasoning 36 (2), 5-37.
Guo, Y., Ding, L., Zhou, Y., Guo, L., 2009. Analysis for E-commerce Protocols Based on
ProVerif. Journal on Communications 30 (3), 125-129.
15
Guo, H., Li, Z., Zhuang, L., Ji, H., 2010. New Approach for Analyzing of E-commerce Protocol.
Computer Science 37 (8), 56-60.
Guttman, J.D., 2012. State and Progress in Strand Spaces: Proving Fair Exchange.
Journal of Automated Reasoning. 46-60.
Gao, Y., Peng D., Tang, P., 2013. A Formal Analysis Method for Optimistic Fair
Exchange Protocol. Journal of Convergence Information Technology 8 (3), 35-46.
Kailar, R., 1996. Accountability in electronic payment protocols. IEEE Transaction on
Software Engineering 22 (5), 313-328.
Steve, K., 2004. Formal Analysis of Optimistic Fair Exchange Protocols. Universite
Libre de Bruxelles, Brussels, Belgium.
Sirbu, M., Tygar, J., 1995. NetBill: an internet commerce system optimized for network
delivered services. IEEE Personal Communications 2 (4), 34-39.
Li, B., Luo, J., 2006. Formal Analysis of Timeliness in Non-Repudiation Protocols. Journal of
Software 17 (7), 1510-1516.
Liu, W., Ma, S., Si, Y., H, G., 2013. A Combining Deterministic Finite Automaton with Logic
Rules Approach for Analyzing of E-commerce Protocol. Journal of Chinese Computer
Systems 34 (3), 492-497.
Papa, M., Bremer, O., Hale, J., Shenoi, S., 2001. Formal Analysis of E-Commerce Protocols. In:
Proceedings of the 5th International Symposium on Autonomous Decentralized Systems.
19-28.
Patrick, M., Siamak, F.S., Feng, H., 2016. Refund attacks on Bitcoin's Payment Protocol.
In: Proceedings of the 20th Financial Cryptography and Data Security. Barbados.
Qing, S., 2005. A Formal Method for Analyzing Electronic payment protocols. Journal
of Software 16 (10), 1758-1765.
16
Volker, K., Heike, N., 1998. A Sound Logic for Analysing Electronic payment
protocols. In: the 5th European Symposium on Research in Computer Security
Louvain-la-Neuve. Berlin, Heidelberg. 345-360.
Wen, J., Zhang, M., Zhang, H., 2007. Formal Analysis of Electronic Payment Protocols
Based on Game Logic. Microelectronics Computer 24 (9), 113-115.
Xie, X., Zhang, H., 2004. Fairness Research of Electronic Commerce Paying Protocols
Based on Finite Automaton Model. Computer Applications 24 (6), 13-18.
Zhou, D., Qing, S., Zhou Z., 2001. A new approach for the analysis of electronic payment
protocols. Journal of Software 12 (9), 1318-1328.
