A Cryptographically Sound Dolev-Yao Style Security Proof of an Electronic Payment System

proof of a comprehensive electronic payment system.  The payment
system is a slightly simplified variant of the 3KP payment system
and comprises a variety of different security requirements ranging
from basic ones like the impossibility of unauthorized payments to
more sophisticated properties like disputability.  We show that the
payment system is secure against arbitrary active attacks, including
arbitrary concurrent protocol runs and arbitrary manipulation of
bitstrings within polynomial time if the protocol is implemented using
provably secure cryptographic primitives.  Although we achieve
security under cryptographic definitions, our proof does not have to
deal with probabilistic aspects of cryptography and is hence within
the scope of current proof tools. The reason is that we exploit a
recently proposed Dolev-Yao-style cryptographic library with a
provably secure cryptographic implementation.  Together with
composition and preservation theorems of the underlying model, this
allows us to perform the actual proof effort in a deterministic
setting corresponding to a slightly extended Dolev-Yao model.