Verificación automática del protocolo DP-3T asociado a las aplicaciones COVID-19

Abstract

[ES] Actualmente, vivimos en una sociedad ultra conectada que gira en torno al intercambio de información entre los dispositivos y usuarios de forma continuada. De la mano de la información va la privacidad y la confidencialidad de los datos, la cual debe de estar preservada y garantizada de la forma óptima y segura posible y en la que cada vez se está imprimiendo un mayor esfuerzo para trabajar en entornos más seguros, con la finalidad de evitar intrusismos o pérdida de datos. Debido a la situación ocasionada por la pandemia de COVID-19, el Gobierno de España ha puesto a disposición del ciudadano una aplicación capaz de controlar los contactos y contagios de una forma más personal y ágil, realizando un intercambio bidireccional de datos con todos los usuarios que posean la aplicación y que haya habido contacto, ofreciendo la posibilidad de notificar un caso de COVID-19 positivo simplemente pulsando un botón, de forma que se alerte a todos los contactos del usuario de una forma más rápida y efectiva. En este trabajo, vamos a analizar mediante la herramienta Maude-NPA la seguridad que tiene el protocolo DP-3T; protocolo desarrollado en respuesta a la pandemia que permite el intercambio de identificadores entre contactos a través de Bluetooth Low Energy, sobre el que se basa la APP RadarCovid, realizando una simulación de ejecuciones del protocolo y proponiendo varias situaciones donde un intruso podría obtener información para un uso indebido, y comprobar si existen ejecuciones del protocolo en la que pueda ocurrir alguno de los casos propuestos.

[EN] Nowadays, we live in a ultra connected society, that spins around data exchange between devices and user continuously. From data comes privacy and confidentiality, which should be preserved and guaranteed in the best and safest way possible and in which more and more effort is being made to work in safer environments, aiming to avoid data loss and intrusion. Due to the situation by the pandemic Covid 19, the Gobierno de España has given the citizen anapp able to control the contacts and contagion in a more agile and personal way, doing a bidirectional data exchange with all the users that has the application and have had contact, giving the possibility to notify a positive Covid 19 case with only pressing a button, alerting all the users that had been in contact in a quick and effective way. In this project, we are going to analyze through the Maude-NPA tool the DP-3T protocol; developed in response to the pandemic situation that allows id through Low Energy Bluetooth, in which the APP Radar Covid is based, doing an execution simulation of the protocol and proposing various situations where an intruder could get information for an undue use, and check if there is any execution of the protocol that can match the proposed cases.