1 Introduction
NetBill[
1,
2] enables sales of information goods deliverable over the network. It has very low transaction costs for micro-payments (around 1 cent for a 10 cent item), protects the privacy of the transaction, which make it suitable to Peer to Peer commerce transaction. The key security goal of NetBill is certified delivery, which implies: 1) the transfer of funds from one party to another without the possibility of the creation or destruction of money; 2) an exact transfer of goods for money; 3) both a merchant and a customer to prove exactly which goods were delivered.
NetBill deserves to be analyzed formally because it is one of the most important infrastructures in electronic commerce and also subject to subtle errors. Therefore, there have been many attempts to apply formal methods to analyses of NetBill. [
5] verified all honest participants protection properties using theory proving techniques. [
6] verified the reliability of the protocol using finite-state model checker SPIN. Both two methods were limited to a single protocol run, so they may fail to find some attacks on the protocol.
In this paper NetBill is analyzed with the APA/SHVT method as follows. NetBill is modeled as an APA and verified with SHVT [
9]. Compared to previous approaches, we present an attack on it, that, to our knowledge, has not been published before. To prevent the attack we propose an improved version of the protocol.
This paper is organized as follows. Section 2 describes the NetBill protocol. Section 3 explains our approach to automated protocol analysis. Section 4 describes possible attacks on the protocol and suggests an improvement. Section 5 concludes this paper.
2 NetBill
NetBill involves three parties: the customer, the merchant and the NetBill transaction server. A transaction involves three phases: price negotiation, goods delivery, and payment. In this paper we will assume that the customer and the merchant have negotiated a price for the goods, and restrict our attention to just the last two phases. Since NetBill relies on secure communication channels which are guaranteed by the Kerberos protocol, we hide the information about Kerberos ticket and encryption. We also hide some unnecessary quantities that are supposed to be irrelevant to what we are interested in.
We show the simplified protocol in
Fig.1.
C,
M and
N stand for a customer, a merchant and a NetBill server, respectively. Request, EncGoods, Payment, Endorse, Result and Forward are tags of messages.
Cryptographic primitives used in the protocol as follows:
-CC (Message) : A cryptographic checksum of Message using a hash function.
-Ek (Message) : Message, encrypted with a symmetric key K. The key K may
-[Message]X : Message, signed by X with his private key. It includes Message and the signature of Message.
Quantities occurring in the protocols as follows:
-Goods : Information goods C purchase.
-K : Symmetric key generated by M to encrypt Goods.
-TID : Transaction ID, It is not globally unique and used only by C and M to maintain context between them.
-EPOID : Payment ID that is globally unique.
-CAcct : C's NetBill account number.
-MAcct:M 's NetBill account number.
-result, transferred: binary values indicating respectively whether a transaction yielded a successful result and whether any funds have been transferred.
Composite fields used in the protocols as follows:
-EPO:C,M,CC(EK( Goods )),EK( Goods ),EPOID,ECN(CAcct)
-Receipt: C,M,K,EPOID,result,transferred
We are about to describe how the simplified NetBill works.
-Request: C requests M to deliver the goods by supplying Transaction ID, or TID used in the price request phase.
-EncGoods: On receipt of Request, M generates a unique symmetric cipher key K, encrypts the goods using this key and sends the encrypted goods to C, along with a cryptographic checksum computed on the encrypted goods. He also sends an Electronic Payment Order ID, or EPOID, with the keys.
-Payment: On receipt of EncGoods, C submits payment to M in the form of a signed Electronic Payment Order, or EPO, which is tied to EPOID.
-Endorse: On receipt of Payment, M verifies the signature. He endorses EPO and forwards the endorsed EPO to N. The endorsed EPO adds 's account number and the decryption key K.
-Result: On receipt of Endorse, N verifies the two signatures, checks CAcct is 's account number, the account balance is enough to pay, etc. and EPOID is fresh and unique. If so, N credits some amount to M and debits the amount against C. Then it issues a receipt containing the EPOID, the key K needed to decrypt the goods, the identities of the parties, etc. The receipt is digitally signed by N.
-Forward: On receipt of Result, M forward the message result to C.
We specify the key security goal relatives to the role in the protocol. The security goal of the customer has to be satisfied in all scenarios where the customer acts in accordance with the protocol specification while the merchant may act maliciously, and vice versa.
We show here how the main security goals that an exchange protocol must fulfill. Informally, the protocol ensures for customer C that if C behaves correctly, then the other party M cannot get the item of C unless C gets the item of M and vice versa.
Definition 1 (C's security goal PC ). If M is entitled to a payment, then C is guaranteed the goods.
Definition 2 (M's security goal PM ). If C is guaranteed the goods, then M is entitled to a payment.
In Def. 1 and 2, M is entitled to a payment if and only if
M1 : he has proof that C received the goods, or
M2 : he has proof that N committed the transaction a) with a successful result, and b) and did so in response to a valid request.
And C is guaranteed the goods if and only if
C1 : she actually receives the goods during the protocol execution, or
C2 : she can claim the goods in court.
3 APA model of NetBill
In our model we make abstraction of the protocol and give some assumptions. An asynchronous product automaton (APA) is a universal and very flexible operational description concept for cooperating systems. It is supported by the SH verification tool (SHVT) that provides components for the complete cycle from formal specification to exhaustive analysis and verification. An APA can be seen as a family of elementary automata. The set of all possible states of the whole APA is structured as a product set. Different elementary automata can "communicate" by changing the content of shared state components. We view protocols as cooperating systems, thus APA is an adequate means for protocol formalization.
Fig.2. shows the structure of an APA of NetBill including protocol agents
C,
M and
N. The circles represent state components and boxes are elementary automata. Each agent
P taking part in the protocol is modeled by one elementary automaton
P that performs the agent's actions, and four state components Symkeys, Asymkeys,
States and Goals to store the symmetric and asymmetric keys of.P 's locate state and security goals P should reach within the protocol respectively. The only state component shared between all agents (all elementary automata) is the component Network, which is used for communication. A message is sent by adding it to the content of Network and received by removing it from network. The neighborhood relation (graphically represented by an arc) indicates which state components are included in the state of an elementary automaton and may be changed by a state transition. For example, automaton C may change States C and Network but cannot read or change the state of StatesM. The full specification of the APA includes the state sets (the data types), the transition relations of the elementary automata and the security goals and the initial state, which we will explain in the following paragraphs.
3.1 State sets
Here a state set indicates the domains of the state component. For the definition of a state set we need the following basic sets :
-$\mathbb{N}$ : set of natural names
-Agents: set of agents names
-Keynames: set of constants to name keys. Agents $\subseteq $ Keynames
-Keywords: {start, respond, agent, server}
-Symflags: {sym,··· }
-Asymflags: {pub, priv, ··· }
-Nonces: set of nonces(numbers that have never been used before)
-Keys: $\left\{\right(\mathit{w},\mathit{f},\mathit{n})-\mathit{w}\in $ Keynames, $\mathit{f}\in $ Symflags $\cup $ Asymflags, $\mathit{n}\in \mathbb{N}\}$
-Predicates: set of predicates on global states
It is helpful to include the agents' name in the set Keynames in order to be able to formalize, for example, the public key of agent P by " (P, pub,$\mathit{n}\left)\right(\mathit{n}\in \mathbb{N})$ ". "pub" indicates its type and the third key component allows to use more than one key with the same name and type. The key K for example in the first run of NetBill can be formalized by (K,sym,1), the key of the next run by (K,sym,2), and so on.
The union of the sets Agents, N, Nonces, Keywords and Keys is the set of atomic messages, and we construct a set M of messages in the following way:
-Every atomic message is an element of M.
-If ${\mathit{m}}_{1},\cdots,{\mathit{m}}_{\mathit{r}}\in \mathit{M}$, then $\left({\mathit{m}}_{1},\cdots,{\mathit{m}}_{\mathrm{r}}\right)\in \mathit{M}$.
-If $\mathit{k},\mathit{m}\in \mathit{M}$, then $\mathrm{e}\mathrm{n}\mathrm{c}(\mathit{k},\mathit{m}),\mathrm{d}\mathrm{e}\mathrm{c}(\mathit{k},\mathit{m}),\mathrm{c}\mathrm{c}\left(\mathit{m}\right),\mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}(\mathit{k},\mathit{m})\in \mathit{M}$.
For all $\mathit{P}\in $ Agents and $\mathit{k},\mathit{m}\in \mathit{M}$ we define the following properties of the symbolic functions enc and dec, and verify and sign, respectively:
-$\mathrm{d}\mathrm{e}\mathrm{c}(\mathit{k},\mathrm{e}\mathrm{n}\mathrm{c}(\mathit{k},\mathit{m}\left)\right)=\mathit{m}$
- verify$\left(\right(\mathit{P},\mathrm{p}\mathrm{u}\mathrm{b},\mathit{n})$,m,sign$\left(\right(\mathit{P},\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{v},\mathit{n}),\mathit{m}))=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}(\mathit{n}\in \mathbb{N})$.
The symbolic functions enc, dec, sign and cc together with the above properties model the cryptographic algorithms. We define standard functions $\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}\left(\mathit{k},\left({\mathit{m}}_{1},\cdots \right.\right.$, mr )) which return the k th component (or, if k⩾r, the r th component).
Formally, for each state component C we define its state set ZC. The state of a state component is a multiset. Therefore, state sets are sets of multisets. A multiset of a set M is formally defined as a function $\mathit{f}\in {\mathit{N}}^{\mathit{M}}$ where for $\mathit{x}\in \mathit{M},\mathit{f}\left(\mathit{x}\right)$ indicates the multiplicity of x in the multiset of M. If f(x)>0 for $\mathit{x}\in \mathit{M}$, we say that x is the element of the multiset f of M (denoted by $\mathit{x}\in \mathit{f}$ ). NM is the set of all multisets of M, which we shortly denote by $\stackrel{\mathit{‾}}{\mathit{P}}\left(\mathit{M}\right)$. For each state component C a set MC has to be specified such that the state set ZC is defined as ${\mathit{Z}}_{\mathit{C}}={\mathit{N}}^{{\mathit{M}}_{\mathit{C}}}=\stackrel{\mathit{‾}}{\mathit{P}}\left({\mathit{M}}_{\mathit{C}}\right)$. Thus domains of the state component of a protocol agent P can now be defined as follows:
$\begin{array}{rr}{\mathit{Z}}_{\text{Network}\text{ }}& \mathit{ }=\stackrel{\mathit{‾}}{\mathit{P}}\left(\text{ }\text{Agents }\text{×}\text{ Agents}\text{ × }\text{Messages}\text{ }\right),\\ {\mathit{Z}}_{{\text{States}\text{ }}_{\mathit{P}}}& \mathit{ }=\stackrel{\mathit{‾}}{\mathit{P}}\left(\text{ }\text{Messages}\text{ }\right),\\ {\mathit{Z}}_{{\text{Symkeys}\text{ }}_{\mathit{P}}}& \mathit{ }=\stackrel{\mathit{‾}}{\mathit{P}}\left(\text{ }\text{Agents }\text{×}\text{ Symflags}\text{ × }\text{Messages}\text{ }\right),\\ {\mathit{Z}}_{{\text{Asymkeys}\text{ }}_{\mathit{P}}}& \mathit{ }=\stackrel{\mathit{‾}}{\mathit{P}}\left(\text{ }\text{Agents}\text{ × }\text{Asymflages}\text{ × }\text{Keys}\text{ }\right),\\ {\mathit{Z}}_{{\text{Goals}\text{ }}_{\mathit{P}}}& \mathit{ }=\stackrel{\mathit{‾}}{\mathit{P}}\text{ }\text{(Predicates}\text{ }).\end{array}$
3.2 State transition relation
Actions of agents can be simulated by state transitions of automata. Step2 of the NetBill protocol for example, where agent
C receives message sent by
M can be specified as shown in
Table 1 (we neglect information of agents' account number ).
The lines above $\stackrel{\mathit{c}\mathrm{ }}{\to }$ indicate the necessary conditions for automaton B to transform a state transition. The lines behind specify the changes of the state. $\hookrightarrow $ and $\hookleftarrow $ denote that some data are added to and removed from a state component, respectively.
3.3 Security goals
In the APA model of NetBill, the state components Goals are used to specify security goals. Whenever an agent P performs a state transition after which a specific security goal shall hold from the agents view, a predicate representing the goal is added to the state of GoalsP.
A protocol is secure (with the scope of our model) if a predicate is true whenever it is the element of a Goals component. In NetBill, security goals defined in Definition 1 and 2 in section 2 can now be concretized. In the following variables $\mathit{g},\mathit{e}\mathit{n}\mathit{c}_\mathit{g},\mathit{c}{\mathit{c}}_{-}\mathit{g}$, EPOID, EPO, K, receipt represent the goods, the encrypted goods, the checksum, an electronic payment order ID, a signed electronic payment order, a key and a signed receipt, respectively.
For customer C the predicate C1 is true if the following holds:
(1) (enc_g, cc_g, EPOID) (State C, and
(2) $\mathit{K}\in $ State C, and
(3) $\mathrm{c}\mathrm{c}\left(\mathrm{d}\mathrm{e}\mathrm{c}\right(\mathit{K}$, enc_g) ) =g.
In other words, C actually receives the goods if and only if C receives an encrypted message and a key, and the goods can be obtained by decrypting the encrypted message with the key.
And C2 is true if the following holds:
(1) (enc-g,cc-g, EPOID $)\in $ State C, and
(2) receipt $\in $ State C∧ elem (5, receipt) = true, and
(3) EPO(StateN∧ elem (4, receipt )=elem(5, EPO )∧cc-g=elem(3, EPO ), and
4) cc(dec( elem (1, receipt ), enc_g $)\ne \mathit{c}{\mathit{c}}_{-}\mathit{g}$.
Intuitively, C can claim g in court if C can show that the transaction was successfully processed by N in response to a valid request, but the goods cannot be retrieved from the decryption key released in the transaction receipt and the encrypted message given by M.
For merchant M the predicate M1 is true if the following holds:
(1) $\mathrm{E}\mathrm{P}\mathrm{O}\in {\mathrm{S}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{e}}_{\mathit{M}}\wedge \mathrm{E}\mathrm{P}\mathrm{O}\mathrm{I}\mathrm{D}\in {\mathrm{S}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{e}}_{\mathit{M}}\wedge \mathrm{E}\mathrm{P}\mathrm{O}\mathrm{I}\mathrm{D}=\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}(5,\mathrm{E}\mathrm{P}\mathrm{O})$, and
(2) receipt ( State M∧ EPOID =elem(4, receipt ), and
(3) $\mathrm{c}\mathrm{c}\left(\mathrm{e}\mathrm{n}\mathrm{c}\right(\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}(3$, receipt ),g))=elem(3, EPO ).
And the predicate M2 is true if the following holds:
1) receipt $\in $ State M∧ EPOID $\in $ State M∧ elem (5, receipt) = true ∧ EPOID = elem (6, receipt), and
2) $\mathrm{E}\mathrm{P}\mathrm{O}\in {\mathrm{S}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{e}}_{\mathit{N}}\wedge \mathrm{E}\mathrm{P}\mathrm{O}\mathrm{I}\mathrm{D}=$ elem (5, EPO).
For customer C the predicate PC is true if and only if that if M1 or M2 is true, then C1 or C2 is true. For merchant M the predicate PM is true if and only if that if C1 or C2 is true, then M1 or M2 is true. The predicates PC and PM have to be satisfied in all possible states in all protocol runs. They can therefore be in the initial state of Goals C and Goals M, respectively.
3.4 Initial state
The initial state, that is, the content of all state components in the state the protocol starts with. For NetBill this can be specified in
Table 2.The tuple ( g,message) represents a reservoir of the goods that M can sell, the agents Symkeys components as well as Network are empty in the initial state.
4 Protocol analysis
Starting with the initial state, the SHVT computes all reachable states until it finds a state in which M owns EPO and Receipt for the goods, while C is not able to actually get the goods. The SHVT outputs the state indicating a successful attack. Now one can let the SHVT compute a path from the initial state to this attack state, showing how the attack works.
In the first protocol run both C and M comply with the protocol. M generates a new key k1 and a payment id EPOID1 and stores them in StateM for later use. At the end of the protocol run, M owns in her state component StateM both 's EPO1 and a receipt receipt1 signed by N.
${\text{ }\text{State}\text{ }}_{\mathit{M}}=\left\{\begin{array}{l}\cdots (\mathit{g}1,\mathit{g}2,\text{ }\text{messages}\text{ }),(\mathit{k}1,\text{ }\text{EPOID1}\text{ }),\\ \left(\text{ }\text{EPO1, signed_EPO1}\text{ }\right),(\text{ }\text{receipt1}\text{ },\text{ }\text{signed_receipt1}\text{ }),\cdots \end{array}\right\}.$
C may now start the next protocol run. C is honest but M does not generate a new key and payment id. Instead, he uses k1 and EPOID1 of the first run. Thus the state component Network contains the following data,
$\text{ }\text{Network}\text{ }=\left\{\left(\mathit{M},\mathit{C},\left(\mathrm{e}\mathrm{n}\mathrm{c}(\mathit{k}1,\mathit{g}2),\mathit{c}{\mathit{c}}_{-}\mathit{g}2,\text{ }\text{EPOID1}\text{ }\right)\right)\right\}.$
C may still own k1 and EPOID1 in StateC and may therefore be able to decrypt the ciphertext enc( k1,g2 ). However, the protocol does not require him to check it and C has no reason to try any old keys on the new message. The assumption that C stores all proofs he ever received is quite unrealistic in any case, thus C may have deleted the particular key and the transaction id. Consequently, C responds M with EPO2, which results in
$\text{ }\text{Network}\text{ }=\left\{\right(\mathit{C},\mathit{M},(\text{ }\text{EPO2}\text{ },\text{ }\text{signed_EPO2}\text{ })\left)\right\}.$
Now, since M still owns EPO2 and receipt1, he owns a valid proof of C having received g2 that will be accepted by any judge, i.e., the predicate M1 is true. Now if M stops the protocol run, then C cannot receive any receipt of this run from N. So condition 2) in the predicate C1 and C2 cannot be satisfied, i.e., the predicate C1 and C2 are both false. Thus, the security goal PC is not satisfied and C in fact will never be able to retrieve g2.
We suggest improving the protocol by letting C introduce his own label LC when receiving the encrypted goods and including this label in subsequent messages EPO. Thus, the new EPO and Receipt are defined as follows:
-EPO: $\mathit{C},\mathit{M},\mathrm{C}\mathrm{C}\left({\mathit{E}}_{\mathit{K}}\left(\mathrm{G}\mathrm{o}\mathrm{o}\mathrm{d}\mathrm{s}\right)\right),{\mathit{E}}_{\mathit{K}}\left(\mathrm{G}\mathrm{o}\mathrm{o}\mathrm{d}\mathrm{s}\right),\mathrm{E}\mathrm{P}\mathrm{O}\mathrm{I}\mathrm{D},{\mathit{E}}_{\mathit{C}}\mathit{N}\left(\mathrm{C}\mathrm{A}\mathrm{c}\mathrm{c}\mathrm{t}\right),{\mathit{L}}_{\mathit{C}}$
-Receipt: C,M,K, EPOID, result, transferred, LC
We analyze the improved protocol using SHVT and find out it is secure to the above attack. The attack is prevented because even if M has EPO2 and receipt1 of the first run, the value of LC in EPO2 is not equal to that of receipt1. i.e., condition 2) in M1 and condition 1) in M2 are false. So M cannot prove that C has received the goods g2, thus nobody will trust that they are of the same transaction.
5 Conclusion
We have proposed an APA model of NetBill and analyzed it using SHVT. By our method we find an attack on interleaved protocol runs. To avoid the attack we improve the protocol. Compared to other approaches, our methods are both flexible and minimal with respect to implicit assumptions used. Our current work includes applying the method to the designing of an e-commerce protocol.
PDF
(304KB)
