Security analysis of two fair exchange protocols

Abstract

E-commerce applications enable two parties to exchange digital items electronically. It is critical for such applications that the underlying protocols ensure the fairness requirement: no honest participant should suffer any loss of significant value. It is important to verify that an e-commerce protocol satisfies its fairness goal. Formal methods such as model checking can be helpful in this regard. To this end, it is essential to develop a model of the protocol under realistic assumptions. Using the NetBill protocol as an example this work shows how improper modelling can lead to incorrect claims about the protocol. It also shows how a carefully developed formal model can be successfully used to discover previously unknown flaws in an existing protocol.