Formal Analysis of Fairness in E-Payment Protocol Based on Strand Space

Fairness as one of most important properties in E-payment protocol, it is important to verify it through informal and formal analysis approach. In this paper, we present the procedure to analyze iKP protocol in terms of strand space model, which consists of three key steps: First, we use strand space terminology to create the bundle of iKP protocol. Second, we enumerate all possible traces of each participant's strand in the run process of iKP. Third, according to the definition of fairness, determine whether iKP satisfy fairness. Then, we present the algorithm to verify fairness of E-payment protocol in pseudo code and use this algorithm to analyze ISI protocol successfully. This algorithm allows us to automatically verify fairness of E-payment protocol.