AVISPA Thesis Proposals


A Unified Visual Language for the Specification of Security Protocols


In a world with a growing connectivity between numerous entities all over the world, the security of information has been positioned as one of the most important issues in communication networks. Formerly, the analysis of security was done using rather primitive mechanisms, often based on intuitions to find flaws in a security system. However, recently the complexity of the topic have evidenced the need of solid, mathematical and formal foundations that could give guarantees of the correctness of a security system.

This motivation has generated great research efforts within the concurrency theory community. Indeed, not only formal models where each aspect of security can be stated (the Spi calculus, SPL, or CSP are just but few examples) have been proposed, but also a great amount of applications based in formal grounds that perform security analysis in communication protocols have been developed.

This project aims at providing a unified visual language to specify security protocols. At the moment, each of application provides its own specification language but most of them rely on the Dolev-Yao (DY) model, a well-known threat model. In the DY, an open view of the network as well as a powerfull attacker capable to overhear and include new messages in the network are assumed. Some efforts have been started in order to provide a unique specification language ( i.e.: CAPSL, EVA, and HLPSL), however, none of them have succeeded in the establishment of a unique specification language, mostly due to their own views of the network (based on roles, or on logical formulae, to cite a couple of examples).

We believe that a visual formalism could be the appropriate layer where this integration can be done. In fact, visual modelling has been successfully used to show attacks in security protocols (e.g.: Chi-Spaces, the Avispa Tool or Scyther), but mostly none of them have been considered the visual specification of protocols.

The project will include the following activities:

  • A revision of previous efforts on the definition of formally-inspired visual languages as well as of related works in security.
  • A comparative analysis of the current specification languages (CAPSL, HPSL, EVA and others).
  • Based on the above, the definition of a vsual language for the specification of security protocols based on the Dolev Yao model.
  • Implementation of appropriate translations from the proposed visual language to some representative specification languages.

It will be interesting if to consider an integrated tool where the different frameworks of security can be integrated used the visual language proposed.


Some people have demonstrated their interest in this topic of research are:

  • Federico Crazzolara (Datev EG, Nurmberg).
  • Cas Cremers (ETH, Zurich)


  • C. Caleiro, L. Viganò, D. Basin, Deconstructing Alice and Bob, in Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005), ENTCS 135(1):3-22, 2005.
  • Sjouke Mauw: The Formalization of Message Sequence Charts. Computer Networks and ISDN Systems 28(12): 1643-1657 (1996)
  • Sjouke Mauw, Michel A. Reniers: An Algebraic Semantics of Basic Message Sequence Charts. Comput. J. 37(4): 269-278 (1994)
  • André Engels, Sjouke Mauw, Michel A. Reniers: A hierarchy of communication models for Message Sequence Charts. Sci. Comput. Program. 44(3): 253-292 (2002)
  • Federico Crazzolara, Giuseppe Milicia. Graphical Descriptions of Security Protocols, in Proceedings of the 1st Workshop on COnstraint & LOgic Programming in Security (COLOPS 2003), Mumbai, December 2003
  • Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drieslma, J. Mantovani, S. Mödersheim and L. Vigneron, A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols, in Proceedings of Workshop on Specification and Automated Processing of Security Requirements (SAPS 2004), 2004. download
  • The CAPSL Integrated Protocol Environment (postscript) by Denker, Millen, and Ruess; TIPE project final report and language reference document.
  • Rapport Technique EVA No 2, Langage de spécification de protocoles cryptographiques de EVA : syntaxe abstraite et sémantique, Jean Goubault-Larrecq, novembre 2001. PDF


Hugo A. López (http:www.hugolopez.phi.com.co)

Constraint Programming

Process Calculi

grupos/avispa/thesis_proposals.txt · Última modificación: 2011/01/24 15:30 (editor externo)
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki