Tesis:
Automated Analysis of Cryptographic Constructions
- Autor: AMBRONA CASTELLANOS, Miguel
- Título: Automated Analysis of Cryptographic Constructions
- Fecha: 2018
- Materia: Sin materia definida
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: LENGUAJES Y SISTEMAS INFORMATICOS E INGENIERIA DE SOFTWARE
- Acceso electrónico: http://oa.upm.es/53392/
- Director/a 1º: BARTHE, Gilles
- Resumen: La criptografía asistida por ordenador es un área de investigación cada vez más popular que estudia la aplicación de métodos formales y técnicas de análisis automatizado a la criptografía. Permite que los criptógrafos deleguen en un ordenador algunos cálculos tediosos y propensos a errores (por ejemplo, partes rutinarias del análisis y validación de pruebas criptográficas, verificar cálculos complejos o explorar diferentes variantes de construcciones criptográficas). La criptografía asistida por ordenador ha sido utilizada con éxito para el análisis de varias primitivas, tanto en sistemas de clave-pública clásicos, como en sistemas de clave simétrica. Sin embargo, todavía no es muy claro cómo se podrían aplicar dichos métodos automatizados a las construcciones más recientes y avanzadas. En esta tesis se desarrollan nuevas técnicas y herramientas que amplían el alcance de la criptografía asistida por ordenador, con especial énfasis en la criptografía basada en pairings. La primera contribución se trata de un nuevo método (con su correspondiente implementación) para comprobar la seguridad de esquemas criptográficos (como structure-preserving signatures, message-authentication codes o asunciones definidas sobre bilinear pairings) de forma completamente automática y garantizando niveles de estandarizados de seguridad. Primero, nuestro nuevo método estudia cómo reducir la seguridad de dichos esquemas a la ausencia de soluciones a sistemas de restricciones. Después, desarrollamos técnicas para resolver dichos sistemas y demostrar que no admiten ninguna solución. La segunda contribución se centra en attribute-based encryption (ABE). Más concretamente, presentamos nuevos resultados sobre predicate encodings, una primitiva criptográfica que se utiliza para construir ABE de manera modular. Proponemos una caracterización puramente algebraica de la noción de privacidad de los encodings, que da lugar a diversas nuevas aplicaciones: combinadores lógicos de predicate encodings y técnicas de optimización que han resultado en construcciones de ABE mejoradas (con nuevas propiedades y mejor eficiencia). Además, nuestra caracterización hace posible nuestros siguientes resultados. La tercera contribución construye sobre las dos primeras. Proponemos, por primera vez en criptografía asistida por ordenador, técnicas y algoritmos (además de una implementación) para demostrar automáticamente la seguridad de construcciones ABE en el generic group model. Nuesto método permite estudiar experimentos de seguridad basados en indistinguibilidad (como require ABE), lo que supone un logro muy importante. Los trabajos anteriores sobre análisis automático se centraban especialmente en experimentos de seguridad computacional. Como última contribución también estudiamos la noción de indiferenciabilidad en construcciones de clave simétrica (como por ejemplo, diferentes variantes de Feistel networks o cifrados Even-Mansour). Al contrario que en nuestras primeras contribuciones, donde nuestro análisis estaba orientado a la búsqueda de demostraciones, aquí nos centramos en formalizar y sintetizar ataques. Desarrollamos métodos para automatizar la búsqueda de ataques. Primero, definimos formalmente el concepto de distinguidor universal y proporcionamos métodos para probar la universalidad de distinguidores candidatos. Después, desarrollamos e implementamos heurísticas que toman como entrada la descripción de una componente criptográfica y tratan de encontrar un ataque universal. Todas nuestras contribuciones comparten una metodología común: utilizamos técnicas de la teoría de métodos formales, expresando las construcciones criptográficas y sus definiciones de seguridad en un lenguaje simbólico. A continuación, proporcionamos teoremas que garantizan su validez computacional de forma que las conclusiones obtenidas simbólicamente se puedan extrapolar al modelo real sin símbolos. Además, demostramos la efectividad de nuestros métodos a través de varias herramientas que implementan nuestras técnicas y que han sido evaluadas en un amplio conjunto de ejemplos de la literatura. Los resultados presentados en esta tesis amplían el alcance de la criptografía asistida por ordenador, permitiendo el análisis de nuevas primitivas y garantizando mejores nociones de seguridad. ----------ABSTRACT---------- Computer-aided cryptography is an emerging area of research concerned with the application of formal methods and techniques from automated reasoning in cryptography. It allows cryptographers to outsource tedious or error-prone tasks to computers (including mundane parts of the analysis and validation of cryptographic proofs, verifying complex calculations or exploring design spaces of cryptographic constructions). Computer-aided cryptography has been successfully applied to the analysis of several primitives in classic public-key systems and symmetric schemes. However, it is still not clear how automated methods can be applied to more recent and advanced constructions. In this thesis we develop new techniques and tools to broaden the scope of computer-aided cryptography, with special emphasis on pairing-based cryptography. Our first contribution consists of a novel method (and an implementation) for automatically checking the security of cryptographic schemes (such as structure-preserving signatures, message authentication codes or assumptions defined over bilinear groups) in the generic group model, under strong standard definitions of security. Our work improves on previous works, which consider weaker security models. Our new approach allows us to reduce the security of schemes to the absence of solutions to a system of constraints. We then develop dedicated constraints-solving algorithms for testing that the systems are unsatisfiable. Our second contribution focuses on attribute-based encryption (ABE). More precisely, we present several new results about predicate encodings, a cryptographic primitive that can be used to build ABE in a modular way. We propose a purely algebraic formulation of the notion of privacy for predicate encodings, that leads to several new applications, such as logical combinations of predicate encodings and optimization techniques that resulted in improved ABE constructions (with extra features and better performance). Our third contribution builds on the first two. We provide, for the first time, computer-aided techniques and algorithms (plus an implementation) for automatically proving the security of attribute-based encryption constructions in the generic group model. Our method allows us to deal with indistinguishabilitybased security definitions (as is required for ABE), which is a very important achievement. Previous works on automated analysis mainly focused on computational security experiments instead. As a last contribution we also study indifferentiability of symmetric constructions (such as different variants of Feistel networks or Even-Mansour ciphers). Unlike in our previous contributions, where our analysis was oriented towards proof search, here we focus on formalizing and synthesizing attacks. We develop methods for fully automated attack search. First, we formally define the notion of universal indifferentiability distinguishers and provide methods for proving the universality of candidate distinguishers. Then, we develop (and implement) heuristics that take the description of a cryptographic component and try to find a universal distinguisher for it. All our contributions share a common methodology: we leverage techniques from formal methods, expressing cryptographic constructions and security definitions in a symbolic language. We then provide computational soundness theorems for such symbolic models that guarantee that the conclusions derived symbolically can be lifted to the actual non-symbolic model. We demonstrate the effectiveness of our approaches by developing several tools that implement our techniques, which are then evaluated on a wide range of examples from the literature. The results presented in this thesis expand the scope of computeraided cryptography, capturing stronger security notions and new settings.