Descripción: El objetivo es desarrollar e implementar un marco de trabajo y unas herramientas para la especificación, diseño y análisis sistemático de las transacciones que se realizan en las aplicaciones de comercio y gobierno electrónico. Con todo esto se pretende, no sólo producir protocolos de comunicación seguros, sino fundamentarlos en un formalismo que respalde y garantice la seguridad de dichos protocolos. Como punto final se contempla también la generación de código haciendo uso de estas herramientas.
Las metodologías y herramientas desarrolladas permitirán al diseñador de una aplicación de comercio o gobierno electrónico generar una especificación formal del protocolo con las propiedades de seguridad pertinentes; también se podrán usar para analizar protocolos ya existentes. Después de un análisis exitoso, estas herramientas y metodologías serán útiles para transformar esa especificación formal en el código final, generar baterías de pruebas para testear el código con respecto a los requerimientos iniciales y servicios de auditoría en tiempo real para comprobar que los participantes del protocolo se comportan de acuerdo a la descripción del protocolo.