___

a Security Protocol ANimator for AVISPA

___

Download SPAN+AVISPA in a VirtualBox disk (700Mo)

The SPAN+AVISPA video tutorial and PDF tutorial

 

 
CAS+
to HLPSL
protocol NeedhamSchroederPublicKey;
identifiers
A,B : user;
Na,Nb : number;
KPa,KPb : public_key;

messages
1. A -> B : {Na, A}KPb
2. B -> A : {Na, Nb}KPa
3. A -> B : {Nb}KPb

knowledge
A : A,B,KPa,KPb;
B : A,B,KPa,KPb;

session_instances
[A:alice,B:bob,KPa:ka,KPb:kb];








->

role Alice (A, B: agent,             
KPa, KPb: public_key,
SND, RCV: channel (dy))
played_by A def=
transition

0. State = 0 /\ RCV(start) =|>
State':= 2 /\ Na' := new() /\ SND({Na'.A}_KPb)
...

role Bob(A, B: agent,
KPa, KPb: public_key,
SND, RCV: channel (dy))
...


 HLPSL

to
Animation with SPAN
role Alice (A, B: agent,             
KPa, KPb: public_key,
SND, RCV: channel (dy))
played_by A def=
transition

0. State = 0 /\ RCV(start) =|>
State':= 2 /\ Na' := new() /\ SND({Na'.A}_KPb)
/\ secret(Na',na,{A,B})
...

role Bob(A, B: agent,
KPa, KPb: public_key,
SND, RCV: channel (dy))
...

 -> 




is a security protocol animator for HLPSL and CAS+ specifications. HLPSL is the language used for specifying cryptographic protocols for the AVISPA toolset and CAS+ is a light evolution of the CASRUL language. Version 1.6 of now permits to:

also includes a local graphical interface similar to the one of AVISPA.

is distributed under LGPL.



Version 1.6 – September 2017. Download VirtualBox disk (700Mo).

This is the simplest solution to have a complete and fully functional SPAN+AVISPA installation. First install Virtual Box, then import the .ova file using File>Import in VirtualBox.

This is a small update w.r.t. version of January 2017. The old version was using an outdated HLPSL parser. The updated version (many thanks to Laurent Vigneron) correctly uses "hash_func" instead of "function".

For older distributions in source or binary form, see the page for older versions.

SPAN: Copyright (C) 2006-2017 Yann Glouche, Thomas Genet, Olivier Heen, Erwan Houssay and Ronan Saillard.

AVISPA: Copyright (C) 2003-2006, see participants here.

The CAS+ Parser includes source code from the CASRUL tool
CASRUL: Copyright (C) 2001 Florent Jacquemard, Michael Rusinowitch and Laurent Vigneron.



Looking for older versions...



Publications

[HGH08] 
O. Heen, T. Genet, E. Houssay. Votre protocole est-il vérifié? In MISC 39, p 58--68, Février 2008.
[HGGP08] (pdf)
O. Heen, T. Genet, S. Geller and N. Prigent. An Industrial and Academic Joint Experiment on Automated Verification of a Security Protocol. In IFIP Networking  Workshop on Mobile and Networks Security, Singapore, May 2008.

[BGGH07] (pdf)
Y. Boichut, T. Genet, Y. Glouche and O. Heen. Using Animation to Improve Formal Specifications of Security Protocols. In Proceedings of SAR-SSI'07, 2007.
[GGHC06] (pdf)
Y. Glouche, T. Genet, O. Heen and O. Courtay A Security Protocol Animator Tool for AVISPA. In ARTIST2 Workshop on Security Specification and Verification of Embedded Systems , Pisa, May 2006.


Bug report and comments

thomas.genet@irisa.fr
http://www.irisa.fr/celtique/genet