User Manual
Contents
1. C C Qt N e 11 12 14 SPAN a Protocol Animator for AVISPA Page 13 000 X SPAN 1 4 Protocol Verification NSPK hlpsl File IX SPAN 1 4 Protocol Simulation NSPK hlpsl Trace File auto gen trc Loadint Trace Files Modes Variables monitoring lt Previous step Next step gt J Untype intruder alice bob Incoming events i 0 a 3 b 4 inonce 1 a ki inonce 1 Past events Altalice 6 gt Intruder_ 0 Intruder_ 0 gt bob 4 mum bob 4 gt Intruder 0 Intruder 0 gt alice 6 abire cB cs Int Ruder DIS nonce 2 ki um di AT _ gt 2 u pl Intruder knowledge Compose knowledge Figure 13 Automatic construction of the MSC for attack over Needham Shroeder public key protocol LS export A MISC 9 ne nee RP ae MA 16 Display modes for messages 195 SPAN a Protocol Animator for AVISPA Page 14 Load and save an execution trace of a protocol Sua MEC Protocol Simulation t hlpsl E 2 Variables monitoring step1 _ Untyped variables 3 Step2 ing events user 3 ERROR A e mz gt user 3 ERROR pene Print schema device 4 PUSH A Emission PUSHJAJ PUSH B _ device 5 PUSH B E Quit Steps Em15s1on WAIT D qj plexp a nonce inv Kpubb p epe Past events SORTS RM LP SAP UGE ONCE 5 PF INV PR2. 1 1 SPAN overview 1 1 What is AVISPA Avispa ABB 05 avi is now a commonly used verification tool for cryptographic protocols The main advantage of this tool is the ability to use different verification techniques on the same protocol specification The protocol designer interacts with the tool by specifying a security problem ie a protocol paired with a security property that the protocol is expected to achieve in the High Level Protocol Specifica tion Language HLPSL for short Ohe05 The HLPSL is an expressive modular role based formal language that is used to specify control flow patterns data structures alternative intruder models and complex security properties as well as different cryptographic primitives and their algebraic properties These features make HLPSL well suited for specifying modern industrial scale protocols SPAN HLPSL SATMC TAASP Figure 1 AVISPA system architecture and SPAN Then the HLPSL specification is translated into an Intermediate Format IF which is used by the various verification tools embedded in AVISPA OFMC the On the Fly Model Checker BMV05 CL Constraint Logic based model checker Tur06 SATMC SAT based Model Checker ACO5 and TA4SP Tree Automata based Automatic Approximations for the Analysis of Security Protocols BHK04 The role of SPAN is to symbolically execute a HLPSL protocol specification This turns out to be useful when writing HLPSL so as to have a bett
3. 2 77 _ERBT RP 9 nonce 5 device 4 PUSH A Emibsion exp G xX ReCh inv 53 gt user 3 WATT D Step q a device 5 PUSH B device 4 gt device 5 exp G X Emission PREFIHAL D ERROR device 5 gt device 4 exp 6 Y device 4 gt device 5 exp G device 5 gt uscr 3 PREFIWNAL D Y Hi 5 Figure 14 Load and save an execution trace of a protocol Trace Files Modes Variables monitoring Open trace axt step gt Untyped variables Save trace oming events Save trace as 3 user 3 Exporeschaemalas m user 37 Print schema device device 5 Step2 Steps Step4 Steps expig nonce 3 _ invi pk 4 Jexp expig nonc onfexp G Ch exp G Y inv Kpubb nonce 3 _inv pkK 2 _exp amp Steps p g nonce 3 1 3 gt device 4 Emibbsion f exp G xX ReCh _invi Kpuba exp ReCh X ERRORGJ 4 gt user 3 WAIT D step 3 gt device 5 PUSH B prefina Y device2 1 43 gt device 5 exp G x Emission PREFIMAL D ERROR 1 53 gt device 4 exp G Y 4 gt device 5 f exp G 1 53 gt user 3 PREFINAL D Figure 15 Export a MSC References ABB 05 A Armando D Basin Y Boichut Y Chevalier L Compagna J Cuellar P Han kes Drielsma P C H am O Kouchnar
4. built using OFMC CL ATSE 4 2 Basic Protocol Animation Starting from such an HLPSL specification such as the one given in Section 3 SPAN helps to build one possible MSC corresponding to that specification SPAN can represent one or more sessions of the protocol in parallel according to the informations given in the role environment Then MSCs are produced interactively with the user At every moment SPAN proposes to the user to choose between all the transitions for which a message can be sent by a principal and received by another This approach makes it possible to resolve interactively all the choices that may arise during the construction of MSC Non deterministic protocols choices between two transitions to trigger in two different sessions etc The execution of a protocol s transition generally adds a transition on the MSC Figure 4 shows a partial execution of a protocol where the frame Incoming events contains all the transitions that can be currently fired by double click and the frame Past events contains the list of all transitions already fired SPAN a Protocol Animator for AVISPA Page 5 Editable zone for HLPSL specification loaded by the user Open or Save an HLPSL specification or Quit the application e 068 X SPAN 1 4 Protocol Verification NSPK hlpsl Open File la B agent A Save Ka Kb public key Save as SND RCV channel dy defz F ize
5. made explicit SPAN a Protocol Animator for AVISPA Page 4 role session A B agent Ka Kb public_key def local SA RA SB RB channel dy composition alice A B Ka Kb SA RA bob A B Ka Kb SB RB end role Finally the environment used for protocol execution is defined where i denotes the intruder The environment also defines the initial knowledge of the intruder and the initial setting for the sessions 1 e how many sessions are runned and who run them role environment def const a b c d agent ka kb ki kc kd public key intruder knowledge la b ka kb kc kd ki inv ki composition session a b ka kb N session c d kc kd session a i ka ki end role In the example above four honnest agents are defined namely a b c and d and the intruder knows all the public keys as well as its own private key inv ki For more details about HLPSL refer to avi Ohe05 4 SPAN reference manual 4 1 Local Graphical User Interface for AVISPA As shown in figure 3 SPAN comes with a local version of the web graphical interface of AVISPA It looks the same and provides the same features simple editing of protocol specifications selection and configuration of the AVISPA verification back ends and two buttons those ones are new Protocol simulation honnest agents alone Intruder simulation honnest agents and an intruder and Attack simulation same layout as Intruder simulation but attacks are automatically
6. see Figure 10 where in the current session the value of the nonce NA is nonce 1 Since Kg is also known by the intruder using the message construction interface the user can build the message LNA4 A xk whose value in the current session is nonce 1 a _ kb see Figure 10 I A B N1 A K The intruder J sends NA Ajx to Bob B Thus Bob thinks that the message comes from Alice though it comes from the intruder Then Bob continues to execute the protocol with A using the nonce N4 that A has created for initiating a communication with the intruder Alices continues to execute the protocol with the intruder see Figure 12 SPAN a Protocol Animator for AVISPA Page 10 Compose an intruder knowledge Compose amp Pair Scrypt Exp w Xor nonce 1 a Add nonce l a nonce 1 bob 10 can receive Na i kb type text agent public key nonce 1 E tnonce 1 a _ki alice 6 can receive nonce 1 Nb ka type text text public key nonce 1 a ki bob 4 can receive Na a kb type Na a kb Add knowledge composed with this pattern F Na a E nonce 1 a Clear gt Cancel Figure 10 The intruder compose a message for Bob Thus we can build the original attack found by G Lowe Low96 AI LUNA Atk I A gt B NA AK BoA UNA NBI KA AI NB K I A gt B Ns 4 5 The attack simulation In the previous section we show how to b
7. 1 A A Protocol animator Quit Nb text init State 0 Protocol animator transition x with intruder 0 State 0 X RCV start gt State 2 Na new SND Na A Kb secret Na 7 Pi ml witness A e neo DOVE the ALPSL Automatic construction State 4 X SND 1Nb I rest specification of attack simulations HLPSL to IF translator Save file View file Protocol Intruder Attack simulation simulation simulation Is Options PSL _ Session Compilation HLPSL2IF Choose Tool option and Defth press execute IF Execute Path OFMC ATSE SATMC TA4SP Reload the HLPSL specification Execution of the verification tool selected by the user on the Verification Tools HLPSL specification Options of the selected verification tool Figure 3 Details of the general verification graphical interface 4 3 Variables Monitoring SPAN also includes the possibility to check the values at every moment of the variables of each principals the user chooses the variables of each roles he wants to monitor It is possible to control the values of variables In the item menu Variables Monitoring the user chooses the role for which he wants to control the variables Then among all the variables of a given role he can choose the variables to monitor See Figure 5 a Finally the user can double click on the rectangular click zones displayed in the MSC in order to display the values at a given st
8. A Trace Files Modes Variables monitoring Protocol Simulation NSPK txt Trace File nspk trace Previous step Untyped variables Intruder 0 alice 3 bob 4 mu 7 Incoming events MN alice 3 gt Intruder_ 0 Ma A nonce l a ki xL 0 l1 gt Past events alice 6 Intruder 0 Na A Intruder 0 gt bob 4 nonce 1 bob 4 gt Intruder 0 Na Nb _ Intruder 0 alice 6 nonce alice 6 gt Intruder 0 Nb K CON DTK ND e mom FR a N nonce l nonce 2 ka nonce l a kb alice 6 Figure 12 The man in the middle attack continued the intruder is between Alice and Bob List of Figures AVISPA system architecture and SPAN Local version of the AVISPA web interface Details of the general verification graphical interface The SPAN animator interface during an interactive execution Variables monitoring Simulation with the intruder Intruder message construction interface The initial intruder s knowledge Alice starts the protocol with the ade ii at hos The intruder compose a message for Bob Load and save an execution trace of a protocol Bob receives a message from the intruder sad of Alice m The man in the middle attack continued the intruder is en Mies 2nd Bob Automatic construction of the MSC for attack over Needham Shroeder public key protocol 13 O O OO
9. INRIA IRISA LANDE Project SPON a Security Protocol ANimator for AVISPA Version 1 5 User Manual September 2008 Yann GLOUCHE Thomas GENET and Erwan HOUSSAY IRISA Universit de Rennes 1 SPAN a Security Protocol ANimator for AVISPA Copyright Yann GLOUCHE Thomas GENET and Erwan HOUSSAY 2006 2008 SPAN uses the following libraries e HLPSL2IF Laurent Vigneron 2005 e Matching modulo exp and xor part of CL ATSE Mathieu Turuani 2005 Contents 1 SPAN overview 1 La WWhatas AVISA a ue eub amp ar aa a A RA 1 1 2 Availability License and Installation e 2 or Bue reDOPt and MO rMatiOM a q do XC VERE Ge o e uude de Bee eS 3 2 Installation 3 3 Specification Language 3 4 SPAN reference manual 4 4 1 Local Graphical User Interface for AVISPA 4 AD BASIC Protocol Animation wx 52s Date o PRE be pc VL Do ee 4 4 Ac Variables MOBIUOPIBE ue sa ae web d wd cR A AAA AAA does 5 A Te UGE SI AO 3S idee Soe ek cat iere eee dose Oe e e a 4e oS E dos 6 ZI OSGPIDDIOD amados a RA m cob s aa ess A AAD MON ODOSHSC LA auk AC ap ara A a ew en Tete do 8 T5 Che sttack simulatio du SEL SR SSL A OY e REIN acd d 10 Zob iDOSCEIDUOB is RUE e des a RA o Se vb dar 10 452 EAMPDI OPUS lt 8 4 465 LIEN yum ur pu LT A ode idee md 11 4 6 Load Save Print Export and Specific display modes 11 Figure list 11 SPAN a Protocol Animator for AVISPA Page
10. art of the interface proposes relevant message patterns messages that are likely to be received by the other principals in the current protocol step Once a pattern is selected in the lower part of the interface the user can select relevant informations to fill the gaps relevant w r t type message structure and intruder knowledge This permits to quickly reconstruct the MSC of a known attack SPAN a Protocol Animator for AVISPA Page 8 on a protocol or with a little expertise to find new ones Add a pair an exponential expression a xor expression or an encrypted message in the intruder s knowledge from the current intruder s knowledge Compose an intruder knowledge Compose amp Pair Scrypt Exp xor Add nonce 1 a nonce 1 nonce l a ki a b ka kb inv ki bob 10 can receive Ma i kb type text agent public key alice 6 can receive Na Nb ka type text text public key bob 4 can receive Na a kb type Ma aj kb Add knowledge composed with this pattern Na t nonce 1 5e a message nonce 1 2 nonce 1 na na patterns nb nb Cancel Figure 7 Intruder message construction interface 4 4 2 How to use it Recall the protocol given in Section 3 Here are the basic data of the protocol e KA and KB are two publics keys e inv K 41 and inv K pg are two privates keys e NA and Np are nonces The initial knowledge of the intruder con
11. ce 1 y e Coma gt Intruder knowledge A nonce 1 a _kb nonce 1 a nonce 1 nonce l a ki a EI b ka kb inv ki 1 bob 4 alice 6 Emission MB A Kb Figure 11 Bob receives a message from the intruder instead of Alice Once the MSC of the attack has been built in the intruder simulation interface you can play with it go backward forward see intruder s knowledge monitor variables and also save it like any other MSC protocol simulation 4 5 2 Example of use On the protocol given in Section 3 the automatic tools OFMC CL ATSE find the same man in the middle attack It can be automatically built as a MSC by clicking on the attack simulation button see Figure 13 4 6 Load Save Print Export and Specific display modes Save Load For a given protocol a constructed MSC can be saved reloaded and replayed in SPAN See Figure 14 Print Export The MSCs can be exported in postscript format or PDF format to be printed or integrated in other documents See Figure 15 Display mode Using the options of the Modes menu it is possible to display additionnal informations on the MSC the message pattern of the sender the message pattern of the receiver all the message sendings on the network useful when several messages are sent at once Each of these elements can be drawn or not on the MSC See Figure 16 SPAN a Protocol Animator for AVISP
12. cular MSC corresponding to the HLPSL specification SPAN a Protocol Animator for AVISPA Page 2 e 06 X SPAN 1 4 Protocol Verification NSPK hlpsl File role alice A B agent PA Ka Kb public key SND RCV channel dy played_by A def local State nat Na Nb text init State 0 transition DO State 0 RCV start gt State 2 Na new SND Na A Kb A secret Na na A BY witness A B bob alice na Na 2 State State 2 RCV Na Nb Ka gt 4 SND INb Y Kb request A B alice bob nb Nb end role 353535757575 757575 57575 75 5757575 5757575 5 EEE 56 5 5 EEE EEE 56 5 5 55 5 5 55 5 5 5 55 5 5 55 5 5 55 55 55 5555 5575 role bob A B agent Ka Kb public key SND RCV channel dy played by B def local State nat Na Nb text init State 1 Protocol Intruder Attack Save file iew fi 1 dd cse simulation simulation simulation Tools THIERS HLPSL2IF Choose Tool option and press execute IF OFMC ATSE SATMC TA4SP Execute Figure 2 Local version of the AVISPA web interface e Intruder Simulation for simulating the protocol with an active passive intruder e Attack Simulation for automatic building of MSC attacks from the output of either OFMC or CL ATSE tools When an intruder is under concern after each step of protocol execution SPAN shows the current intruder knowledge and proposes to construct and send malicio
13. enko J Mantovani S Modersheim D von Ohe imb M Rusinowitch J Santos Santiago M Turuani L Vigano and L Vigneron The AVISPA Tool for the automated validation of internet security protocols and applications SPAN a Protocol Animator for AVISPA Page 15 alice 3 bob 4 Emission alice bob 4 Modes Na A Kb E view messages emissions view sender pattern message alice bob 4 view real message alice bob 4 view sender pattern in principal position nonce l a kb view receiver pattern message alice 3 bob 4 Na A Kb Figure 16 Display modes for messages In K Etessami and S Rajamani editors 17th International Conference on Computer Aided Verification CAV 2005 volume 3576 of Lecture Notes in Computer Science pages 281 285 Edinburgh Scotland 2005 Springer AC05 Alessandro Armando and Luca Compagna An optimized intruder model for sat based model checking of security protocols Electr Notes Theor Comput Sci 125 1 91 108 2005 avil Avispa a tool for Automated Validation of Internet Security Protocols http www avispa project org BHK04 Y Boichut P C H am and O Kouchnarenko Automatic Approximation for the Veri fication of Cryptographic Protocols In Proc AVIS 2004 joint to ETAPS 04 Barcelona Spain 2004 BMV05 David A Basin Sebastian M dersheim and Luca Vigan Ofmc A s
14. ep SPAN a Protocol Animator for AVISPA Page 6 Protocol Simulation A SETE Trace Files Modes Variables monitoring MISC lt Previous step Nextstep gt Untyped variables user 3 device 4 device 5 i Incoming events E Incoming events device 4 gt user 3 ERROR Stepl device 5 gt user 3 ERROR push devicel f user 3 gt device 4 PUSH A Emission PUSH A PUSH B user 3 device 5 PUSH B Step2 s Step3 Emission WUSH B step4 Past events Past events user 3 gt device 4 PUSH A device 4 gt user 3 WAIT D user 3 gt device 5 PUSH B device 4 gt device 5 exp G X device 5 gt device 4 exp G Y device 4 gt device 5 exp G device 5 gt user 3 PREFINAL D pal ae Emissiion exp G Ch exp G Y exp g nonce 1 expi g Emission PREF INE Figure 4 The SPAN animator interface during an interactive execution Variables of alice 3 Unelect all Select all OK a Variables selection alice 3 bob 4 Step1 nonce l a kb nonce 1 Step2 nonce l nonce 2 ka nonce 2 nonce 1 Step3 inonce 2 kb b Content of variables displayed in the MSC Figure 5 Variables monitoring 4 4 The intruder simulation Steps exp exp q nonc i
15. er understanding of the specification check that it is executable and that it corresponds to what is expected Figure 1 depicts the overall architecture of the system including SPAN The initial development of the SPAN tool was done in collaboration with Olivier Heen and Olivier Courtay of Thomson R amp D France GGHCO06 Since HLPSL is a far more expressive language than basic Alice amp Bob notation writing an HLPSL specification is still not an easy task In HLPSL protocols are defined role by role rather than message by message like it is done using Alice amp Bob notation As a result HLPSL specifications are far less ambiguous but more difficult to read Thus it is sometimes difficult for the protocol designers to figure out if the HLPSL specification they wrote corresponds to the Alice amp Bob protocol they had in mind SPAN helps in interactively producing Message Sequence Charts HT03 MSC for short which can be seen as an Alice amp Bob trace from an HLPSL specification SPAN can represent one or more sessions of the protocol in parallel according to the informations given in the role environment Then MSCs are produced interactively with the user SPAN also includes the possibility to check the values at every moment of the variables of each principals the user chooses the variables of each roles he wants to monitor The three modes of SPAN are e Protocol Simulation for simulating the protocol and build a parti
16. nv Kpubb steps nonce 3 _inv pk 2 _exp dxp g nonce 3 Emipsion ftexp G X ReCh inv Kpuba exp ReCh X ERROR device2 In this section we describe the intruder simulation interface The purpose of this interface is to provide a way to build by hand attacks over protocols Indeed the automatic verification tools always end up with the smallest attack that can be found on a protocol Note that the attacks found by OFMC CL ATSE can be automatically loaded as MSC in the intruder simulation interface see section 4 5 However it is sometimes useful to represent or to try other attacks This is the purpose of the manual SPAN a Protocol Animator for AVISPA Page 7 intruder simulation interface we know present 4 4 1 Description It is possible to simulate an intruder who can receive all messages store them in its knowledge decrypt information if he has the key build new messages and send them to any other agent In HLPSL the intruder is named 2 and his initial knowledge is explicitely defined in the specification intruder_knowledge After each step of the protocol execution when the intruder receives a message he can automatically deduce a new knowledge from its current knowledge and this new message see Figure 6 For example if intruder knowledge m _k where m is a message and k is a symmetric key resp a public key then if the intruder receives k resp inv k then he is abble to deduce and s
17. rns data structures alternative intruder models and complex security properties as well as different cryptographic primitives and their algebraic properties We give a flavour of HLPSL using the specification of the Needham Schroeder Public Key proto col NS78 1 AS B N14 A eg 2 B A 1NA Nn 3 A B iNpiIx HLPSL specifications are based on role descriptions i e finite state automata where transitions are fired when a message is sent or received With regards to Alice amp Bob notation HLPSL makes internal state of roles nounce generation message sending and reception explicit Here is an example of a basic role decalaration extracted from the HLPSL specification of this protocol role alice A B agent Ka Kb public key SND RCV channel dy played by A def local State nat Na Nb text init State O transition 0 State O RCV start gt State 2 N Na new SND Na A _ Kb 2 State 2 RCV Na Nb _Ka gt State 4 SND Nb _Kb end role role bob A B agent Ka Kb public key SND RCV channel dy played by B def local State nat Na Nb text init State 1 transition 1 State 1 RCV Na A Kb gt State 3 N Nb new N SND Na Nb Ka 3 State 3 RCV Nb _Kb gt State 5 end role Then roles are composed together in sessions where the knowledge shared between the roles public keys for instance are
18. tains all the public keys as well as its own public and private key see Figure 8 T he protocol can be attacked if Alice wants to start a protocol session with the intruder Alice starts the protocol with the Intruder and thus use its public key A to cipher the message AI LUNA Al k This first step can be simulated in SPAN see Figure 9 SPAN a Protocol Animator for AVISPA Page 9 v Protocol Simulation NSP K txt BEA Trace Files Modes Variables monitoring MSC lt Previous step t st Untyped variables Intruder 0 alice 3 bob 4 alice 6 bob 16 2 Incoming euents alice 3 gt Intruder_ 0 Na A alice 3 gt bob 4 Ma A Kb alice 6 gt Intruder_ 0 Na A E 1 105 15 MEZ Past events IA lt A The intruder knows Intruder knowledge J the private key inv ki a and the public key kb inv J Protocol Simulation NSPK txt Trace Files Modes variables monitoring MSC Previous step Untyped variables Intruder 0 alice 3 bob 4 alice 6 bob 10 Incoming events alice 3 gt Intruder_ 0 Na A alice 3 gt bob 4 Ma A Kb Stepi nonce l a ki Emission Figure 9 Alice starts the protocol with the intruder instead of Bob Then the intruder J can decrypt Na Ajx with i nv Kr thus he automatically deduces N4 and A
19. tore m In that case his knowledge becomes intruder knowledge m _k k m In the same way when the intruder receives a tuple a b c then he automatically deduces a b and c Protocol Simulation NSPK txt Trace File nspk trace Trace Files Modes Variables monitoring MSC Previous step Untyped variables Intruder alice 3 bob 4 alice 6 bob 10 Incoming events A alice 3 Intruder 0 Na A Stepl n nonce l a ki on nonge l a kb Emission N Nb Ka nonce l nonce 2 ka Y E Past events alice 6 gt Intruder 0 Na A Intruder_ 0 gt bob 4 nonce 1 bob 4 gt Intruder Na Nb _ Intruder 0 gt alice 6 nonce alice 6 gt Intruder 0 Nb K The intruder on the MSC P Fa p Intruder knowledge nonce 2 ki nonce 1 nonce 2 nonce 2 The intruder s knowledge nones L nonce 2 ra e nonce l a nonce 1 inonce l a ki a b Button to compose a new message from intruder s knowledge Figure 6 Simulation with the intruder Using a specific interface see Figure 7 SPAN can also compose terms of the intruder s knowledge to generate a new message In this interface message patterns and potential receivers are proposed to the user conjointly with intruder data that fit in the pattern holes In Figure 7 we can see that the upper p
20. uild by hand an attack over a protocol using the intruder simulation interface However when the automatic verification tools OFMC CL ATSE find the attack of interest this one can be automatically loaded in the intruder simulation interface using the attack simulation button 4 5 1 Description From version 1 5 SPAN proposes a new button for automatically building MSC from the output of OFMC and CL ATSE verification tools Once an HLPSL specification is loaded in the interface select either OFMC or ATSE verification tools then click on the attack simulation button SPAN is then running the selected verification tool get its output and if an attack is found then it is loaded in the intruder simulation interface Note that both verification with OFMC CL ATSE and loading in the intruder simulation interface may take some time SPAN a Protocol Animator for AVISPA The intruder knows the private key inv ki the message nonce 1 aj_ki and the public key kb then he can deduce nonce 1 a and send nonce 1 a _ki v Protocol Simulation NSPK txt Trace Files Modes Wariables monitoring lt Previous step Untyped variables Intruder 0 alice 3 Incoming events Ai alice 3 gt Intruder 0 Na A bob 4 gt Intruder 0 Na Nb _ nonce l a ki bob 4 gt alice 6 Na Nb Ka 2 fo DA LII 7d i Past events Altalice 6 gt Intruder 9 Na A Intruder 0 gt bob 4 non
21. us messages from this knowledge Message patterns are proposed to the user conjointly with intruder data relevant w r t pattern structure and type The tool can save and load execution traces corresponding to the execution of the protocol super vised by the user The MSC can be exported in postscript format or PDF format Finally as shown in Figure 2 SPAN comes with a local version of the web interface of AVISPA that supports the editing of protocol specifications allows the user to select and configure the back ends integrated into the tool and launch the three different kind of animations protocol simulation with no intruder intruder simulation build your own attacks by hand attack simulation load attacks found by OFMC CL ATSE in the simulation 1 2 Availability License and Installation SPAN is freely available under the terms of the GNU LIBRARY GENERAL PUBLIC LICENSE SPAN a Protocol Animator for AVISPA Page 3 1 3 Bug report and information Please report comments and bugs to Thomas Genet irisa fr 2 Installation SPAN is developped in OCaml The Tcl Tk library version 8 4 for Linux and MacOS and version 8 3 Windows is necessary to use this application See README txt file of the distribution for details about installation of binary versions and for compilation of source versions 3 Specification Language The HLPSL is an expressive modular role based formal language that is used to specify control flow patte
22. ymbolic model checker for security protocols Int J Inf Sec 4 3 181 208 2005 GGHC06 Y Glouche T Genet O Heen and O Courtay A Security Protocol Animator Tool for AVISPA In ARTIST 2 workshop on security of embedded systems Pisa Italy 2006 SPAN a Protocol Animator for AVISPA Page 16 H T03 D Harel and P S Thiagarajan Message sequence charts UML for Real Design of Embedded Real time Systems 2003 Low96 G Lowe Some New Attacks upon Security Protocols In 9th Computer Security Founda tions Workshop IEEE Computer Society Press 1996 INS78 R M Needham and M D Schroeder Using Encryption for Authentication in Large Networks of Computers CACM 21 12 993 999 1978 Ohe05 D von Oheimb Specification language hlpsl developed in the eu project avispa In APPSEM 2005 l ur06 Mathieu Turuani The cl atse protocol analyser In Frank Pfenning editor RTA volume 4098 of Lecture Notes in Computer Science pages 277 286 Springer 2006
Download Pdf Manuals
Related Search