So far, many proprietary solutions exist to facilitate online sales processes and they all share the need to obtain customer information and to perform a corresponding financial transaction. The Web Payment APIs are a set of specifications by the W3C Web Payments Working Group that aim to offer new and improved checkout and payment mechanisms for the Web. As these specifications strive to become the new standard for Web payments, security is a crucial aspect.
We have performed a rigorous, systematic formal analysis of the proposed Web Payment standards, based on the Web Infrastructure Model (WIM). The WIM is the most comprehensive formal model of the Web to date and serves as a framework to precisely analyze Web protocols, standards, and applications.
During our analysis of the Web Payment specification, we discovered several vulnerabilities, one of which even allowed a malicious merchant to charge a customer multiple times for the same transaction. This security flaw is caused by an imprecision in the specification, which we discovered when trying to prove security. We verified that the attack works in practice and notified the W3C Web Payments Working Group as well as the Chromium developers about our findings. We also proposed fixes for the problem, which have been adopted in the meantime. We have also incorporated these fixes in our formal model and have then formally proved that the fixed standard is secure.