| The recent years have witnessed an explosion in the volume of trade over computer networks, also called e-commerce (or electronic commerce). E-commerce transactions can be either general transactions (two party exchange of product for payment), auctions, or multi-party (stock/commodity market) transactions. These transactions may or may not involve real-time constraints. To successfully complete e-commerce transactions, the involved parties execute a sequence of steps, called a protocol. The design of good protocols requires the addressing of various issues, which have been universally identified as required or desired for e-commerce protocols: security, atomicity, privacy, anonymity, and low overhead cost. Current state-of-the-art protocols for general transactions, such as Ecash, NetBill, etc., have been designed to specifically target only a subset of the above properties. Only preliminary research has been done in the areas of electronic auctions and multi-party transactions.; This dissertation is focussed on the design and verification of e-commerce protocols for four categories of transactions: (a) general transactions, (b) auctions, (c) multi-party transactions, and (d) each of the above with real-time constraints. E-commerce protocols having all of the five above mentioned properties are developed for each of these categories of transactions. Furthermore, the developed protocols have various other attractive characteristics. For example, a customer is not required to store money in a special account, mediation by a third party is required only in some rare special cases, multiple rounds of automated bidding are allowed by the auction protocols, and the developed protocols are simple to implement. Also, a novel methodology is developed which allows incorporation of real-time constraints into any given e-commerce protocol with the guarantee that all existing properties will be preserved.; A formal logic is developed based on the semantics of the popular BAN logic, which allows the modeling of powerful intruders capable of both passive and active attacks. The logic is used to prove that each of the developed protocols have all the five properties. Together, the developed protocols, the real-time methodology, and the associated proofs, make a fundamental contribution to the process of realizing the promise of e-commerce. |
