Implementing a term rewriting engine for the EasyCrypt framework
Guillermo Ramos Gutiérrez · 2015
La sociedad depende hoy mas que nunca de la tecnologia, pero la inversion en seguridad es escasa y los sistemas informaticos siguen estando muy lejos de ser seguros. La criptografia es una de las piedras angulares de la seguridad en este ambito, por lo que recientemente se ha dedicado una cantidad considerable de recursos al desarrollo de herramientas que ayuden en la evaluacion y mejora de los algoritmos criptograficos. EasyCrypt es uno de estos sistemas, desarrollado recientemente en el Instituto IMDEA Software en respuesta a la creciente necesidad de disponer de herramientas fiables de verificacion formal de criptografia. En este trabajo se abordara la implementacion de una mejora en el reductor de terminos de EasyCrypt, sustituyendolo por una maquina abstracta simbolica. Para ello se estudiaran e implementaran previamente dos maquinas abstractas muy conocidas, la Maquina de Krivine y la ZAM, introduciendo variaciones sobre ellas y estudiando sus diferencias desde un punto de vista practico.---ABSTRACT---Today, society depends more than ever on technology, but the investment in security is still scarce and using computer systems are still far from safe to use. Cryptography is one of the cornerstones of security, so there has been a considerable amount of effort devoted recently to the development of tools oriented to the evaluation and improvement of cryptographic algorithms. One of these tools is EasyCrypt, developed recently at IMDEA Software Institute in response to the increasing need of reliable formal verification tools for cryptography. This work will focus on the improvement of the EasyCrypt’s term rewriting system, replacing it with a symbolic abstract machine. In order to do that, we will previously study and implement two widely known abstract machines, the Krivine Machine and the ZAM, introducing some variations and studying their differences from a practical point of view.