Security analysis of efficient (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 and on two more recent optimistic fair non-repudiation protocols. Attacks on all these protocols are presented and an improved version of the Zhou-Gollmann protocol is proposed.