Departamento de Computación

En la última década, los emparejamientos bilineales se han utilizado para brindar soluciones eficientes y elegantes a varios problemas criptográficos emblemáticos. Sin embargo, hoy en día, el proceso de implementación de un protocolo basado en emparejamientos bilineales es en gran parte un proceso manual que se lleva a cabo por un equipo experimentado de diseñadores e implementadores, debido a que existen un puñado de propuestas reportadas para automatizar este proceso. Por otra parte, en muchos casos, surge la cuestión de si la versión implementada de un protocolo es fiel a la descripción criptográfica original. Esta tesis describe el análisis, diseño e implementación de un compilador que permite traducir las descripciones de protocolos criptográficos a sus versiones en lenguajes de programación estándar. Un componente crucial para el compilador que aquí se presenta, es el diseño del lenguaje formal LENPROC, el cual tiene suficiente expresividad para describir de manera intuitiva cualquier protocolo basado en el emparejamientos bilineales. Por lo tanto, el compilador que se presenta en este trabajo toma como entrada la descripción de un protocolo criptográfico basado en emparejamientos bilineales utilizando LENPROC, y posteriormente genera la implementación eficiente de la misma en lenguaje Magma y/o lenguaje C/C++. La implementación creada utiliza curvas Barreto-Naehrig con un nivel de seguridad de 126 bits.

Abstract

In the last decade, bilinear pairings have been used to devise efficient and elegant solutions to several emblematic cryptographic problems. However, as of today, the process of implementing a given pairing-based protocol is largely a manual process that must be carried out by an experienced team of designers and implementors, as there exist just a handful of reported proposals to automate this process. Moreover, in many cases, it arises the question of whether the implemented version of a given protocol is indeed faithful to its original cryptographic description. This thesis describes the analysis, design and implementation of a compiler tool that permits to translate cryptographic protocol descriptions into standard programming languages instantiations of them, which can be readily implemented in software platforms. One crucial component of the compiler tool presented here, is the design of the formal language LENPROC that has enough expressivity to be applied for the intuitive specification of any customary pairing-based protocol. Hence, the compiler presented in this work takes as input the description of a pairing-based cryptographic protocol given in LENPROC, and then it generates an efficient implementation of it in Magma and/or the C/C++ programming languages. All the schemes are instantiated using Barreto-Naehrig curves at a security level of 126 bits.