A Formal Analysis of the Mimblewimble Cryptocurrency Protocol with a Security Approach

Una criptomoneda es una moneda digital que puede ser intercambiada por bienes y servicios. Las criptomonedas utilizan cadena de bloques (blockchains) públicas donde las transacciones se encuentran duplicadas y distribuidas en los nodos de una red de computadoras. Este mecanismo descentralizado es concebido para lograr confiabilidad en una red compuesta por nodos no fiables. La privacidad, el anonimato y la seguridad se han vuelto cruciales en este contexto. Por esta razón, los enfoques formales y matemáticos han ganado popularidad con el fin de garantizar la corrección de las implementaciones. Mimblewimble es una criptomoneda orientada a la privacidad con propiedades de seguridad y escalabilidad que la distingue de otras criptomonedas. En agosto de 2016, un usuario anónimo, bajo el seudónimo de Tom Elvis Jedusor (nombre en francés de Voldemort en la saga de Harry Potter), publicó un archivo de texto en el canal de chat IRC donde explicaba las bases de este nuevo protocolo. Mimblewimble está basado en Criptografía de Curvas Elípticas lo que permite verificar la validez de las transacciones sin revelar información alguna sobre el monto y las partes involucradas. Mimblewimble combina transacciones confidenciales y las técnicas de CoinJoin y cut-through para alcanzar mayor nivel de privacidad, seguridad y escalabilidad. En esta tesis, presentamos y discutimos estas propiedades de seguridad y describimos un enfoque basado en la verificación de modelos para alcanzar la certificación de la corrección de las implementaciones del protocolo. En particular, proponemos un modelo idealizado que es clave en el proceso de verificación descrito. Los principales componentes de nuestro modelo idealizado son las transacciones, los bloques y la cadena. Luego, identificamos y describimos precisamente las condiciones que nuestro modelo debe cumplir para asegurar la verificaciones de propiedades de seguridad relevantes de Mimblewimble. Además, analizamos el estado actual de sus dos más importantes implementaciones, Grin y Beam. Finalmente, presentamos conexiones detalladas entre nuestro modelo y las implementaciones en relación a la estructura de Mimblewimble y sus propiedades de seguridad.