___

a Security Protocol ANimator for AVISPA

___

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

The SPAN+AVISPA short tutorial and installation instructions

 

 
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 in source form. binary packages run on linux Linux, windowsWindows, macos MacOS and also provide binary versions of AVISPA verification tools.




Version 1.6 – September 15, 2015. Download VirtualBox disk (628Mo).

This is the simplest solution to have a complete and fully functional SPAN+AVISPA installation. First install Virtual Box.




Binary packages (no longer supported) --  Including binary versions of , the AVISPA Tools, plus documentation



Source package ( only) distributed under LGPL





See the documentation for more information about SPAN and the README.txt file for details about installation and (if necessary) compilation.


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

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