___

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.

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.

Publications
[Gen15] (pdf)(Bibliographic reference)
T. Genet. A Short SPAN+AVISPA Tutorial. Technical Report, Inria, 2015.

[GGHC06] (pdf)(Bibliographic reference)
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.

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

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

Bug report and comments

thomas.genet@irisa.fr
http://people.irisa.fr/Thomas.Genet/