Formal verification of fairness properties in Secure Electronic Transactions (SET) | |
| Author | Nguyen Trung Hieu |
| Call Number | AIT Thesis no.CS-03-13 |
| Subject(s) | SET (Computer network protocol) Computer network protocols |
| Note | A thesis submitted in partial fulfillment of the requirements for the degree of Master of Engineering, School of Engineering and Technology |
| Publisher | Asian Institute of Technology |
| Series Statement | Thesis ; no. CS-03-13 |
| Abstract | Secure electronic transaction protocol is an important security protocol used to secure bankcard payments on internet. Beside authentication, authority & privacy requirement this protocol needs to meet fairness requirement which ensures no protocol participant gains advantage over other. Non-repudiation is one of the most important properties in fairness requirement. Non-repudiation guarantees that merchant can not deny having sent the product and customer can not deny having received it. Existing version of SET does not support non-repudiation property when good is digital like software’s. This thesis proposes a new protocol which is based on original SET protocol and satisfies this requirement. To prove this new protocol satisfies fairness properties, Game based method proposed by Kremer is applied. This method uses alternating transition system to model protocol and alternating time temporal logic to express requirements. This method is automated by using the model checker MOCHA. However, in my verification process I find that using MOCHA tool directly is not correct. MOCHA tool verifies formula at initial state only, and lacks ability to verify formula at certain reachable state of system. In this thesis I have put efforts in direction to enhance the capability of this tool also. |
| Year | 2003 |
| Corresponding Series Added Entry | Asian Institute of Technology. Thesis ; no. CS-03-13 |
| Type | Thesis |
| School | School of Engineering and Technology (SET) |
| Department | Department of Information and Communications Technologies (DICT) |
| Academic Program/FoS | Computer Science (CS) |
| Chairperson(s) | Phan Minh Dung; |
| Examination Committee(s) | Guha, Sumanta;Huynh Trung Luong; |
| Scholarship Donor(s) | Petro Vietnam; |
| Degree | Thesis (M.Eng.) - Asian Institute of Technology, 2003 |