Game-Based Analysis of Multi-Party Non-Repudiation Protocols

Fairness and non-repudiation turn out to be increasingly important security services with the fast growth of electronic commerce on the Internet. We have made some game based analysis of multi-party non-repudiation protocols recently. We use alternating transition systems, a game based model, to model protocols and alternating temporal logic, a game based logic, to express requirements that the protocols must ensure. Fairness and non-repudiation of the MK multi-party non-repudiation protocol are automated analyzed by using Mocha, a model-checker that supports the alternating transition systems and the alternating temporal logic. Finally we have made some improvement of the protocol which enable it to have fairness and non-repudiation.