Analysis of accountability property in payment systems using strand space model

Abstract

Nowadays payment protocols are facing difficulties in its implementation, as the parties involved in the execution deny their performed actions. In this context, there should be a provision to link the action to the concerned party, which is addressed by the accountability property. In this paper, a new framework in strand space model for the analysis of accountability property is proposed that can overcome the drawbacks of the existing models. Strand space model is improved so that the analysis of accountability property of a payment protocol that is designed under symmetric key cryptosystem can be done. As a test example, symmetric key based BPAC, a bill payment protocol ensuring accountability is used. Fine-grained analysis of accountability property of BPAC protocol is carried out and proved its correctness using the automated support provided by CPSA along with the strong mathematical proof.