TY - JOUR
T1 - Modeling and verifying non-repudiation protocols using extended Horn logic
AU - Xu, Chang
AU - Li, Zhoujun
AU - Guo, Hua
AU - Zhang, Fan
PY - 2012/10
Y1 - 2012/10
N2 - 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.
AB - 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.
KW - Extended Horn logic model
KW - Fairness
KW - Non-repudiation
KW - Solved-form fixed point
UR - http://www.scopus.com/inward/record.url?scp=84871121063&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:84871121063
SN - 1000-0054
VL - 52
SP - 1488
EP - 1495
JO - Qinghua Daxue Xuebao/Journal of Tsinghua University
JF - Qinghua Daxue Xuebao/Journal of Tsinghua University
IS - 10
ER -