DEPARTMENT OF COMPUTER SCIENCE
SEMINAR REPORT
ON
MODEL CHECKING
FOR
SECURING E-COMMERCE TRANSACTIONS
PRESENTED BY
JAHFAR.C
Batch 2008-2010
Department of Computer Science
CUSAT
1Page 2

Seminar Report
Model checking for securing E-commerce transaction
Cochin University of Science & Technology
Cochin-22
DEPARTMENT OF COMPUTER SCIENCE
CERTIFICATE
This is to certify that, the seminar report entitled
ËœMODEL
CHECKING
FOR
SECURING
E-COMMERCE
TRANSACTIONSâ„¢ Submitted by JAHFAR .C in partial fulfillment of the
requirements for the award of Master of Technology in SOFTWARE
ENGINEERING of Cochin University of Science and Technology is a
record of seminar presented by him in the department of computer science
during the year 2008-2010
.
Seminar Coordinator
Director
Dr.Sumam Marry Idicula
Dr.K.Poulose Jacob
Department of Computer Science
CUSAT
2Page 3

Seminar Report
Model checking for securing E-commerce transaction
ACKNOWLEDGEMENT
I express my deep sense of gratitude to D.r. K.Poulose Jacob, HOD,
Department of Computer Science, CUSAT, for providing an opportunity to
present this seminars.
My profound gratitude to Dr.Sumam Marry Idikula for her valuable
guidance and timely support she offered. My sincere thanks to all other
teaching staff, especially, Mr.Santhosh Kumar and all non teaching staff for
their generous help and guidance. I also express my friendly gratitude to my
batch mates for their kind co-operation and good wishes.
Finally, I thank the God Almighty, without whose blessings nothing
starts good or ends well.
Department of Computer Science
CUSAT
3Page 4

Seminar Report
Model checking for securing E-commerce transaction
ABSTRACT
The rapid growth of electronic commerce (e-commerce) has
necessitated the development of e-commerce protocols. These protocols
ensure the confidentiality and integrity of information exchanged. In addition,
researchers have identified other desirable properties, such as, money
atomicity, goods atomicity and validated receipt, that must be satisfied by e-
commerce protocols. This seminar shows how model checking can be used to
obtain an assurance about the existence of these properties in an e-commerce
protocol. It is essential that these desirable properties be satisfied, even in the
presence of site or communication failure. Using the model checker we
evaluate which failures cause the violation of one or more of the properties.
The results of the analysis are then used to propose a mechanism that handles
the failures to make the protocol failure resilient.
.
Department of Computer Science
CUSAT
4Page 5

Seminar Report
Model checking for securing E-commerce transaction
CONTENTS
1. INTRODUCTION¦¦¦¦¦¦¦¦¦¦¦¦¦¦
-6-
2 . PROACTIVE, AUTOMATED AND CONTINUOUS -
CONTROL AND ASSURANCE FRAMEWORK
-7-
¢ Mechanism Design
¢ Atomic Transactions
¢ Model Checking
¢ Real-time Monitoring
3. FAILURE ANALYSIS OF AN E-COMMERCE -
PROTOCOL USING MODEL CHECKING
-12-
¢
Basic Protocol
¢ Model the e-commerce protocol
¢
Detecting Violation of Properties due to Failures
¢
Ensuring Failure Resilence of the Protocol
4. STRENGTH AND WEAKNESS ¦¦¦¦¦¦¦¦¦¦ -26-
5. CONCLUSION¦¦¦¦¦¦¦¦¦¦¦¦¦¦¦
-27-
6. REFERENCES¦¦¦¦¦¦¦¦¦¦¦¦¦¦¦
-28-
Department of Computer Science
CUSAT
5Page 6

Seminar Report
Model checking for securing E-commerce transaction
INTRODUCTION
The growing popularity of e-commerce has resulted in the development
of a number of e-commerce protocols. Most of these protocols ensure that the
information exchanged between the parties is protected from unauthorized
disclosure and modification. Moreover, researchers have identified several
other desirable properties of e-commerce protocols. Examples of these
properties include money atomicity and goods atomicity and validated receipt.
Money atomicity ensures that money is neither created nor destroyed in the
course of an e-commerce transaction. Goods atomicity ensures that a merchant
receives payment if and only if the customer receives the product. Validated
receipt ensures that the customer is able to verify the contents of the product
about to be received, before making the payment. Although such properties
have been identified, a major problem is verifying if a given e-commerce
protocol satisfies these properties, specially in the presence of network and site
failures. In this paper we address the problem of protocol verification using an
existing software verification technique known as model checking.
The reasons for using model checking are as follows. First, model
checking is a completely automated technique and considerably faster than
other approaches, such as, manual proofs and simulations. Second, if a
property does not hold, a counter example is produced by the model checker
which helps in understanding why the property does not hold. Last, but not the
least, model checking has previously been used successfully to verify security
protocols
.
Department of Computer Science
CUSAT
6Page 7

Seminar Report
Model checking for securing E-commerce transaction
PROACTIVE, AUTOMATED AND CONTINUOUS CONTROL
AND ASSURANCE FRAMEWORK (PACCAF)
We define an e-commerce system as a network of distributed digital
processes, interacting in an established manner to serve business objectives.
An e-business is a system of such systems. The analysis of an e-business
decomposes a high level entity into its sub-systems that follow the same rules
used to analyze a single system. To control and assure an e-system, auditors
must thoroughly understand the subject system. To do so, auditors should
investigate the entire life cycle of the system. System Development Life Cycle
(SDLC) is a popular systems approach to problem solving. It has long proven
itself to be a disciplined approach to developing information systems. SDLC
remains one of the design models for developing e-business applications; for
instance, parts of the IBM e-business framework are designed to work within
SDLC (Harvey 2000). Similarly, our methodology framework PACCAF is
also embedded within SDLC because we believe that control and assurance
should be an inimitable process running in parallel to the entire life cycle of a
system. There are six phases in SDLC: system analysis, definition, design,
development, implementation and maintenance. We embed an innovative set
of methods “ economic reasoning, atomic transaction design, model checking
and real-time monitoring “ in SDLC, with each of them to be applied
respectively in different phases of SDLC
Department of Computer Science
CUSAT
7Page 8

Seminar Report
Model checking for securing E-commerce transaction
Using Mechanism Design in SDLC Phase I: System Analysis
The major task in system analysis is to obtain an in-depth understanding of
the present system and of the problems and limitations inherent in it. Analysis
is particularly critical in ecommercebecause many digital firms, when
transitioning to e-commerce, have simply carried over the traditional policies
and trading rules by redressing them to execute in the Web computing
environment, but, unfortunately, policies and trading rules that function well
in the brick-and-mortar commerce may fail in the digital setting. Fraudulent or
Department of Computer Science
CUSAT
8Page 9

Seminar Report
Model checking for securing E-commerce transaction
malicious traders may exploit the resulting structural weaknesses. Designing a
robust process structure, safe against fraud and attack, falls into the realm of
traditional internal controls. However, reinterpretation is needed for handling
special issues that appear in e-commerce. For example, separation of duties
should be applied not only to divide responsibilities among personnel who
design, implement, operate or monitor an e-system, but also to direct how to
divide functionalities among e-processes.
Atomic Transactions in SDLC Phase II: System Definition
In SDLC phase II “ system definition “ detailed business requirements
are further defined in terms of the overall system objectives. Based on these
requirements, the designers prepare a conceptual design of the system. These
business requirements also determine the properties and specifications that the
system should satisfy. To define them, the designers first need to bound the
system. This is an easier task for a brick-and-mortar system than an e-
commerce system because of the dynamic and real-time interconnectivity and
interdependence of e-processes within and across firms.
The pervasive use of distributed computation today implies that the
integrity of such systems must be accepted as effective. The achievement of
the reasonable integrity should be subject to the ACID properties, i.e.,
atomicity, consistency, isolation, and durability, because these properties have
emerged as the unifying concepts for distributed computing. Achieving the
integrity of distributed e-commerce systems must also follow these established
concepts. Moreover, an e-business must protect its assets and privacy not
addressed directly by ACID. Thus, we add authorization, authentication and
confidentiality, resulting in the ACID-AAC property list:
Atomicity. A transactionâ„¢s changes to the state are atomic: either all happen or
none happen.
Department of Computer Science
CUSAT
9Page 10

Seminar Report
Model checking for securing E-commerce transaction
Consistency. A transaction is a correct transformation of the state. The
operations taken as a group do not violate any of the integrity constraints
associated with the state.
Isolation. Even though transactions are executed concurrently, it appears to
each transaction that, others executed either before it or after it, but not both.
Durability. Once a transaction completes successfully (commits), its changes
to the state survive failure.
Authorization. A transaction is only executed upon proper approval.
Authentication. Entities involved in a transaction are proved as what they
claim to be.
Confidentiality. A transaction is kept secret from unauthorized observation.
A simple and common example for explaining ACID relates to bank
transactions. A cash withdrawal is atomic if it both dispenses money and
reduces your account. It is consistent if the cash dispensed equals to the
account reduction. It is isolated if the withdrawal is unaware of other
transactions accessing your account concurrently (e.g., a deposit). And it is
durable, if, once the transaction is complete, the account balance is sure to
reflect the withdrawal.
Applying Model Checking in SDLC Phases III, IV, and V: System
Design, Development and Implementation
System design, development, and implementation realize the conceptual
design in information systems, including hardware and software. Our main
concern here is with software quality. As we discussed previously, e-system
designers and assures need the quality assurance at the Internet infrastructure
and application layers, choosing reliable networking products and
services,robust operating systems2, reliable databases, and qualified Web
Department of Computer Science
CUSAT
10Page 11

Seminar Report
Model checking for securing E-commerce transaction
commerce development tools. We wish most of these quality assurance can be
purchased in the market in the near future. If so, the correctness of an e-
business system will primarily depend upon the design and coding of e-
business processes.
The reasons for using model checking are as follows. First , model
checking is a completely automated technique and considerably faster than
other approaches, such as, theorem proving. Second, if a property does not
hold, a counter example is produced by the model checker which helps in
understanding why the property does not hold. Last, but not the least, model
checking has previously been used successfully to verify security protocols
Introducing Real-time Monitoring for SDLC Phase VI: System
Maintenance
In the system maintenance phase, the new system is placed in a real-
world execution. While economic reasoning, atomic transaction design, and
model checking aim to ensure system integrity from design to implementation,
how the system actually performs remains a real concern. We suggest that
embedded sensors be included in the system and monitors be used to collect
real-execution information in order to coordinate transactions and verify
system properties in real-time.
Department of Computer Science
CUSAT
11Page 12

Seminar Report
Model checking for securing E-commerce transaction
Failure Analysis of an E-commerce Protocol using Model
Checking
The rapid growth of electronic commerce has necessitated the
development of e-commerce protocols. These protocols ensure the
confidentiality and integrity of information exchanged. In addition, researchers
have identified other desirable properties, such as, money atomicity, goods
atomicity and validated receipt, that must be satisfied by e-commerce
protocols. This paper shows how model checking can be used to obtain an
assurance about the existence of these properties in an e-commerce protocol.
It is essential that these desirable properties be satisfied, even in the presence
of site or communication failure. Using the model checker we evaluate which
failures cause the violation of one or more of the properties. The results of the
analysis are then used to propose a mechanism that handles the failures to
make the protocol failure resilient
.
Briefly, our contribution is as follows. First, we show how to model the
e-commerce protocol and the desirable properties in a specification language,
and then verify these properties using an existing model checker. Formal
specification and verification give an increased assurance that the properties
are indeed satisfied by the protocol. Second, we show how to model site and
communication failures. We use the FDR model checker to identify which
failures preserve the properties and which ones do not. Finally, we propose a
mechanism to handle the identified failures that do not preserve the desirable
properties; integrating this mechanism with the protocol ensures that the
resulting protocol satisfies the properties in the presence of failures.
Department of Computer Science
CUSAT
12Page 13

Seminar Report
Model checking for securing E-commerce transaction
Department of Computer Science
CUSAT
13Page 14

Seminar Report
Model checking for securing E-commerce transaction
Department of Computer Science
CUSAT
14Page 15

Seminar Report
Model checking for securing E-commerce transaction
Modeling Communication between Processes
when two agents are communicating, two channels are associated
with each agent for a total of four channels. For example, to model the
communication between the merchant and the customer four channels, (minc,
coutm, cinm, moutc) and two processes (COMMmc and COMMcm ) are
involved. The process COMMmc reads a data from channel coutm and writes
the data to channel minc and the process COMMcm reads a data from
channel moutc and writes it to channel cinm. Process COMMcm is modeled
in CSP as: COMMcm = []x: {po} @(coutm ?x -> (minc !x ->
COMMcm
Modeling the Customer Process
The protocol starts when the customer browses the catalog hosted on the
third party and downloads the encrypted product from there. The downloading
of the encrypted product is modeled as the sending of the encrypted product
by the third party and the receipt of the product by the customer. Thus, we can
say that, initially the customer waits for an encrypted product from the third
party.
CUSTOMER = cint ?x -> DOWNLOADED_EGOODS(x).
Once the customer has downloaded the product, it sends a purchase order
to the merchant. This is modeled as:
DOWNLOADED_EGOODS(x) = coutm !po -> PO_SENT(x)
The customer then waits for the encrypted product from the merchant.
On receiving a message from the merchant, the customer checks to see if the
message is indeed some encrypted product sent by the merchant. If so, the
customer proceeds to the next step, otherwise it continues to wait for the
encrypted product. The specification for this event is as:
Department of Computer Science
CUSAT
15Page 16

Seminar Report
Model checking for securing E-commerce transaction
PO_SENT(x)
=
cinm
?y
->
if
(y==encryptedGoods1
or
y==encryptedGoods2) then RECEIVED_EGOODS(x,y)else PO_SENT(x)
The next step involves comparing the encrypted product received from
the merchant with those downloaded from the third party. If the two do not
match, the customer terminates the protocol.
RECEIVED_EGOODS(x,y)=
if(x==y)then
RECEIVED_CORRECT_GOODS
else ABORT
When the customer is satisfied with the encrypted product, he sends the
payment token to the third party.
RECEIVED_CORRECT_GOODS = coutt !paymentToken -> TOKEN_SENT
After sending the payment, the customer waits for a message from the
trusted third party. The third party either sends the customer the key or an
abort message, depending on the outcome of the protocol. Once the customer
has received the message from the third party, the protocol stops. Otherwise
the customer continues to wait for the message.
TOKEN_SENT = cint ?y -> if (y==key) then SUCCESS else if (y==
transactionAborted) then ABORT else TOKEN_SENT
Modeling the Merchant Process
On the merchant side, the protocol begins with the merchant waiting to
receive a purchase order from a customer.
MERCHANT = minc ?x -> if (x==po) then PO_REC else MERCHANT
The merchant in response must send an encrypted product to the customer.
The merchant can act in two ways “ either he sends the correct encrypted
product (denoted by encryptedGoods1) or an incorrect encrypted product
(denoted by encryptedGoods2). This non-deterministic choice is modeled as
follows:
PO_REC = (moutc !encryptedGoods1 ->ENCRYPTED_GOODS_SENT)|Ë|(moutc !
encryptedGoods2 -> ENCRYPTED_GOODS_SENT)
Department of Computer Science
CUSAT
16Page 17

Seminar Report
Model checking for securing E-commerce transaction
Once the merchant has sent the encrypted product, he must send the
decryption key to the trusted third party.
ENCRYPTED_GOODS_SENT = moutt !key -> KEY_SENT
After sending the key, the merchant waits to receive the payment token
from the third party. The third party either sends the payment token or a
transaction abort message if the transaction was aborted. The merchant process
terminates once it receives a message, otherwise it continues to wait for the
message.
KEY_SENT = mint ?x -> if (x==paymentToken)then SUCCESS else if
(x==transactionAborted)
then ABORT else KEY_SENT
Modeling the Trusted Third Party Process
The customer downloading the encrypted product, is modeled from the
third partyâ„¢s end, as the trusted third party sending the encrypted product to the
customer.
TP = toutc !encryptedGoods1 -> WAIT_TOKEN_KEY
The next step involves the third party waiting to receive the payment token
from the customer and the key from the merchant. When the third party
receives a message it checks if the message is a payment token or key or
neither. Note that, it is not known whether the key or payment token will
arrive first. If the payment token arrives first, the third party must wait for the
key. On the other hand, if the key arrives first, the third party must wait for the
payment token. This aspect of the protocol is modeled as follows:
WAIT_TOKEN_KEY = (tinc ?a -> if (a==paymentToken)then WAIT_KEY(a) else
WAIT_TOKEN_KEY) [] (tinm ?b -> if (b==key) then WAIT_TOKEN(b)else
WAIT_TOKEN_KEY)WAIT_KEY(a)
=
tinm
?b
->
if
(b==key)
then
CHECK_TOKEN(a,b) else WAIT_KEY(a) WAIT_TOKEN(b) = tinc ?a -> if
(a==paymentToken) then CHECK_TOKEN(a,b) else WAIT_TOKEN(b)
Department of Computer Science
CUSAT
17Page 18

Seminar Report
Model checking for securing E-commerce transaction
Once the third party has received both the key and the payment token, it
proceeds to the next step of validating the payment token with the customerâ„¢s
financial institution. The details of the validation process is outside the scope
of the protocol and is not modeled. Instead, the model no deterministically
chooses between the options: (i) token okay or (ii) token not okay. If the
payment token is okay, the third party proceeds to send out the key to the
customer and the token to the merchant. If the payment token is not okay an
abort message is sent to the customer and the merchant, and the protocol
terminates.
CHECK_TOKEN(a,b) = OK_TOKEN(a,b) |Ë| NOK_TOKEN OK_TOKEN(a,b) =
SEND_TOKEN_KEY(a,b) NOK_TOKEN = SEND_ABORT_MESSAGE
The process of sending an abortmessage to customer and merchant is modeled
by the following step.
SEND_ABORT_MESSAGE = toutc !transAborted -> toutm !transAborted -> STOP
Modeling the Money Atomicity Property
Money atomicity is satisfied when one of the following things happen:
(i)the customer sends the payment token and the merchant receives it or (ii) the
customer sends the payment token and then receives a transaction abort
message. This is modeled as
SPEC1 = STOP |Ë| ((coutt.paymentToken ->mint.paymentToken ->
STOP) [] (coutt.paymentToken cint.transAborted -> STOP))
Modeling the Goods Atomicity Property
The goods atomicity property requires one of the following things to
happen: (i) the customer receives both the correct encrypted product and the
keys and the merchant receives the token, or (ii) the customer receives
just the encrypted product and neither the merchant gets the payment token nor
the customer the keys
Department of Computer Science
CUSAT
18Page 19

Seminar Report
Model checking for securing E-commerce transaction
SPEC2
=
STOP
|Ë|
((cinm.encryptedGoods1
->
STOP)[]
(cinm.encryptedGoods2 -> STOP) [](cinm.encryptedGoods1 ->
cint.key
->
mint.paymentToken
->
STOP)
[]
(cinm.encryptedGoods1 mint.paymentToken -> cint.key -> STOP))
Modeling the Validated Receipt Property
The validated receipt property ensures one of the following things happen:
(i) the customer receives some encrypted product and does not make payment
(either because he has received incorrect product or decides not to purchase
the product), or (ii) the customer makes the payment after receiving the correct
encrypted product. This is modeled as:
SPEC3
=
STOP
|Ë|
((cinm.encryptedGoods2
->
STOP)
[]
(cinm.encryptedGoods1->STOP)[](cinm.encryptedGoods1
coutt.paymentToken -> STOP))
Detecting Violation of Properties due to Failures
An informal analysis reveals that the properties may be violated if the
customer, merchant, third party and commu Communication links fail
arbitrarily. The following paragraphs describe how we use the model checker
to detect failures that result in the destruction of the properties.
Introducing Unreliable Communication Channels
The properties are violated when the following channels are made
unreliable: (i) the channels connecting the third party and the customer and (ii)
those connecting the third party to the merchant.
Department of Computer Science
CUSAT
19Page 20

Seminar Report
Model checking for securing E-commerce transaction
Introducing Failures in the Customer Process
In the following paragraphs we show how the properties get violated when
the customer process fails at certain points. Consider the first step for the
customer process:
CUSTOMER = cint ?x -> DOWNLOADED_EGOODS(x)
Suppose we allow the customer to abort in this step. The question, then, is does
any property get violated? To find out, we need to model the possibility of the
customer aborting in the first step:
CUSTOMER = ABORT |Ë| (cint ?x -> DOWNLOADED_EGOODS(x))
The above specification says that the customer may abort or wait for the
downloading of the encrypted product in a non-deterministic manner. After
making the above alteration to the customer process, we use FDR to check for
the satisfaction of the properties. As expected, the customer aborting in the first
step, has no effect on the properties. We make similar modifications to each
step in the customer process and check for the violation of the properties. Our
results indicate that such modification to any step, except in the last step of the
customer process (that is after the customer has sent the payment token),
preserves all the properties. Allowing the customer to abort in the last step
violates both money atomicity and goods atomicity.
toutc.encryptedGoods1,cint.encryptedGoods1,coutm.po,inc.po,mou
tc.encryptedGoods1,moutt.key,tinm.key,cinm.encryptedGoods1,cou
tt.paymentToken,tinc.paymentToken,toutc.transAborted,
toutm.transAborted, mint.transAborted
The above sequence tells us that the following actions are executed. The
customer downloads the encrypted product from the third party, then sends a
purchase order to the merchant. On receiving the purchase order, the merchant
sends the encrypted product to the customer and the key to the third party. The
Department of Computer Science
CUSAT
20Page 21

Seminar Report
Model checking for securing E-commerce transaction
third party receives the key. The customer receives the encrypted product and
validates it. The customer then sends the payment token to the third party. At
this point, it appears that the customer aborts since we do not see any more
messages sent or received by the customer. The third party receives the key
from the merchant, the payment token from the customer, and then validates the
token. The token turns out to be invalid and an abort message is sent by the
third party to the customer and the merchant. Since the customer has aborted in
the mean time, he does not get the transaction abort message from the third
party. The merchant, however, receives the abort message. In the above
scenario, the customer sends out the payment token, but neither the merchant
received the payment token nor the customer the transaction abort message.
Thus money atomicity is violated. Similarly, a counter example is generated
illustrating how goods atomicity was violated.. Thus, our conclusion is that, the
customer cannot abort after sending out the payment token and before
receivingthe key; if the customer does indeed abort we will no longer have
money atomicity or goods atomicity.
Failures in Merchant, Third Party Processes
Allowing the merchant process to abort in the last step, that is, after
sending the key but before receiving the payment token, violates both money
atomicity and goods atomicity. Finally, we consider the third party process. The
third party process can abort unilaterally only at its first step.
Ensuring Failure Resilence of the Protocol
From the above discussion we can summarize: (i) The customer cannot
abort after he has sent the payment token to the third party. (ii) The merchant
cannot abort after he has sent the product decryption key to the third party. (iii)
The third party cannot abort unilaterally after its first step To ensure that the e-
Department of Computer Science
CUSAT
21Page 22

Seminar Report
Model checking for securing E-commerce transaction
commerce protocol is resilient to site or page link failures we propose the following
extension to the basic protocol. We assume that each party involved in the
transaction, keeps a copy of the information that it sends to another party “ for
example purchase order, payment token and so on “ in its stable storage till
such time as the information is no longer needed. Writes to the stable storage
are atomic and durable until intentionally purged.
1. The customer, the merchant and the third party uses a system-wide unique
identifier, Ti, to denote the current e-commerce transaction. The identifier is a
tuple of the form <PID;C;M>, where PID is the identifier for the product the
customer, C purchases from the merchant, M. The customer stores a log record
of the form <Ti;INITIATE> to its stable storage and then sends the purchase
order to the merchant.
2. When the merchant receives the purchase order, it writes a log record
<Ti;INITIATE> to its stable storage; then the merchant checks to see if the
purchase order is to its satisfaction. If it is not, the merchant writes an abort
record in its log “ <Ti;ABORT> and aborts the transaction. It informs the
customer of this decision. Otherwise it sends the encrypted product to the
customer and the product decryption key and the approved purchase order to
the third party. Finally, it writes a log record to its stable storage of the form
<Ti;KEY-SENT>. At this stage the merchant enters a point of no return; it
cannot abort unilaterally.
3. After receiving a message from the merchant the customer checks to see if it
is an abort message or the encrypted product. If it is an abort, the customer
aborts the transaction and writes a log record of the form <Ti;ABORT>.
Otherwise the customer validates the encrypted product. If validated, the
Department of Computer Science
CUSAT
22Page 23

Seminar Report
Model checking for securing E-commerce transaction
customer sends the payment token and purchase order to the third party and
then writes a log record to its stable storage. The log record is of the form
<Ti;PAYMENT- SENT>. This is the point of no return for the customer. If the
encrypted product is not validated the customer can either request the product
from the merchant, or abort the transaction.
4. One of the messages - either the message containing the payment token and
purchase order from the customer or the message containing the product
decryption key and approved purchase order from the merchant - will arrive at
the third party before the other message. On receiving the message, the third
party associates the unique identifier Ti to this current transaction and writes a
log record to its stable storage of the form <Ti;INITIATE>. The third party
starts a timer at this point. If the third party does not receive the other message
before the timer expires, it writes a log record <Ti;ABORT> and sends abort
messages to both the customer and the merchant.
5. After receiving the payment token from the customer, the third party
validates the token with the customerâ„¢s financial institution. If the validation
fails the third party writes a log record <Ti;ABOR> and informs both the
customer and the merchant. Otherwise, after the third party has received both “
the product decryption key from the merchant and the payment token from the
customer “ the third party sends the payment token to the merchant and writes
a log record <Ti;PAYMENT “FORWARDED>, and sends the decryption key
to the customer and writes a log record <Ti;KEY-FORWARDED>.
Department of Computer Science
CUSAT
23Page 24

Seminar Report
Model checking for securing E-commerce transaction
6. The customer writes the log record <Ti;FINISH> after receiving the
decryption key from the third party. 7. The merchant also writes a log record
<Ti;FINISH>, after it has received the payment token.
Protocol Failure Analysis
1.Merchant fails after sending product decryption key but before
writing <Ti;KEY-SENT>. After recovery from failure the merchant finds from
its log that Ti has been initiated but the product decryption key has not been
sent out (no information about the key having been sent is recorded).
Consequently, it queries the third party to find out the status. If the status is
abort, the merchant aborts. If the third party has not received the key, the
merchant resends the key and write the appropriate record. If the third party
cannot provide a status, the merchant resends the encrypted product to the
customer, and the key and approved purchase order to the third party and
writes the appropriate log records. It then waits for the payment token from the
third party. Finally, as a result of the status query the merchant may receive the
payment token. It then finishes by writing the appropriate log record.
2. Merchant fails after writing <Ti,KEY “SENT> or Merchant fails before
writing <Ti,FINISH>. After recovery from failure, the merchant finds that it
has not received the payment token. It asks the third party for the payment
token. The third party responds either by sending the payment token or an
abort message. If it is an abort message, the merchant write <Ti,ABORT> in its
stable storage and aborts. If payment token is received the merchant writes
<Ti,FINISH> to log.
3. Customer fails after sending payment token but before writing
<Ti,PAYMENT “SENT>. After recovery, the customer notes from log that Ti
Department of Computer Science
CUSAT
24Page 25

Seminar Report
Model checking for securing E-commerce transaction
has been initiated but no other information (such as, information about the
product received or payment token sent) is recorded in the log. The customer,
in this case, gets in touch with the merchant and asks for the product. The
merchant either sends the encrypted product or an abort message. If the
customer receives the encrypted product, the customer validates it, sends the
payment token and writes the appropriate log record.
4. Customer fails after writing <Ti,PAYMENT “SENT> or Customer fails
before writing<Ti,FINISH>. After recovery the customer notes that the
decryption key has not been received. So it requests the third party for the
product decryption key. The third part responds with either an abort message or
the decryption key. If it is an abort
message, the customer writes <Ti,ABORT> to its log and aborts. If it is the
decryption key, the customer writes <Ti,FINISH> to the log and finishes.
5. Third party fails before writing <Ti,INIT IATE>. At this stage the third
party is not aware of the transaction Ti. Consequently the third party does
nothing. At some point of time either the customer or the merchant will get in
touch asking for the product decryption key or a status query. At this stage the
third party will write the log record <Ti,INITIATE> and ask the customer for
the payment token and purchase order, and the merchant for the product
decryption key and the approved purchase order. It then starts the timer.
6. Third party fails after writing hTi;INITIATEi. or Third party fails before
writing either <Ti,PAYMENT “FORWARDED>
or <Ti,KEY “
FORWARDED>. After recovery the third party notes that Ti has been initiated.
It asks the customer for the payment token and purchase order, and the
merchant for the product decryption key and the approved purchase order. Once
the third party has received a response, it starts the timer and waits for the other
message.
Department of Computer Science
CUSAT
25Page 26

Seminar Report
Model checking for securing E-commerce transaction
7. Third party fails after writing one of the records<Ti,PAYMENT-
FORWARDED> or <Ti,KEY “FORWARDED> but before writing the other.
After recovery the third party sends the message that was not sent out and
writes the appropriate record.
Department of Computer Science
CUSAT
26Page 27

Seminar Report
Model checking for securing E-commerce transaction
Strength and Weakness
Model checking is a completely automated technique and considerably
faster than other approaches, such as, manual verification and simulations.
Second, if a property does not hold, a counter example is produced by the
model checker which helps in understanding why the property does not hold.
Third, It helps to locate critical flaws that other approaches may not find. Last,
but not the least, model checking has previously been used successfully to
verify security protocols.
In model checking we have to model each and every processes and
property using a suitable specification language. In some cases it will be very
difficult to model business systems. Also need Limited expenses of formal
presentation language.
Department of Computer Science
CUSAT
27Page 28

Seminar Report
Model checking for securing E-commerce transaction
Conclusion
Model checking is an extremely powerful technique for protocol
verification. It is used to get an assurance that an e-commerce protocol does
satisfy the properties of money atomicity, goods atomicity, and validated
receipt properties in the presence of site and communication failures. After
verification, it propose a mechanism that preserves the properties even in the
event of sites or communications failures.
Department of Computer Science
CUSAT
28Page 29

Seminar Report
Model checking for securing E-commerce transaction
References
1. Anderson, B.B., Hansen,J.V., and Summers,S. Model checking for design
and assurance of e-business process.Communications of ACM 49, 6 (June
2006),97-101
2. Heintze, N., Tygar, J., Wing, J., and Wong,H. Model checking electronic
commerce protocols
3. I. Ray and I. Ray. Failure Analysis of an E-commerce Protocol using Model
Checking . Technical report, University of Michigan-Dearborn, Jan. 2000.
4. http://engin.umd.umich.edu/Ëiray.
5. http://en.wikipediawiki/Model_checking