Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model

Se ha publicado en el JFR un artículo de razonamiento formalizado en PVS titulado Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model.

Sus autores son Mauricio Ayala Rincón y Yuri Santos Rêgo (de la Univ. de Brasilia).

Su resumen es

In this work, we present an algebraic approach for modeling the two-party cascade protocol of Dolev-Yao and for fully formalizing its security in the specification language of the Prototype Verification System PVS. Although cascade protocols could be argued to be a very limited model, it should be stressed here that they are the basis of more sophisticated protocols of great applicability, such as those which allow treatment of multiparty, tuples, nonces, name-stamps, signatures, etc. In the current algebraic approach, steps of the protocol are modeled in a monoid freely generated by the cryptographic operators. Words in this monoid are specified as finite sequences and the whole protocol as a finite sequence of protocol steps, that are functions from pairs of users to sequences of cryptographic operators. In a previous work, assuming that for balanced protocols admissible words produced by a potential intruder should be balanced, a formalization of the characterization of security of this kind of protocols was given in PVS. In this work, the previously assumed property is also formalized, obtaining in this way a complete formalization which mathematically guarantees the security of these protocols. Despite such property being relatively easy to specify, obtaining a complete formalization requires a great amount of effort, because several algebraic properties, that are related to the preservation of the balancing property of the admissible language of the intruder, should be formalized in the granularity of the underlying data structure (of finite sequences used in the specification). Among these properties, the most complex are related to the notion of linkage property, which allows for a systematic analysis of words of the admissible language of a potential saboteur, showing how he/she is unable to isolate private keys of other users under the assumption of balanced protocols. The difficulties that can arise in conducting this formalization are also presented in this work.

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

A fully automatic problem solver with human-style output

Se ha publicado un artículo sobre automatización del razonamiento titulado A fully automatic problem solver with human-style output.

Sus autores son Mohan Ganesalingam y Timothy Gowers.

Su resumen es

This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians. The program is part of a more general project, which we also discuss.

Proof assistant based on didactic considerations

Se ha publicado un artículo sobre el uso de sistemas de razonamiento en la enseñanza de la lógica titulado Proof assistant based on didactic considerations.

Sus autores son Jorge Pais y Álvaro Tasistro (de la Universidad ORT Uruguay, Uruguay).

Su resumen es

We consider some issues concerning the role of Formal Logic in Software Engineering education, which lead us to promote the learning of formal proof through extensive, appropriately guided practice. To this end, we propose to adopt Natural Deduction as proof system and to make use of an adequate proof assistant to carry out formal proof on machine. We discuss some necessary characteristics of such proof assistant and subsequently present the design and implementation of our own version of it. This incorporates several novel features, such as the display and edition of derivations as trees, the use of meta-theorems (derived rules) as lemmas, and the possibility of maintaining a set of draft trees that can be inserted into the main derivation as needed. The assistant checks the validity of each edition operation as performed. So far, it has been implemented for propositional logic and (quite satisfactorily) put into practice in courses of Logic for Software Engineering and Information Systems programs.

El artículo se ha publicado en Journal of Universal Computer Science.

On the role of formalization in computational mathematics

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

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).