Next: Atomicity Properties Up: Model Checking Electronic Commerce

Model Checking Electronic Commerce Protocols

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.

• Atomicity Properties
• Model Checking
• Two Case Studies
  • NetBill
  • A Simplified Digital Cash Protocol
• Summary and Discussion of Our Contributions
• Future Work
• References
• Appendix
  • NetBill
  • A Simplified Digital Cash Protocol
• About this document ...