Verification of payment protocols via multiagent model checking

Abstract

The paper presents a logic of belief and time (called MATL) that can be used to verify electronic payment protocols. This logic encompasses its predecessors in the family of logics of authentication. According to our approach, the verification is performed by means of MultiAgent Model Checking Checking, an extension of traditional model checking to cope with time and beliefs. In this framework, principals are modeled as concurrent processes able to have beliefs about other principals. The approach is applied to the verification of the Lu and Smolka protocol, a variant of SET. The results of our analysis show that the protocol does not satisfy some important security requirements, which make it subject to attacks.