Automated security analysis of payment protocols
Enyang Huang · DSpace@MIT (Massachusetts Institute of Technology) · 2012
Formal analyses have been used for payment protocol design and verification but, de-spite developments in semantics and expressiveness, previous literature has placed little emphasis on the automation aspects of the proof systems. This research develops an automated analysis framework for payment protocols called PTGPA. PTGPA com-bines the techniques of formal analysis as well as the decidability afforded by theory generation, a general-purpose framework for automated reasoning. A comprehensive and self-contained proof system called TGPay is first developed. TGPay introduces novel developments and refinements in the formal language and inference rules that conform to the prerequisites of theory generation. These target desired properties in payment systems such as confidentiality, integrity, authentication, freshness, acknowledgement and non-repudiation. Common security primitives such as encryption, decryption, digital signatures, message digests, message authentication codes and X.509 certificates are modeled. Using TGPay, PTGPA performs analyses of payment protocols under two scenarios