Modeling and Analysis of Multi-Party Fair Exchange Protocols

Fair multi-party exchange protocol is a new focus of research. We have made some researches for the modeling and analysis of multi-party fair exchange 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. This method is automated by using the model-checker MOCHA, a model-checker that supports the alternating transition systems and the alternating temporal logic. Fairness of multi-party exchange protocols are analyzed by using MOCHA.