Modeling and verifying non-repudiation protocols using extended Horn logic

This paper presents a method to verify the non-repudiation property and fairness of a non-repudiation protocol based on an extended Horn logic model. The authors describe the message communications in non-repudiation protocols using the logic rules of the extended Horn logic model, then model the fairness, the non-repudiation property, and the actions of honest users, malicious users and the authorities based on the extended Horn logic model in an algorithm to verify non-repudiation protocols. The authors verify the Zhou-Gollman protocol based on the extended Horn logic model show that Witness facts and Request facts are not matched, and show that the Zhou-Gollman protocol does not provide fairness. For real time operation, the system can not compare with every rule when X-revolution is executed. Thus, the fixed point computation was accelerated by dividing the rules into UnSolvedForm rules and SolvedForm rules.