Title :
Equational approach to formal verification of SET
Author :
Ogata, Kazuhiro ; Futatsugi, Kokichi
Author_Institution :
NEC Software Hokuriku, Ltd., Japan
Abstract :
We have formally verified that a payment protocol, which is an abstract SET payment protocol but retains the essential part of the SET payment protocol, has several desired properties. Among the properties are that, if the payment gateway authorizes a payment, then both cardholder and merchant concerned always agree on the payment, and at this time, the two principals also agree on the transaction amount.
Keywords :
algebraic specification; authorisation; electronic money; formal verification; protocols; rewriting systems; theorem proving; abstract SET payment protocol; algebraic specification; cardholder; equational approach; formal verification; interactive theorem proving; merchant; payment gateway; rewriting; security; transaction amount; Algebra; Equations; Formal verification; Logic; National electric code; Protocols; Security; Software quality; Specification languages; State-space methods;
Conference_Titel :
Quality Software, 2004. QSIC 2004. Proceedings. Fourth International Conference on
Print_ISBN :
0-7695-2207-6
DOI :
10.1109/QSIC.2004.1357944
