Accountability logic for mobile payment protocols

Abstract

Accountability is one of the most important security properties of electronic commerce (e-commerce) protocols. It can be used to resolve disputes among involved parties. Several formal logics were proposed to analyze this property. However, they lack of reasoning about the accountability of symmetric cryptography which is necessary for analyzing mobile payment protocols. In this paper, we propose an extension of existing accountability logics which is capable to deal with both symmetric and asymmetric cryptographic messages. Moreover, we show that our logic is general in that party's requirements for payment transactions which are considered as goals of a payment protocol can be formalized by our logic.