2006-2007 AVISPA

The aim of the Avispa project is to provide the public with an industrial strength platform for automated validation of cryptographic communication protocols.For verification, the protocol is firstly modeled in the high-level language HLPSL. Then, a compiler translates the specification in an automatically processable format, called the IF format. At this point, the protocol's properties can be checked using different tools like model-checkers.

Dr. Heinrich Hördegen has developed various modules for the compiler of the Avispa project. Development language was Objective Caml, a functional programming language. In addition, he has developed parts of a Web interface that allows you to interactively verify communication protocols. Dr. Heinrich Hördegen has published several publications on issues of IT security.

The international project was a collaboration of the University of Genoa, ETH Zurich, the LORIA and Siemens AG. It was financed by the European Commission.

Selected Publications

Explicit Randomness is not Necessary when Modeling Probabilistic Encryption


Pseudo-Random Generator Based on Chinese Remainder Theorem