Authors: Nevin Heintze, Doug Tygar, Jeannette Wing, and Hao-Chi Wong
To appear in the Second USENIX Workshop on Electronic Commerce, 1996.
The full text of this paper is here (in PostScript).
The paper develops model checking techniques to examine NetBill and Digicash. We show how model checking can find atomicity problems by analyzing simplified versions of these protocols that retain crucial security problems. For our analysis we used the FDR model checker~\cite{fdr}. The submission is an extended abstract only.