Verificación automática de un protocolo de voto electrónico

Abstract

[ES] La seguridad y transparencia de los procesos electores son la garantía fundamental de la voluntad popular. Sin ellos es imposible la construcción y el mantenimiento de la democracia. Las nuevas tecnologías van integrándose en los procesos electorales lentamente, pero aún hay muchas resistencias y problemas que resolver. La propuesta de protocolos de voto electrónico ha de ir acompañada de métodos formales para la validación de estos protocolos. El protocolo TAVS es una aproximación elegante, sencilla y flexible para la implementación del voto remoto. Maude-NPA es una herramienta formal plástica y potente para poder llevar a cabo estas validaciones. En este trabajo se utilizará la Maude-NPA para hacer una primera aproximación a la validación formal de TAVS, demostrando los beneficios de este tipo de evaluación

[EN] The security and transparency of the electoral processes are the fundamental guarantee of the popular will. Without them, the construction and maintenance of democracy is impossible. New technologies are slowly being integrated into electoral processes, but there is still much resistance and problems to be solved. The proposal of electronic voting protocols has been accompanied by formal methods for the validation of these protocols. The TAVS protocol is an elegant, simple, and flexible approach for the implementation of remote voting. Maude-NPA is a plastic and powerful formal tool to be able to carry out these validations. In this work, the MaudeNPA was used to make a first approximation to the formal validation of TAVS, demonstrating the benefits of this type of evaluation.