References

1

Ross Anderson. UEPS - a second generation electronic wallet. In The Second European Symposium on Research in Computer Security, pages 411-418, 1992.

2

L. Jean Camp, Marvin Sirbu, and J. D. Tygar. Token and notational money in electronic commerce. In Proceedings of the First USENIX Workshop in Electronic Commerce, pages 1-12, July 1995.

3

D. Chaum. Security without identification: Transaction systems to make big brother obsolete. Communications of the ACM, 28(10):1030-1044, October 1985.

4

D. Chaum, A. Fiat, and M. Naor. Untraceable electronic cash. In Advances in Cryptology -- CRYPTO '88 Proceedings, pages 200-212. Springer-Verlag, 1990.

5

Benjamin Cox, J. D. Tygar, and Marvin Sirbu. NetBill security and transaction protocol. In Proceedings of the First USENIX Workshop in Electronic Commerce, pages 77-88, July 1995.

6

David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522-525, 1992.

7

J. Gray and A. Reuter. Transaction Processing. Morgan-Kauffman, 1993.

8

James N. Gray. A transaction model. Technical Report RJ2895, IBM Research Laboratory, San Jose, California, August 1980.

9

Zvi Har'El and Robert P. Kurshan. Software for analytical development of communications protocols. In AT&T Technical Journal, pages 45-60, January/February 1990.

10

C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, New Jersey, 1985.

11

G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.

12

Daniel Jackson. Nitpick: A checkable specification language. In Proc. Workshop on Formal Methods in Software Practice, San Diego, CA, January 1996.

13

Rajashekar Kailar. Reasoning about accountability in protocols for electronic commerce. In Proceedings of the IEEE Symposium on Security and Privacy, pages 236-250, May 1995.

14

Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems: Second International Workshop, TACAS '96, pages 147-166, March 1996.

15

Formal Systems (Europe) Ltd. Failures Divergence Refinement--User Manual and Tutorial, 1993. Version 1.3.

16

Nancy Lynch, Michael Merritt, William Weihl, and Alan Fekete. Atomic Transactions. Morgan Kaufmann, San Mateo, CA, 1994.

17

K. L. McMillan. Symbolic model checking: An approach to the state explosion problem. Technical Report CMU-CS-92-131, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, 1992. Ph.D. thesis.

18

Roger M. Needham and Michael D. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993-999, December 1978. Also Xerox Research Report, CSL-78-4, Xerox Research Center, Palo Alto, CA.

19

A. W. Roscoe. CSP and determinism in security modelling. In Proceedings 1995 IEEE Symposium on Security and Privacy, pages 114-127, May 1995.

20

A.W. Roscoe and H. MacCarthy. A case study in model-checking CSP. submitted for publication, October 1994.

21

Marvin Sirbu and J. D. Tygar. NetBill: an internet commerce system optimized for network delivered services. IEEE Personal Communications, pages 34-39, August 1995.

22

J. D. Tygar. Atomicity in electronic commerce. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pages 8-26, May 1996.

23

Jeannette Wing and Mandana Vaziri-Farhani. A case study in model checking software systems. Science of Computer Programming, January 1996. To appear. Preliminary version in SIGSOFT Proc. of Foundations of Software Engineering, October 1995.