We present the full code for our model of NetBill and the digital cash protocol (lines beginning with ``-'' are comments). We also give some excerpts of the FDR verifications.
-
