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

Abstract. 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.