Security analysis of (un-)fair non-repudiation protocols

An approach to protocol analysis using asynchronous product automata (APA) and the simple homomorphism verification tool (SHVT) is demonstrated on several variants of the well known Zhou-Gollmann fair non-repudiation protocol. Attacks on these protocols are presented, that, to our knowledge, have not been published before. Finally, an improved version of the protocol is proposed. This paper describes results of work within the project CASENET partly being funded by the European Commission under IST-2001-32446.