Verification of Payment Protocols via MultiAgent Model Checking

  • M. Benerecetti
  • M. Panti
  • L. Spalazzi
  • S. Tacconi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2348)


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.


Model Check Security Requirement Security Protocol Propositional Atom Axiom Schema 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    M. Abadi and M. Tuttle. A semantics for a logic of authentication. In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, pages 201–216, 1991.Google Scholar
  2. 2.
    M. Bellare, J. A. Garay, R. Hauser, A. Herzberg, H. Krawczyk, M. Steiner, G. Tsudik, and M. Waidner. iKP-a family of secure electronic payment protocols. In Proc. of the First USENIX Workshop of Electronic Commerce, Berkeley, CA, USA, 1995. USENIX Assoc.Google Scholar
  3. 3.
    M. Benerecetti and A. Cimatti. Symbolic Model Checking for Multi-Agent Systems. In CLIMA-2001, Workshop on Computational Logic in Multi-Agent Systems, Paphos, Cyprus, December 1st 2001. Co-located with ICLP’01.Google Scholar
  4. 4.
    M. Benerecetti and F. Giunchiglia. Model checking security protocols using a logic of belief. In Proc. of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), Berlin, Germany, March 27th-April 1st 2000.Google Scholar
  5. 5.
    M. Benerecetti, F. Giunchiglia, M. Panti, and L. Spalazzi. A Logic of Belief and a Model Checking Algorithm for Security Protocols. In Proc. of IFIP TC6/WG6.1 International Conference FORTE/PSTV 2000, Dordrecht, The Netherlands, 2000. Kluwer Academic Publisher.Google Scholar
  6. 6.
    M. Benerecetti, F. Giunchiglia, and L. Serafini. Model Checking Multiagent Systems. Journal of Logic and Computation, 8(3):401–423, June 1998.Google Scholar
  7. 7.
    D. Bolignano. Towards the Formal Verification of Electronic Commerce Protocols. In Proceedings of 10th Computer Security Foundations Workshop, pages 133–146, 1997.Google Scholar
  8. 8.
    Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18–36, February 1990.Google Scholar
  9. 9.
    A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new Symbolic Model Verifier. In Proceedings of the International Conference on Computer-Aided Verification (CAV’99), Trento, Italy, July 1999.Google Scholar
  10. 10.
    E. Clarke, O. Grumberg, and D. Long. Model Checking. In Proc. of the International Summer School on Deductive Program Design, Marktoberdorf, Germany, 1994.Google Scholar
  11. 11.
    E. Clarke, S. Jha, and W. Marrero. A machine checkable logic of knowledge for specifying security properties of electronic commerce protocols. In Proc. of the Workshop on Formal Methods and Security Protocols, 1998.Google Scholar
  12. 12.
    E. A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 996–1072, Amsterdam, The Netherland, 1990. Elsevier Science Publishers.Google Scholar
  13. 13.
    N. Heintze, J. D. Tygar, J. Wing, and H. C. Wong. Model Checking Electronic Commerce Protocols. In Proc. of the 2 nd USENIX Workshop on Electronic Commerce, 1996.Google Scholar
  14. 14.
    R. W. Lichota, G. L. Hammonds, and S. H. Brackin. Verifying Cryptographic Protocols for Electronic Commerce. In Proc. of the 2 nd USENIX Workshop on Electronic Commerce, pages 53–65, 1996.Google Scholar
  15. 15.
    S. Lu and S. A. Smolka. Model Checking the Secure Electronic Transaction (SET) Protocol. In Proceedings of 7 th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, pages 358–365. IEEE Computer Society, 1999.Google Scholar
  16. 16.
    Mastercard and Visa. SET Secure Electronic Transaction Specification. Mastercard & Visa, May 1997. Available at
  17. 17.
    M. Panti, L. Spalazzi, and S. Tacconi. Verification of Security Properties in Electronic Payment Protocols. In IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS’ 02), Portland, Oregon, January 2002. Co-located with POPL’02.Google Scholar
  18. 18.
    P. Syverson and P. C. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 14–28, Oakland, CA, May 1994. IEEE Computer Society Press.Google Scholar
  19. 19.
    E. Van Herreweghen. Non-repudiation in SET: Open Issues. In Proceedings of the 4 th Conference on Financial Cryptography, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • M. Benerecetti
    • 1
  • M. Panti
    • 2
  • L. Spalazzi
    • 2
  • S. Tacconi
    • 2
  1. 1.Dept. of PhysicsUniversity of Naples ”Federico II”NapoliItaly
  2. 2.Istituto di InformaticaUniversity of AnconaAnconaItaly

Personalised recommendations