Аннотация:This panel will discuss the properties appropriate to E-Commerce protocols, principally payment protocols, and the applicability of current formal analysis techniques to the development and verification of those protocols. Some of the requirements, and non-requirements, turn out to be surprising: for example, support for repudiation disputes is affected by commercial and consumer law, and is deliberately downplayed in some protocols. Other potential requirements such as whole-protocol integrity (as opposed to individual message integrity) are not obviously modelled by many existing formal analysis tools. Protocols being deployed in practice, such as VISA/Mastercard's SET, also include a significant number of optional elements and variants, whose combinatoric interaction makes formal analysis both more tedious and more desirable. We intend to stimulate both the analysis of proposed protocols and the development of analysis formalisms.
