Interesante artículo (pdf) donde comentan algunas fallas de algunas plataformas de comercio electrónico. Recuerdo que hace unos años, me había tocado integrar ese tipo de cosas en aplicaciones existentes. En ese entonces habían bastantes cosas que las daba por seguras, haciendo evidentemente la aplicación propensa a los problemas que se describen en ese artículo.
Ahora veo necesario el uso de herramientas que permitan verificar formalmente este tipo de protocolos, si bien es cierto que puede que no sea perfecto o que haya errores al definir los modelos, al menos da cierto grado de garantía de que las propiedades que se prueban en este tipo de herramientas, se mantienen.