Formal Specification of Requirements for Payment Transactions in the SET Protocol

摘要

Payment transactions in the SET (Secure Electronic Transaction) protocol are described. Requirements for SET are discussed and formally represented in a version of NPATRL (the NRL Protocol Analyzer Temporal Requirements Language). NPATRL is language for expressing generic requirements, heretofore applied to key distribution or key agreement protocols. Transaction vectors and other new constructs added to NPATRL for reasoning about SET payment transactions are described along with properties of their representation.