Automated security analysis of payment protocols
Thesis (Ph. D. in the Field of Computer Engineering)--Massachusetts Institute of Technology, Dept. of Civil and Environmental Engineering, 2012.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2013
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/78140 |
| _version_ | 1826197111175118848 |
|---|---|
| author | Huang, Enyang |
| author2 | George A. Kocur. |
| author_facet | George A. Kocur. Huang, Enyang |
| author_sort | Huang, Enyang |
| collection | MIT |
| description | Thesis (Ph. D. in the Field of Computer Engineering)--Massachusetts Institute of Technology, Dept. of Civil and Environmental Engineering, 2012. |
| first_indexed | 2024-09-23T10:42:40Z |
| format | Thesis |
| id | mit-1721.1/78140 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T10:42:40Z |
| publishDate | 2013 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/781402019-04-12T21:53:36Z Automated security analysis of payment protocols Huang, Enyang George A. Kocur. Massachusetts Institute of Technology. Dept. of Civil and Environmental Engineering. Massachusetts Institute of Technology. Dept. of Civil and Environmental Engineering. Civil and Environmental Engineering. 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). 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. by Enyang Huang. Ph.D.in the Field of Computer Engineering 2013-03-28T18:07:36Z 2013-03-28T18:07:36Z 2012 2012 Thesis http://hdl.handle.net/1721.1/78140 829118724 eng 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. http://dspace.mit.edu/handle/1721.1/7582 206 p. application/pdf Massachusetts Institute of Technology |
| spellingShingle | Civil and Environmental Engineering. Huang, Enyang Automated security analysis of payment protocols |
| title | Automated security analysis of payment protocols |
| title_full | Automated security analysis of payment protocols |
| title_fullStr | Automated security analysis of payment protocols |
| title_full_unstemmed | Automated security analysis of payment protocols |
| title_short | Automated security analysis of payment protocols |
| title_sort | automated security analysis of payment protocols |
| topic | Civil and Environmental Engineering. |
| url | http://hdl.handle.net/1721.1/78140 |
| work_keys_str_mv | AT huangenyang automatedsecurityanalysisofpaymentprotocols |