LI2013: Presentación del curso de “Lógica informática”

PorJosé A. Alonso

En la primera parte de la clase de hoy, se ha presentado el curso Lógica Informática siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red:

En la segunda parte, se ha explicado la instalación y uso de Isabelle/HOL. Como ejemplo se ha resuelto el primer ejercicio de la 1ª relación. Finalmente se ha explicado cómo publicar la solución en la wiki.

Como tarea para la próxima clase, se ha propuesto la solución de los ejercicios de la 1ª relación.

On the role of formalization in computational mathematics

PorJosé A. Alonso

Se ha publicado un artículo sobre razonamiento formalizado en topología algebraica titutado On the role of formalization in computational mathematics.

Su autor es Julio Rubio (de la Universidad de la Rioja).

Su resumen es

In this paper, we will report on the developments carried out in Isabelle/HOL, ACL2 and Coq/SSReflect on Computational Algebraic Topology, in the frame of the ForMath European project. The aim is to illustrate, trough concrete examples, the role of formalization technologies in Computational Mathematics in general.

Theory exploration for interactive theorem proving

PorJosé A. Alonso

Se ha publicado un artículo sobre automatización del razonamiento titulado Theory exploration for interactive theorem proving.

Su autora es Moa Johansson (de la Universidad Técnica Chalmers en Gotemburgo, Suecia).

Su resumen es

Theory exploration is an automated reasoning technique for discovering and proving interesting properties about some set of given functions, constants and datatypes. In this note we describe ongoing work on integrating the HipSpec theory exploration system with the interactive prover Isabelle. We believe that such an integration would be beneficial for several reasons. In an interactive proof attempt a natural application would be to allow the user to ask for some suggestions of new lemmas that might help the current proof development. Theory exploration may also be used to automatically generate and prove some basic lemmas as a first step in a new theory development. Furthermore, when the theory exploration system is used as a stand-alone system, it should output a checkable proofs, for instance for Isabelle, so that sessions can be saved for future use.

El trabajo se presentó el 22 de julio en el AI4FM 2013 (4th International Workshop on Artifical Intelligence for Formal Methods).

Formal verification of language-based concurrent noninterference

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Formal verification of language-based concurrent noninterference.

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (de la Universidad Técnica de Munich, Alemania).

Su resumen es

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of non-interference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

El trabajo se ha publicado en el Journal of Formalized Reasoning.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

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.