Second USENIX Workshop on Electronic Commerce
Model Checking Electronic Commerce Protocols
Nevin Heintze, Bell Labs
J.D. Tygar, Jeannete Wing, and H. Chi Wong
Carnegie Mellon University
Abstract
The paper develops model checking techniques to examine NetBill and
Digicash. We show how model checking can verify atomicity properties
by analyzing simplified versions of these protocols that retain
crucial security constraints. For our analysis we used the FDR model
checker.
View the full text of this paper in
HTML and
POSTSCRIPT (187,504 Bytes) form.
To Become a USENIX Member, please see our
Membership Information.
|