Formal verification of cryptographic security proofs

PorJosé A. Alonso

Se ha publicado una tesis de verificación formal con Isabelle/HOL titulada Formal verification of cryptographic security proofs.

Su autor es Matthias Berg (de la Universidad de Sarre (en alemán: Saarland)) dirigido por Michael Backes.

Su resumen es

Verifying cryptographic security proofs manually is inherently tedious and error-prone. The game-playing technique for cryptographic proofs advocates a modular proof design where cryptographic programs called games are transformed stepwise such that each step can be analyzed individually. This code-based approach has rendered the formal verification of such proofs using mechanized tools feasible.

In the first part of this dissertation we present Verypto: a framework to formally verify game-based cryptographic security proofs in a machine-assisted manner. Verypto has been implemented in the Isabelle proof assistant and provides a formal language to specify the constructs occurring in typical cryptographic games, including probabilistic behavior, the usage of oracles, and polynomial-time programs. We have verified the correctness of several game transformations and demonstrate their applicability by verifying that the composition of 1-1 one-way functions is one-way and by verifying the IND-CPA security of the ElGamal encryption scheme.

In a related project Barthe et al. developed the EasyCrypt toolset, which employs techniques from automated program verification to validate game transformations. In the second part of this dissertation we use EasyCrypt to verify the security of the Merkle-Damgård construction – a general design principle underlying many hash functions. In particular we verify its collision resistance and prove that it is indifferentiable from a random oracle.

Formalization of basic linear algebra

PorJosé A. Alonso

Se ha publicado una tesis de máster de razonamiento formalizado en Isabelle/HOL titulada Formalization of basic linear algebra.

Su autor es Bhavisha M. Talsania (de la California State University, San Marcos).

Su resumen es

This thesis discusses the formalization of basic results from linear algebra up to the following theorems, using the computer proof checker Isabelle:

  • Theorem 1 (Basis Size Theorem): Suppose that V is a finite dimensional vector space. Then any two bases have the same number of elements.
  • Theorem 2 (Basis Characterization Theorem): Suppose that V is a vector space of dimension n. Then any spanning set has at least n elements, and any spanning set with exactly n elements is a basis. In addition, any linearly independent set of vectors has at most n elements, and any set of linearly independent vectors with exactly n elements is a basis.
  • Theorem 3 (Rank-Nullity Theorem): Let L : V1 → V2 be a linear map between finite dimensional vector spaces. Then the nullity of L plus the rank of L equals the dimension of V1 : dim(V1 ) = rank(L) + null(L).

Chapter 1 provides a discussion of informal and formal proofs and an introduction to the thesis topic. Chapter 2 provides a brief overview of the proof assistant Isabelle and it’s layout and syntax. Chapter 3 to Chapter 13 go into detail of the formalized proofs done in Isabelle. In Chapter 14, we end with remarks and conclusion of the thesis.

Reseña: Formalized algebraic numbers: construction and first-order theory

PorJosé A. Alonso

Se ha publicado una tesis de razonamiento formalizado en Coq sobre los números algebraicos titulada Formalized algebraic numbers: construction and first-order theory.

Su autor es Cyril Cohen dirigido por Assia Mahboubi y Benjamin Werner (de la Escuela Politécnica de París)

Su resumen es

This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in proof assistants, Coq in our case: the intuitionistic construction of real algebraic numbers together with the proof they form a real closed field, and the programming and certification of quantifier elimination procedures for the theories of algebraically closed fields and real closed fields. In order to reach those results, we brought multiple contributions to the toolboxes and formalization and proof methodologies in Coq. More particularly, we provide in Coq/SSReflect a framework to work with quotient types. We provide a complete library about ordered and normed number algebraic structures. We wrote a short implementation of Cauchy reals together with tactics to deal easily with reasoning using assertions of the form “let n be a big enough number”, commonly used in mathematical paper proofs. We also developed a short library of real polynomial analysis. A big part of our contributions is useful for the formalization of the proof of Odd Order Theorem and they also aim at helping to prove and certify more efficient quantifier elimination procedures on reals.

La correspondientes teorías en Coq se encuentran en aquí.

Reseña: Contributions to the formal verification of arithmetic algorithms

PorJosé A. Alonso

El pasado mes de septiembre se presentó una tesis sobre verificación formal con Coq titulada Contributions to the formal verification of arithmetic algorithms.

Su autor es Érik Martin-Dorel, dirigido por Micaela Mayero y Jean-Michel Muller.

Su resumen es

The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the “Table Maker’s Dilemma” (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of “Rigorous Polynomial Approximation”, allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel’s lemma that we have formalized for both univariate and bivariate cases. In particular, our “ISValP verifier” is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of “augmented-precision” FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x²+y²) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the “double-rounding” phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.

Las transparencias usadas en la presentación se encuentran aquí.

Reseña: Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2

PorJosé A. Alonso

Una de las líneas de trabajo en la automatización del razonamiento es la paralelización de las demostraciones. En dicha línea se inscribe la Tesis doctoral Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2 presentada por David L. Rager en la Univ. de Texas en Austin el pasado 20 de Agosto.

Su resumen es

Multi-core systems have become commonplace, however, theorem provers often do not take advantage of the additional computing resources in an interactive setting. This research explores automatically using these additional resources to lessen the delay between when users submit conjectures to the theorem prover and when they receive feedback from the prover that is useful in discovering how to successfully complete the proof of a particular theorem.

This research contributes mechanisms that permit applicative programs to execute in parallel while simultaneously preparing these programs for verification by a semi-automatic reasoning system. It also contributes a parallel version of an automated theorem prover, with management of user interaction issues, such as output and how inherently single-threaded, user-level proof features can be configured for use with parallel computation. Finally, this dissertation investigates the types of proofs that are amenable to parallel execution. This investigation yields the result that almost all proof attempts that require a non-trivial amount of time can benefit from parallel execution. Proof attempts executed in parallel almost always provide the aforementioned feedback sooner than if they executed serially, and their execution time is often significantly reduced.

Las transparencias de la presentación se encuentran aquí.