{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/78140"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/78140","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Automated security analysis of payment protocols","abstract":"Formal analyses have been used for payment protocol design and verification but, despite 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 combines 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 in full automation. An Alpha-Scenario is one in which a candidate protocol runs in a perfect environment without attacks from any intruders. The candidate protocol is correct if and only if all pre-conditions and post-conditions are met. PTGPA models actions and knowledge sets of intruders in a second, modified protocol that represents an attack scenario. This second protocol, called a Beta-Scenario, is obtained mechanically from the original candidate protocol, by applying a set of elementary capabilities from a Dolev-Yao intruder model. This thesis includes a number of case studies to demonstrate the feasibility and benefits of the proposed framework. Automated analyses of real-world bank card payment protocols as well as newly proposed contactless mobile payment protocols are presented. Security flaws are identified in some of the protocols; their causes and implications are addressed.","abstract_html":"Formal analyses have been used for payment protocol design and verification but, despite 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 combines 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 in full automation. An Alpha-Scenario is one in which a candidate protocol runs in a perfect environment without attacks from any intruders. The candidate protocol is correct if and only if all pre-conditions and post-conditions are met. PTGPA models actions and knowledge sets of intruders in a second, modified protocol that represents an attack scenario. This second protocol, called a Beta-Scenario, is obtained mechanically from the original candidate protocol, by applying a set of elementary capabilities from a Dolev-Yao intruder model. This thesis includes a number of case studies to demonstrate the feasibility and benefits of the proposed framework. Automated analyses of real-world bank card payment protocols as well as newly proposed contactless mobile payment protocols are presented. Security flaws are identified in some of the protocols; their causes and implications are addressed.","abstract_has_math":false,"creators":["Huang, Enyang"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Dept. of Civil and Environmental Engineering.","school":null,"contributors":[],"advisors":["George A. Kocur."],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012","date_published":"2012","updated_at":"2026-07-22T22:21:16Z","subjects":["Civil and Environmental Engineering."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/78140","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["George A. Kocur."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Dept. of Civil and Environmental Engineering."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Dept. of Civil and Environmental Engineering."]},{"key":"dc:creator","label":"Author","values":["Huang, Enyang"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2013-03-28T18:07:36Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2013-03-28T18:07:36Z"]},{"key":"dc:date.issued","label":"Date","values":["2012"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Civil and Environmental Engineering."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/78140"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (Ph. D. in the Field of Computer Engineering)--Massachusetts Institute of Technology, Dept. of Civil and Environmental Engineering, 2012.","Cataloged from PDF version of thesis.","Includes bibliographical references (p. 173-182)."]},{"key":"dc:description.abstract","label":"Abstract","values":["Formal analyses have been used for payment protocol design and verification but, despite 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 combines 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 in full automation. An Alpha-Scenario is one in which a candidate protocol runs in a perfect environment without attacks from any intruders. The candidate protocol is correct if and only if all pre-conditions and post-conditions are met. PTGPA models actions and knowledge sets of intruders in a second, modified protocol that represents an attack scenario. This second protocol, called a Beta-Scenario, is obtained mechanically from the original candidate protocol, by applying a set of elementary capabilities from a Dolev-Yao intruder model. This thesis includes a number of case studies to demonstrate the feasibility and benefits of the proposed framework. Automated analyses of real-world bank card payment protocols as well as newly proposed contactless mobile payment protocols are presented. Security flaws are identified in some of the protocols; their causes and implications are addressed."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Ph.D.in the Field of Computer Engineering"]},{"key":"dc:title","label":"Title","values":["Automated security analysis of payment protocols"]}]}],"canonical_facts":{"dc:contributor.advisor":["George A. Kocur."],"dc:contributor.department":["Massachusetts Institute of Technology. Dept. of Civil and Environmental Engineering."],"dc:contributor.other":["Massachusetts Institute of Technology. Dept. of Civil and Environmental Engineering."],"dc:creator":["Huang, Enyang"],"dc:date.accessioned":["2013-03-28T18:07:36Z"],"dc:date.available":["2013-03-28T18:07:36Z"],"dc:date.issued":["2012"],"dc:description":["Thesis (Ph. D. in the Field of Computer Engineering)--Massachusetts Institute of Technology, Dept. of Civil and Environmental Engineering, 2012.","Cataloged from PDF version of thesis.","Includes bibliographical references (p. 173-182)."],"dc:description.abstract":["Formal analyses have been used for payment protocol design and verification but, despite 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 combines 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 in full automation. An Alpha-Scenario is one in which a candidate protocol runs in a perfect environment without attacks from any intruders. The candidate protocol is correct if and only if all pre-conditions and post-conditions are met. PTGPA models actions and knowledge sets of intruders in a second, modified protocol that represents an attack scenario. This second protocol, called a Beta-Scenario, is obtained mechanically from the original candidate protocol, by applying a set of elementary capabilities from a Dolev-Yao intruder model. This thesis includes a number of case studies to demonstrate the feasibility and benefits of the proposed framework. Automated analyses of real-world bank card payment protocols as well as newly proposed contactless mobile payment protocols are presented. Security flaws are identified in some of the protocols; their causes and implications are addressed."],"dc:description.degree":["Ph.D.in the Field of Computer Engineering"],"dc:identifier.uri":["http://hdl.handle.net/1721.1/78140"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Civil and Environmental Engineering."],"dc:title":["Automated security analysis of payment protocols"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:21:16Z"}