An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols
Wang Yu-min · Xi'an Jiaotong Daxue xuebao · 2010
A new formal analysis method using extended strand space is presented to weaken initial assumptions and to avoid state space explosion in analyzing the fairness of non-repudiation protocols.Signature operations are introduced into the strand space theory,so that the set of terms and sub-term relations are redefined in the strand space theory.Then,an extended strand space model is constructed by inducing the action of protocols to the penetrating strand,the origin strand,the receiver strand,and the trusted third party strand.The fairness of non-repudiation protocols is analyzed by verifying that the existence of the origin strand in the bundle is equivalent to the existence of the receiver strand in the bundle depending on the measure of theorem proving.Analyzing results on Zhou-Gollmann protocol show that the proposed method can weaken initial assumptions compared with the logic method,and can avoid state space explosion compared with the state space method.