Abstract:
The Secure Electronic Transaction (SET) protocol has been
jointly developed by Visa and MasterCard toward achieving secure
online-transactions. This paper presents formal verification of the Purchase
Request phase of SET, by using ENDL (extension of nonmonotonic
logic). The analysis unveils some potential flaws. To overcome
these vulnerabilities, some feasible countermeasures are proposed
accordingly during the validation. Also, the modelling of Purchase Request
is described to implement the mechanically model checking instead
of manual verification.
