...

This work was supported in part by Defense Advanced Research Project Agency (ARPA contract F33615-93-1-1330), the National Science Foundation (NSF cooperative agreement IR-9411299), and by the US Postal Service. This work is the opinion of the authors and does not necessarily represent the view of their employers, funding sponsors, or the US Government.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...properties

Use of formal methods to demonstrate protocol security has attracted wide attention - we cannot survey all the results in a brief paper such as this. However, electronic commerce protocols have received less attention - two important papers on formal (non-model checking) methods for electronic commerce are [1, 13].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...K

What if a corrupt merchant sends a bogus K? In the Netbill protocol, in step 4, the merchant sends a signed version of K to the bank. Previously, in step 2, the merchant has sent the goods (encrypted with K) to the consumer, and the hash of those has been included in the EPO and signed by both the merchant and the consumer. Hence, after the fact, the fraud and responsible party can be detected and proven to other parties. This is treated at length in [5, 22]. Our analysis in this paper does not consider the impact of bogus keys.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.