Home

AVISPA v1.1 User Manual

1. avispa script file Figure 1 Architecture of the AVISPA tool v 1 1 2 1 Specifying Protocols HLPSL Protocols to be studied by the AVISPA tool have to be specified in HLPSL standing for High Level Protocols Specification Language and written in a file with extension hlpsl This language is based on roles basic roles for representing each participant role and composition roles for representing scenarios of basic roles Each role is independent from the others getting some initial information by parameters communicating with the other roles by channels In this section we present the syntax of HLPSL and some guidelines for HLPSL beginners 2 1 1 HLPSL Syntax The syntax of HLPSL is detailed in the following using the standard BNF Before describing the syntax we list the lexical entities used in the grammar keywords and expressions being written as strings i e arbitrary sequences of characters enclosed by two characters AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 10 a Lexical entities In HLPSL all variables start with a capital letter and constants start with a small letter note that natural numbers can also be used as constants without any specific interpretation var_ident A Z A Za z0 9_ const_ident a z A Za z0 9_ nat_ident 0 9 The list of HLPSL keywords is the following accept agent authentication_on bool channel compositio
2. BACKEND ident Statistics STATISTICS LabeledStat LabeledStat StatLabel ShortStat UnitLabel StatLabel ident UnitLabel ident ShortStat float Trace ATTACK TRACE Step Step StepNumber Agent gt Agent Msg StepNumber int Agent ident SessionNumber l j SessionNumber int Msg Msg cru Msg Msg Msg ident u n Msg nyn l won Msg yu msg_ident An example of output is given in Section 2 2 4 for the protocol NSPK KS analysed by CL AtSe AVISPA Tool v1 1 User Manual 4 CONTRIBUTIONS 67 4 Contributions 4 1 XEmacs mode A mode for editing compiling and analyzing protocol specifications written in HLPSL is available for XEmacs This mode can either be installed directly by the avispa package or an archive file can be downloaded separately at http www avispa project org software html 4 1 1 Installation The xemacs mode for avispa tools is distributed in a script avispa mode bin This script relies on the definition of certain variables in order to install the mode properly We give these variables by order of preference e AVISPA PACKAGE should be set to a directory that will contain all other directories as subdirectories This variable is automatically set correctly when installing the mode using the makefile provided by the avispa package using the make xemacs command If the above variables are not defined th
3. commutativity of xor xor PreludeM1 PreludeM2 nilpotency of xor xor xor PreludeM1 PreludeM1 PreludeM2 generating rules step gen_pair PreludeM1 PreludeM2 iknows PreludeM1 iknows PreludeM2 gt step gen_crypt PreludeM1 PreludeM2 iknows PreludeM1 iknows PreludeM2 gt step gen_scrypt PreludeM1 PreludeM2 iknows PreludeM1 iknows PreludeM2 gt step gen_exp PreludeM1 PreludeM2 iknows PreludeM1 iknows PreludeM2 gt step gen_xor PreludeM1 PreludeM2 iknows PreludeM1 iknows PreludeM2 gt step gen_apply PreludeM1 PreludeM2 iknows PreludeM1 iknows PreludeM2 gt analyzing rules step ana_pair PreludeM1 PreludeM2 iknows pair PreludeM1 PreludeM2 step ana_crypt PreludeK PreludeM xor xor PreludeM1 PreludeM2 PreludeM3 xor PreludeM2 PreludeM1 PreludeM2 Y for the Dolev Yao model iknows pair PreludeM1 PreludeM2 iknows crypt PreludeM1 PreludeM2 iknows scrypt PreludeM1 PreludeM2 iknows exp PreludeM1 PreludeM2 iknows xor PreludeM1 PreludeM2 iknows apply PreludeM1 PreludeM2 gt iknows PreludeM1 iknows PreludeM2 iknows crypt PreludeK PreludeM iknows inv PreludeK gt iknows PreludeM step ana_scrypt PreludeK PreludeM iknows scrypt PreludeK PreludeM iknows PreludeK gt iknows PreludeM generating fresh constants of any type step generate PreludeM
4. var_ident var_ident Bracketed_par_compositions_list Composition Composition Bracketed_par_compositions_list Compositions_list Bracketed_seq_compositions_list Composition Composition Bracketed_seq_compositions_list Compositions_list Bracketed_compositions_list Composition Compositions_list An example of composition of roles is server S Ks _tin A B Ka Kb Instances alice A Ka bob B Kb Note that in this case Instances has to be a set whose elements are of the compound type agent agent public_key public_key provided A and B are variables of type agent and Ka and Kb are variables of type public_key For example a b ka kb a i ka ki could be the value of Instances o Instantiation of a role To create an instantiation of a role is like calling a procedure giving values to each argument Of course the number of arguments has to be the same as the number of formal parameters and the type of each argument has to be compatible with the type of the corresponding formal parameter AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 18 Role_instantiation const_ident Expressions_list p Declaration of goals Goals are declared in a specific section Such declarations are done either by using predefined macros or by using a LTL formula The available macros correspond to e the secrecy of some information e the st
5. Used A IK IK U z 19 Figure 5 Dolev Yao intruder knowledge formulae It must be noted that according to the definition given in Figure 6 the intruder is able to send Intruderpy O A IK 4 IK v _ Read SND V ASplit V AAdec V GPair V GAcrypt V GFresh AAE RCV msg gt msg IK Figure 6 Dolev Yao intruder behaviour messages on more than one channel at the same time Since we provide an interleaving semantics for HLPSL that behaviour needs to be restricted by adding the constraint depicted in Figure 7 2Notice that the TLA variable Used keeps track of those fresh values that have already been generated by the intruder AVISPA Tool v1 1 User Manual A HLPSL SEMANTICS 81 Interleavingpy VE RCV flag 4 RCV_flag A A J 2 RCV flag RCV flag Figure 7 Dolev Yao intruder behaviour necessary condition for interleaving semantics However the formula in Figure 7 alone does not guarantee the interleaving semantics in fact the HLPSL syntax allows to specify two left hand sides of two transitions within the same basic role such that they both can become enabled allowing both transitions to fire In that case the interleaving semantics is preserved by adding a trigger to the left hand sides in order to enable one transition at the time The trigger may be for instance a signal A 2 4 Freshness In the previous paragraphs we showed that each role Role keeps track in the
6. end role The main role role environment def local KeyMap agent public_key set Snd Rev channel dy const a b s i agent ka kb ki ks public_key sna snb alice_bob_nb bob_alice_na protocol_id init KeyMap fa ka b kb i ki intruder_knowledge la b ks ka kb ki inv ki composition server s ks KeyMap Snd Rcv uspk Snd Rev channels ks public key of server a b ka kb session instances a i ka ki i b ki kb a a ka b kb initial KeyRings AVISPA Tool v1 1 User Manual 2 2 Analyzing a HLPSL Specification 34 b b kb i i ki end role Description of goal properties goal secrecy_of sna snb authentication_on alice_bob_nb authentication_on bob_alice_na end goal Call of the main role environment 2 2 Analyzing a HLPSL Specification Analyzing a protocol is entirely automatic once the HLPSL specification has been written the script avispa can be used to evaluate it and will print the result of the analysis For a basic use of this script you do not need to know many options For a more expert use please read the Advanced User Section Section 3 The AVISPA tool is composed of several modules e a translator for transforming HLPSL specifications written by the user to IF specifications intermediate format see Section 3 1 2 called hlps12if see Section 3 1 1 e four different verification tools back ends that ca
7. exists PreludeM gt iknows PreludeM AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 49 3 1 4 Example The IF specification given in the following has been automatically generated from the HLPSL specification of the Needham Schr der Public Key Protocol with Key Server Section 2 1 3 Note that in the initial state arguments of a role state that have not been initialised are assigned to a generic constant for example dummy_agent for an argument of type agent In the transition rules in general when an argument of a role state is modified its old value in the left hand side is denoted with a generic name for example Dummy_Na if the argument is called Na The description of sets is given by a list of contains facts one per element The set itself is identified by a constant set_94 for example Reading adding or removing elements in a set is possible only if the set identifier is known h IF specification of NSPK KS hlpsl section signature state_bob agent agent public_key public_key set pair agent public_key nat text text public_key set agent nat gt fact state_alice agent agent public_key public_key set pair agent public_key nat text text public_key set agent nat gt fact state_server agent public_key set pair agent public_key agent agent public_key nat gt fact section types snb alice_bob_nb bob_alice_na sna protocol_id M
8. 2 USER SECTION 13 g Declaration of owned variables Roles may declare ownership of variables Declaration of owned variables Owns_declaration owns Variables_list Owned variables may change in only the way described by the owning role even if they are visible from outside However since shared variables are not fully handled in the current version of the AVISPA tool owns declarations are useless h Declaration of constants Constants are declared in roles but are global Multiple declarations of a constant do not raise an error provided the type is the same For clarity reasons this is recommended to declare all constants in the main role ex environment Const_declaration const Constants_declaration_list Constants_declaration_list Constant_declaration Constant_declaration i Initialisation of local variables The initialisation section is a conjunction of simple assignments to variables and of constant predicates Expressions used for assignments and in the predicates have to use initialised variables this is the meaning of a stutter expression Init_declaration init Init_declarations Init_declarations Init_declaration Init_declaration Init_declaration var_ident Stutter_expression const_ident Stutter_expressions_list Let us give a simple example of initialisation init State 0 SetKeys iknows K j Declaration of the acceptan
9. 8 Franz Baader and Tobias Nipkow Term Rewriting and All That Cambridge University Press 1998 9 D Basin S M dersheim and L Vigan Constraint Differentiation A New Reduction Technique for Constraint Based Analysis of Security Protocols In Vijay Atluri and Peng Liu editors Proceedings of CCS 03 pages 335 344 ACM Press 2003 Available at http wuw avispa project org 10 D Basin S M dersheim and L Vigan OFMC A Symbolic Model Checker for Security Protocols International Journal of Information Security 2004 11 D Dolev and A Yao On the Security of Public Key Protocols EEE Transactions on Information Theory 2 29 1983 AVISPA Tool v1 1 User Manual REFERENCES 88 12 E Giunchiglia M Maratea A Tacchella and D Zambonin Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability In R Gor A Leitsch and T Nipkow editors Proceedings of IJCAR 2001 LNAI 2083 pages 347 363 Springer Verlag 2001 13 Leslie Lamport The temporal logic of actions ACM Transactions on Programming Lan guages and Systems 16 3 872 923 May 1994 14 M W Moskewicz C F Madigan Y Zhao L Zhang and S Malik Chaff Engineering an Efficient SAT Solver In Proceedings of the 38th Design Automation Conference DAC 01 2001 15 M Rusinowitch and M Turuani Protocol Insecurity with Finite Number of Sessions is NP complete In Proceedings of the 14th IEEE Co
10. Na A _inv Ka Stutter_expression _ Bracketed_stutter_expression Non_stutter_expression Non_stutter_expression New value of a variable var_ident Inverse of a public private key inv Non_stutter_expression Concatenation right associative Non_stutter_expression Stutter_expression Stutter_expression Non_stutter_expression Non_stutter_expression Non_stutter_expression Function application Variable_or_constant Non_stutter_expression_list Insertion of an element in a set cons Elt Set cons Expression Expression Deletion of an element in a set delete Elt Set delete Expression Expression h Set Non_stutter_expressions_list Encryption Na A _ Ka Kb Non_stutter_expression _ Bracketed_expression Stutter_expression _ Bracketed_non_stutter_expression Expressions_list Expression Expression Expression Stutter_expression Non_stutter_expression Bracketed_stutter_expression inv Stutter_expression AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 24 Variable_or_constant Stutter_expressions_list Variable_or_constant_or_nat Stutter_expression Bracketed_non_stutter_expression var_ident inv Non_stutter_expression Variable_or_constant Non_stutter_expressions_list Non_stutter_exp
11. assuming that it appears on the RHS of a transition meaning it is a write action is a short form for SND Msg The latter assuming that it appears on the LHS of a transition and is therefore a read event is short for RCV_flag RCV_flag RCV Msg where RCV_flag is a binary flag which is toggled each time a new message arrives on channel RCV Recalling our restriction that events contain at least one predicate of the form X X we can see that the former is an action and the latter an event HLPSL also supports signals that is asynchronous events assuming they occur on the LHS of a transition A signal can be seen as a channel through which no information is sent Sig nals in HLPSL are of the form SGNLO As for channels the latter is just a shorthand for It can be the case that at a given point a spontaneous transition is enabled but does not fire directly and meanwhile some other transition is applied such that its effects make the spontaneous transition no longer enabled In that case the latter will not be able to fire anymore unless it becomes enabled once again thanks to the effects of some other transition AVISPA Tool v1 1 User Manual A 2 Formal Semantics 76 SGNL_flag SGNL_flag meaning that something has changed in that particular channel but no messages have been sent through it since there is no assignment SGNL_flag Msg as for normal communication channels In the rest of t
12. const_ident nat_ident const_ident nat_ident x Note that types may be compound using functions representing pairing encryption e Section for variables and constants declaration Variables and constants are all declared using types and functions declared in the prelude file TypesSection section types TypeDeclaration TypeDeclaration AtomicTermList Type AtomicTermList AtomicTerm AtomicTerm AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 43 AtomicTerm const_ident nat_ident var_ident f Section for equations This section represents the equational theory that has to be considered for some specific function operators such as pair xor and exp EquationsSection section equations Equation Equation Term Term Term AtomicTerm ComposedTerm ComposedTerm IF_Operator TermList TermList Term Term g Section for initialisation This section contains all the initial information needed before starting the analysis of the protocol the intruder initial knowledge the instantiated roles states and some additional information needed for the two previous information InitsSection Section inits initial_state const_ident State State Fact Fact Fact IF_Fact TermList IF_Fact state_ const_ident const_ident AVISPA Tool v1 1 User Manual 3 1 Generating an IF
13. AttackStatesSection c Section for type symbols This section contains the list of constant names representing the basic types available such as agent public key symmetric_key TypeSymbolsSection section typeSymbols ConstantList ConstantList const_ident const_ident x d Section for signature This section is decomposed in three parts the declaration of super types an ordered precedence between some types the declaration of function symbols the declaration of predicate symbols SignatureSection section signature SignatureSection0 SignatureSection0 SuperTypeDeclaration FunctionDeclaration PredicateDeclaration One super type message for example is very useful for avoiding to have as many copies of functions and predicates as there are types SuperTypeDeclaration IF_Type gt IF_Type IF_Type const_ident AVISPA Tool v1 1 User Manual 3 1 Generating an IF Specification 42 The type of a function is declared in a very standard way The only difference with the type of a predicate is that the result of a predicate is of type fact FunctionDeclaration IF_Operator TypeStar gt Type PredicateDeclaration IF_Operator TypeStar gt fact IF_Operator const_ident TypeStar Type Type TypeStar Type IF_Type IF_Operator TypeList ConstantNatList TypeList Type UL Type ConstantNatList
14. Section 39 3 1 Generating an IF Specification 4 2 44 4564 4484 bea Oa bees 39 31 1 Automatic Translation from HLPSLtolF osito 39 3 1 2 The IF Specification Language sos sa co sea pca a a ee a 40 Lexi al entities ocd soe ds EYEE EDD ES a b e a e wR GE ES 40 b Prelude and IF files sa cs 6s eet 442 48448 Abbe a en 40 E Dection for type eval s e si ee EE A ORES OAR SD e 41 d Section or SIGMA e s ccone coe po SRE Ee a Re Bis RE n 41 e Section for variables and constants declaration 42 AVISPA Tool v1 1 User Manual CONTENTS 4 J Section for eg ations s s s e asi a Bw Oe GOR Bae e 43 y pectin for Illa cas ca eesi es Bepo t Bi patai s 43 h Section for transition Tules u s ius AR eR ES Eo 44 A DOCU for properties cora diarrea 45 J SEEtOn for attack Sib e s o ostra AR ee ae la BS 45 k Section for intruder behavi t sss ss scarca e roses 46 alg A Prelude Pile seedi se ELE SEEDED YEG EY OES OEE 46 E 2 errs MASH ORES SOE OH Soh OSS REESE EES Ke 49 32 Amalysing a IF Specification 4 se ce ema a ea 54 gal Usine CLAC AI 54 fee SUENO ea a ee ee eS ee A 58 dal Usme SIN o he Ba ee Poe AAA RA A 59 aoe emo MAS sa io a dr aa ena a 60 TA4SP CIO sna caras rocas as Ear e ee BA A 61 TAASP OQUIDUTS AA INE EEE 62 3 3 The Siandard Output Format lt ss s 93 205 64 4 Contributions 67 LE XEma cs modes sad osi oe hae a ha e ae a e E AA 67 Abi een a aigre be ee e ee A e a ee ee
15. a variable in a transition this new value has been either learned in the left hand side of the transition received on a channel or found by decomposing a message or searching in a set or assigned in the right hand side of the transition Assigning the new value of a variable with new means assigning it with a fresh value i e a nonce generated at runtime A primed variable must not appear in the initialisation part or in the intruder knowledge decla ration of a role d Channels In the current version of the AVISPA Tool only Dolev Yao DY channels are handled So this is recommended to use only this kind of channels Semantically channels have changing values depending if they are empty or not So they are declared as variables in general in some composition roles and used as predicates Do not declare constants of type channel e Goal specification Goals are specified as macros representing pre defined safety temporal formulae built on top of the goal predicates witness wrequest for weak authentication request for strong authenti cation and secret These goal predicates are explicitly declared in right hand sides of HLPSL transitions and are translated into corresponding IF facts request and wrequest facts will be augmented with the role ID These predicates are used to specify secrecy and different forms of authentication e Secrecy is modelled by means of the goal predicate secret T id A B standing for t
16. constants Note that setting an option through this menu lasts a whole session 1 e until XEmacs is closed d Navigation The avispa mode keeps internally a current state that takes into account both the current file and the current tool that will be applied on the current file through the Process file button This permits to navigate among the different files using the lt lt and gt gt buttons The lt lt button If the current file is an ATK file it changes to the corresponding IF file If the current file is an IF file it changes to the corresponding HLPSL file The gt gt button If the current file is an HLPSL file it changes to the corresponding IF file If the current file is an IF file it changes to the ATK file corresponding to the current backend The action in other cases depends on the value of the Navigation Button Wrap variable The possible behaviors are explained in Section 4 1 3 4 1 3 Customization The avispa mode may be customized through the command AVISPA Tool v1 1 User Manual 4 1 XEmacs mode 70 M x customize You may then enter one of the following e avispa project permitting access to all other variables e avispa tools containing generic options that are explained in Subsection 4 1 3 e avispa hlpsl2if avispa atse avispa ofmc avispa satmc and avispa ta4sp provide another way to change the options of the backends and
17. eM SAY OHSS EROS E e 15 m Composition of roles is ars ee AA RARA 16 O Instantiation OF AB bok ok e e a e a a RA 17 p Declaratiom ol poal ss s e a s este A E ee eee eS ws 18 q Declaration of types of variables o a 19 r Declaration of types of co stantsss os ssa nes tareata sirds 20 s Types and compound types oao oa a 20 t Stutter and non stutter formulas lt ss ss 46444 ee ae bee GEES 21 AVISPA Tool v1 1 User Manual CONTENTS 3 u Stutter and non stutter expressions 0 22 v Predefined equational theories o oo ao o e a 24 212 LPS Guidelines sic sagor Ce ds E e eee ee eee OY a 25 t Variable constant TAMES o aira dae o ea bee daa 25 Pi lt s s suca oda e SSR Ree Ae a ey i 25 c Old new values of variables o oaa been es RR EEE 25 d Channels parda EY Oe ee we Ko 25 6 Gual sp cilcation sa s oe Oe So eL ERS RARA Ee He 25 J Transitions e 2 odd eS ee Oe eS ee 2 Ode eel ead ws 27 e Teale ke eS ee EOS paris SS eRe RES RM RE 27 Oe eo aa SE ee Bee e eee a 28 en II Ye ee eae wee oe we ee 28 E IR 29 k Sessions generation 2444 ea dee rss oa eee a BR 29 A e he es ee AR TAE 30 2 2 Analyzing a ALPSL Specification ceed ed we deeded ended aan 34 22 UG avispa sas a Koes oe ees oe ee R a 35 LEZ Generated IES s eeue a ode is A pe do ee A 36 226 interpreting the BDO ask ea e a ee a Hee RR a 36 22A Examples A AI 37 3 Advanced User
18. ee a 67 41 2 Usage 646 4 0 be bee 2b G4 GREE hee Eee EEG ES 68 O First Bl eh ek dK PROSE REED RYE REE AA AAA a 68 b Th Avispa Men ssa a eG RK e a e Ge OR 68 e The options pe ed oe Be ho SO a au e eee la de 69 Ms s eee ee ke eee OSS HEEB EHS RSS ER 69 A oak Ee eR CHER SESH ES EE ORES OE ESE a 69 a The avispa project STOUT s ca 42 6446448468 oboe ea He 70 b The auispa 1008 groups s s sos etea os eee ae Ba Sew Bead amp S 71 ALA MIO GS CRE RR RED SON Hee A OEE RS RE 72 a How to delas A Macro Ts eceu a CREE She ee Oe eee ORE EES 72 AVISPA Tool v1 1 User Manual CONTENTS 5 p Eanes be ee eS ee ee be ou Shae eee we See Sd HS 13 a2 Library or Protocols seis we eee Ow eR PEGGY CE SG SSS 73 de LPS documental s 644 2b ew 4 bY OS EER ORES A 73 A HLPSL Semantics 74 AT Preliminaries espet se rmi rapeaa cas ds b uae eee a a 74 Ai The TIAS SV ac poi HC Oe Ee Ce ee W g 74 A 12 Events and Actions lt a ssa rosse koeri ara piara Baw rG 74 As ICI ed epode eA de e DS i a Ee E aae p b REGS ao E a 75 A 1 4 Communication Channels and Signals 000 75 a2 Formal Semantics ci sb sra ee rs EE ww SE Ree eae we 76 Ppl ieee AA 76 A22 TOU Sb Roles e db goa ba oe de we eS padia ead BS 76 A23 Ius Model sucias BMS amp HAT Ra OHS RROD SEAR 79 ADA Freshtiess oo s cai ane Rhea ba eRe eR ERED EEE Ea wR 81 BO AGA parara 660s whee bee eee Se Eo 81 B IF Semantics 83 References 87
19. iknows MGoal gt contains i ASGoal property secrecy_of_snb MGoal ASGoal Csecret MGoal snb ASGoal iknows MGoal gt contains i ASGoal property authentication_on_alice_bob_nb A1Goal A2Goal MGoal SID SID1 SID2 C request A1Goal A2Goal alice_bob_nb MGoal SID equal A2Goal i gt witness A2Goal A1Goal alice_bob_nb MGoal Crequest A1Goal A2Goal alice_bob_nb MGoal SID1 request A1Goal A2Goal alice_bob_nb MGoal SID2 AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 53 equal A2Goal i gt equal SID1 SID2 property authentication_on_bob_alice_na A1Goal A2Goal MGoal SID SID1 SID2 Crequest A1Goal A2Goal bob_alice_na MGoal SID equal A2Goal i gt witness A2Goal A1Goal bob_alice_na MGoal Crequest A1Goal A2Goal bob_alice_na MGoal SID1 request A1Goal A2Goal bob_alice_na MGoal SID2 equal A2Goal i gt equal SID1 SID2 section attack_states attack_state secrecy_of_sna MGoal ASGoal iknows MGoal secret MGoal sna ASGoal amp not contains i ASGoal attack_state secrecy_of_snb MGoal ASGoal iknows MGoal secret MGoal snb ASGoal amp not contains i ASGoal attack_state authentication_on_alice_bob_nb A1Goal A2Goal MGoal SID request A1Goal A2Goal alice_bob_nb MGoal SID not witness A2Goal A1Goal alice_bob_nb MGoal amp not equal A2Goal i attack_state replay_protection_on_alice_bo
20. kind of verification a user wants to do TAZSP Options The options below are used by the binary ta4spv2 at bin backend TA4SP However to use TA4SP from the avispa script the user will have to set these options in the ta4sp config file e level lt integer gt level lt integer gt in ta sp config When this option is initialised to 0 an over approximation will be computed With a number greater than 0 an under approximation is computed and this number corresponds to the number of times that rewrit ing is applied on the tree languages computed by TA4SP e 2AgentsOnly abstractions lt boolean gt in ta4sp config This option is very useful to improve time computations This option provides a specification in which there are only two agents the intruder and an honest agent If secrecy properties are verified in this model then they are verified in the specified model IF specification However if there is an attack then it may be a false one due to the abstractions done Another interesting point is when an initial state specify a session between honest agents and all possible sessions where the intruder plays at least one of the role for example in NSPK Alice played by a Bob played by b Alice played by a Bob played by i and Alice played by i Bob played by b and when the given secrecy properties are verified with TA4SP In this context the given properties will be verified for any sessions AVISPA
21. membership of an element in list are also constraints To interpret the IF transition relation each role is partially executed to extract an exact and minimal list of constraints modeling it The participants s states and knowledge are eliminated thanks to the use of global variables Any protocol step is executed by adding new constraints to the system and reduce eliminate other constraints accordingly Finally at each step the system state is tested against the provided set of security properties The analysis algorithm used by CL AtSe is designed for a bounded number of loops i e a bounded number of protocol steps in any trace That is if the protocol specification is loop free then the whole specification is analyzed otherwise the user must provide an integer bound on the maximal number of loop iterations With a bounded number of loop iterations the search for attacks is correct and complete and corresponds to an optimized deterministic implementation of the NP Completeness result from 15 While reading the IF file CL AtSe tries by default to simplify the protocol specification The goal of that is to reduce the total number of protocol steps that need to be checked Since most of the execution time is consumed in testing all possible interleaving of the protocol steps this simplification can be very important for large protocols The idea is to identify and mark the protocol steps that can be executed as late or as soon as possible T
22. of the translator It also permits to save options from one session to another It is also possible to change the names of the executable launched upon calling a tool the translator or a backend Note that the AVISPA Customize group of variables button permits to directly access the avispa tools a The avispa project group This is the global group of variables related to the avispa mode Its main use is to present the Avispa Project since most variables are member of the avispa tools group It permits to set the Use Abbrev Mode that controls whether abbreviations should be launched when accessing a new buffer with the Avispa mode It also gives access to the shortcuts defined Currently these are e C c C a toggles the abbreviation mode e C c C c process compile or validate current buffer e C c b init where init is the lower case first letter of a backend name changes to this backend For example C c bt permits to change to the TA4SP backend e C c C n shortcut to the e C c C p shortcut to the gt gt navigation button lt lt navigation button The description of this variable also contains the abbreviations defined by default There are currently abbreviated patterns and keywords e The pre defined templates of an hlpsl specification are br creates a template for a basic role cr creates a template for a composition role
23. three basic roles alice bob and server In addition two composition roles are specified nspk representing the classical composition of roles alice and bob and environment representing the composition of several instances of nspk with one instance of server HLPSL Specification Role of the initiator role alice A B agent Ka Ks public_key KeyRing agent public_key set Snd Rev channel dy played_by A def AVISPA Tool v1 1 User Manual 2 USER SECTION 31 local State nat Na Nb text Kb public_key init State 0 transition Start if alice must request bob s public key from key server ask State 0 Rev start not in B Kb KeyRing gt State 1 Snd A B Receipt of response from key server learn State 1 Rcv B Kb _inv Ks gt State 0 KeyRing cons B Kb KeyRing Start resume provided alice knows bob s public key knows State 0 Rev start in B Kb KeyRing gt State 4 Na new Snd Na A _Kb secret Na sna A B witness A B bob_alice_na Na 4 Rev Na Nb _Ka 6 Snd Nb _Kb request A B alice_bob_nb Nb cont State gt State end role Role of the receiver role bob A B agent Kb Ks public_key KeyRing agent public_key set Snd Rev channel dy played_by B def local State nat Na Nb text Ka public_key AVISPA Tool v1
24. to nil if you do not want the mode to automatically display the result of a process i e compilation or verification There is no automatic fetching when the process spawned is not synchronous with XEmacs This is due to a race condition that would often result in XEmacs displaying an out of date version e Navigation Button Wrap The variable permits to define the behavior of the lt lt button when visiting an HLPSL buffer and of the gt gt button when visiting a result If set to nil these buttons will produce no effect If set to any other value the lt lt buffer button permits to jump directly from an HLPSL buffer to the corresponding result buffer The name of this buffer is computed with respect to the backend that would be used for next analysis of a IF buffer Conversely the gt gt permits to jump directly from a result file to the corresponding HLPSL specification These two buttons do not launch any application nor update the content of a buffer visiting a file We currently advice to use the better tested synchronous compilation and validation o ptions Processes launched from the Main buffer are always synchronous The fetch result option is always ignored when launching processes from this buffer since it could lead to the jump to several buffers one after another without any control by the user 4 1 4 Macros It is now possible to defineover hlpsl
25. use of non algebraic pairing operator in the unification algorithm Other wise the unification algorithm tries to consider the associativity property of the pairing short Ask CL AtSe to output a minimal attack if possible i e an attack with a minimal number of protocol steps It usually needs more memory and a bit more cpu time than finding any attack It performs a breath first search instead of depth first in the protocol step interleaving tree e out Write the attack to lt filename gt atk instead of using stdout e dir d Choose d as output directory e help Write a summary of all options including debugging options The CL AtSe verbose output format Using the v or noexec option s of CL AtSe we get a detailed view of the starting point of CL AtSe This is called the Initial System State in the output and represents both the intruder and honest participant s states in CL AtSe just after reading and interpreting the if file While the intruder state is just represented by a list of knowledges Intruder knowledge line the honest participants are described by a set of instantiated roles so called Instantiated protocol specification While the syntax of this protocol specification is quite simple it needs a few explanations Role instances In CL AtSe each protocol role must be independent from the others and use different variable names Therefore each role in the IF file is instantiated into a se
26. who want to do more than just using the avispa script file will find in the following sections important details guiding them for exploiting all the possible options at each step of the AVISPA tool architecture Figure 2 Figure 2 Architecture of the AVISPA tool v 1 1 3 1 Generating an IF Specification Given a HLPSL specification written in a file with extension hlps1 the first step is to translate it into a lower level specification This is automatically done by the translator hlps12if generating a specification in an intermediate format IF The resulting file has the same name with extension if 3 1 1 Automatic Translation from HLPSL to IF This section lists the possible parameters of the hlps12if translator hlps12if is a translator that maps security protocol specifications written in HLPSL into rewriting systems written in IF It is written in Objective Caml which is an implementation of the ML language based on the Caml Light dialect USAGE hlps12if options file hlps1 AVISPA Tool v1 1 User Manual 3 1 Generating an IF Specification 40 Options types Print identifiers and their types init Print initial state rules Print protocol rules goals Print goals all Print everything default split Split goals in different IF files stdout Print on the standard output output dir Set the output directory default same as input nowarnings Do not display warnings help Display this list o
27. 1 User Manual 2 1 Specifying Protocols HLPSL 32 init State 2 transition Start if bob must request alice s public key from key server ask State 2 Rcv Na A _Kb not in A Ka KeyRing gt State 3 Snd B A Receipt of response from key server learn State 3 Rcv A Ka _inv Ks gt State 2 KeyRing cons A Ka KeyRing Start resume provided bob knows alice s public key knows State 2 Rcv Na A _Kb in A Ka KeyRing gt State 5 Nb newO Snd Na Nb _Ka secret Nb snb A B witness B A alice_bob_nb Nb cont State 5 Rcev Nb _Kb gt State 7 request B A bob_alice_na Na end role Role of the key server role server S agent Ks public_key KeyMap agent public_key set Snd Rcv channel dy played_by S def local A B agent Kb public_key transition reqi Rcv A B in B Kb KeyMap gt Snd B Kb _inv Ks end role AVISPA Tool v1 1 User Manual 2 USER SECTION 33 Role representing a partial session between alice and bob role nspk Snd Rev channel dy Ks public_key Instances agent agent public_key public_key set KeySet agent gt agent public_key set def local A B agent Ka Kb public_key composition _ in A B Ka Kb Instances alice A B Ka Ks KeySet A Snd Rcv N bob A B Kb Ks KeySet B Snd Rcv
28. AVISPA www avispa project org IST 2001 39252 Automated Validation of Internet Security Protocols and Applications AVISPA v1 1 User Manual The AVISPA Team Document Version 1 1 June 30 2006 alw E Project funded by the European Community under the Information Society Information Society Technologies Programme 1998 2002 Technologies CONTENTS 2 Contents 1 Introduction 6 LL Installation Procedur 6 so b weg rs Be eo e ae aa A 6 12 How to sethe AVISPA tooll s s ios i oe Gee ao Oe Re Oe ee we eG 7 1 3 About this Manual se s a s arera prd He eee Ee Hw t 8 TA Contact EEE 8 2 User Section 9 2 1 Spee Protocols HLPSL ci 64464 44488 24248 doe ae 211 TP OYA e sois Bh el ee ee ee eA eA ea e 9 q Lexigal entities ecs se ee Se e REE oe eee Bale ws 10 b Structure of a HLPSL specification o o 10 s DeNnition roles oscars EONS e A a E 11 d De nition of a role lt sa ses eK ee ERE aer ae 11 e Declarations In Toles 0 0d pe a e e ee Oe ee SOO 12 f Declaration of local variables ooa aaa et eas 08 12 g Declaration of owned variables o 13 fi Declaration of constants ccoo doi k oe ane ee A 13 i Initialigation of local variables e ciec ooe eee be gia eoi gia ei 13 J Declaration of the acceptance state ooa aa a a 13 k Declaration of intruder knowledge a 14 L Transitions in pasic POI s s cosdas eRe eee AOS 14 m Cee and IAN a
29. AVISPA Tool v1 1 User Manual 1 Introduction AVISPA Automated Validation of Internet Security Protocols and Applications is a push button tool for the automated validation of Internet security sensitive protocols and applications It pro vides a modular and expressive formal language for specifying protocols and their security prop erties and integrates different back ends that implement a variety of state of the art automatic analysis techniques The AVISPA tool has been realized thanks to the AVISPA shared cost RTD FET open project IST 2001 39252 by the Artificial Intelligence Laboratory at DIST University of Genova Genova Italy the CASSIS group at INRIA Lorraine LORIA Nancy France the Information Security group at ETHZ Z rich Switzerland and Siemens AG Munich Germany For more information on this project and on the AVISPA Team please consult http www avispa project org or subscribe to the avispa users avispa project org mailing list by sending an empty e mail to avispa users join avispa project org 1 1 Installation Procedure The AVISPA tool is distributed with a copyright Please take a look at the LICENSE file provided with the tool before proceeding with the installation This software is being developed as a research tool We continue to make significant changes to it This is an alpha release which we are doing primarily in order to get feedback We are willing to know what you think of AV
30. Goal start message ASGoal Set_48 Set_24 Dummy_Set_48 Dummy_Set_24 set agent set_97 set_96 set_94 KeyMap KeyRing Dummy_KeyRing set pair agent public_key Na Nb Dummy_Nb Dummy_Na dummy_nonce text set_125 set_121 set_116 set_107 set dummy_agent A2Goal A Goal a b s A B S Dummy_B Dummy_A i agent SID2 SID1 SID 7 5 3 2 State 6 4 1 O nat ka kb ki ks Kb Ks Ka Dummy_Ka Dummy_Kb dummy_pk public_key section inits AVISPA Tool v1 1 User Manual 3 1 Generating an IF Specification 50 initial_state initi iknows start iknows a iknows b iknows ks iknows ka iknows kb iknows ki iknows inv ki iknows 1 state_server s ks set_94 dummy_agent dummy_agent dummy_pk 2 state_alice a b ka ks set_96 0 dummy_nonce dummy_nonce dummy_pk set_107 4 state_bob b a kb ks set_97 2 dummy_nonce dummy_nonce dummy_pk set_116 5 state_alice a i ka ks set_96 0 dummy_nonce dummy_nonce dummy_pk set_121 6 state_bob b i kb ks set_97 2 dummy_nonce dummy_nonce dummy_pk set_125 9 contains pair a ka set_94 contains pair b kb set_94 contains pair i ki set_94 contains pair a ka set_96 contains pair b kb set_96 contains pair b kb set_97 section rules step step_0 S Ks KeyMap Dummy_A Dummy_B Dummy_Kb SID A B Kb state_server S Ks KeyMap Dummy_A Dummy_B Dummy_Kb SID iknows pair A B contains pair B Kb KeyMap gt state
31. ISPA so please send comments to us at avispa users avispa project org In order to install AVISPA vX Y you need to extract the archive avispa package X Y_ Linux i686 tgz in the desired directory which will create a new sub directory named avispa_ 1 0 populated by a number of files and sub directories Then you need to set the environment variable AVISPA_PACKAGE to refer to the absolute path ending in avispa X Y and to put the script called avispa in the execution path of your shell For example if you want to install the AVISPA tool in a directory opt in a bash shell environment the commands are cd opt AVISPA Tool v1 1 User Manual 1 INTRODUCTION 7 tar xzf home xyz avispa package X Y_Linux i686 tgz export AVISPA_PACKAGE opt avispa X Y export PATH PATH AVISPA_PACKAGE Now you should be able to execute AVISPA using the command avispa Please see the README file for information about the command line options of AVISPA The AVISPA package provides a user friendly mode for XEmacs to allow a simple interaction between the user and the modules of the AVISPA package To set up the XEmacs mode follow the instructions below cd AVISPA_PACKAGE contrib tar xzf avispa mode tgz This command will create a directory temporary avispa containing a makefile for installing the XEmacs mode Follow the instruction in temporary avispa help txt when done delete the temporary directory temporary avispa The AVISPA package furthe
32. S PROTOCOL NSPK fix if COMMENTS TA4SP uses abstractions 2AgentsOnly For the given initial state an over approximation is used with an unbounded number of sessions Terms supposed not to be known by the intruder are still secret AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 63 2 ta4spv2 2AgentsOnly level O NSPK if SUMMARY INCONCLUSIVE DETAILS OVER_APPROXIMATION UNBOUNDED_NUMBER_OF_SESSIONS TYPED_MODEL PROTOCOL NSPK if COMMENTS TA4SP uses abstractions 2AgentsOnly Use an under approximation in order to show a potential attack The intruder might know some critical information 3 ta4spv2 level 7 NSPK if SUMMARY UNSAFE DETAILS UNDER_APPROXIMATION PROTOCOL NSPK if COMMENTS In our model there is a potential attack The intruder may know some critical information 4 ta4spv2 level 3 NSPK if SUMMARY INCONCLUSIVE DETAILS UNDER_APPROXIMATION AVISPA Tool v1 1 User Manual 3 3 The Standard Output Format 64 PROTOCOL NSPK if COMMENTS Use a greater bound or check the protocol in an over approximated context 3 3 The Standard Output Format All back ends of the AVISPA tool have the same output format Based on this format a tool may be used for graphically representing an attack as a sequence of message exchanges Such a graphical tool is not distributed in this light package but will soon be supplied in a more complete version As a conseque
33. Specification 44 h Section for transition rules Contrarily to a HLPSL specification all the transitions of the protocol are listed in the same section independently of the concerned role RulesSection section rules RuleDeclarationx A transition starts with a unique label and the list of variables involved the left hand side is a list of facts containing mostly a role state fact plus maybe some positive or negative conditions the right hand side is a list of facts RuleDeclaration step const_ident VariableList CState ExistsVar gt State CState State ConditionList ConditionList amp Condition Condition PositiveCondition NegativeCondition PositiveCondition equal won Term nou Term yn l leg we Term el Term nyu NegativeCondition not qu Condition l not won Fact UDEL ExistsVar exists VariableList VariableList var_ident var_ident x Variables that have to receive a fresh value for this transition are listed in the implication after the exists keyword AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 45 i Section for properties This section contains properties described by LTL formulas They have to be satisfied all along the execution trace provided the analysers can handle them Those properties come either directly from LTL formulas written in the HLPSL specification or from the HLPSL macro go
34. Tool v1 1 User Manual 3 2 Analysing a IF Specification 62 e new CoarserAbstractions coarserabstractions lt boolean gt in ta4sp config This option allows to merge several data of the same type into a single one For instance let N1 and N2 two variables representing two nonces Usually we distinguish these two nonces by two functionnal symbols like n1 A B and n2 A B where A B are both a variable of type agent With this option the two nonces are represented by the same functional symbol In practice we have 1 obtained better computation times and 2 a lot of positive results SAFE in case of an over approximation But this option has to be used only in an over approximated context otherwise one can encounter some false attacks TA4SP Outputs As seen in the previous paragraph several outputs are possible depending on the options used and the protocol to check These following examples illustrate the following cases 1 Secrecy verified in an over approximation context 2 Secrecy not verified in an over approximation context 3 Secrecy violated in an under approximated context 4 Attack not yet found in an under approximated context These examples about ta4spv2 runs concern the two protocols Needham Schroeder Public Key protocol NSPK if and its corrected version NSPK fix if 1 ta4spv2 2AgentsOnly level 0 NSPK fix if SUMMARY SAFE DETAILS TYPED_MODEL OVER_APPROXIMATION UNBOUNDED_NUMBER_OF_SESSION
35. _server S Ks KeyMap A B Kb SID iknows crypt inv Ks pair B Kb contains pair B Kb KeyMap step step_1 A B Ka Ks KeyRing Na Nb Dummy_Kb Set_24 SID state_alice A B Ka Ks KeyRing 0 Na Nb Dummy_Kb Set_24 SID iknows start Q not contains pair B Kb KeyRing gt state_alice A B Ka Ks KeyRing 1 Na Nb Dummy_Kb Set_24 SID AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 51 iknows pair A B step step_2 A B Ka Ks Dummy_KeyRing Na Nb Dummy_Kb Set_24 SID Kb state_alice A B Ka Ks Dummy_KeyRing 1 Na Nb Dummy_Kb Set_24 SID iknows crypt inv Ks pair B Kb gt state_alice A B Ka Ks Dummy_KeyRing 0 Na Nb Kb Set_24 SID contains pair B Kb Dummy_KeyRing step step_3 A B Ka Ks KeyRing Dummy_Na Nb Dummy_Kb Dummy_Set_24 SID Na Kb state_alice A B Ka Ks KeyRing 0 Dummy_Na Nb Dummy_Kb Dummy_Set_24 SID iknows start contains pair B Kb KeyRing exists Na gt state_alice A B Ka Ks KeyRing 4 Na Nb Kb Dummy_Set_24 SID iknows crypt Kb pair Na A secret Na sna Dummy_Set_24 witness A B bob_alice_na Na contains A Dummy_Set_24 contains B Dummy_Set_24 contains pair B Kb KeyRing step step_4 A B Ka Ks KeyRing Na Dummy_Nb Kb Set_24 SID Nb state_alice A B Ka Ks KeyRing 4 Na Dummy_Nb Kb Set_24 SID iknows crypt Ka pair Na Nb gt state_alice A B Ka Ks KeyRing 6 Na Nb Kb Set_24 SID iknows crypt Kb Nb request A B alice_bob_nb Nb SID st
36. a substitution such that the type of every substituted variable agrees with the type of the term it is replaced with In an untyped model the types are not considered and hence do not constrain the unification As we adopt the standard notion of sorted unification we will not go into further details here but refer the reader to 8 We use the as an associative commutative and idempotent operator i e we have ty to t3 t1 to t3 ti ta to ty t t t Note however that these three properties work only on facts and not on messages With these properties the operator works as a set constructor for facts and in the following we will consequently talk about sets union and set difference for facts as a shorthand Rule Application Let us denote an IF rewrite rule by means of the triple 1 exVar r where is the LHS of the rule r is the right hand side of the rule and exVar is the list of existentially quantified variables A LHS of arule contains a set of positive and negative facts as well as a set of conditions i e a set of equalities and inequalities as follows the IF condition equal t t2 represents equality of the terms and tz not represents negation of a condition and lt t1 t2 represents t lt t For a substitution o we define a Cond on conditions as expected ty to iff tio tego where t and tp are arbitrary terms ty lt ta iff tio lt t20 where t and tz are natural n
37. actical for writing a protocol specification and verifying it automatically 1 3 About this Manual This manual is divided in two part e For non expert users the User Section describes the syntax of the specification language HLPSL and the different steps for analysing a HLPSL specification and interpreting the output e For expert users the Advanced User Section describes how to use all the power of the AVISPA tool it presents the translator of HLPSL specifications into IF Intermediate For mat specifications then it shows how to use each back end it also gives the common syntax of the output of the back ends In the appendix the XEmacs mode is described and the semantics of the HLPSL and IF speci fication languages are detailed 1 4 Contact For contacting the AVISPA Team either for questions or for proposing improvements or for bug reports please do not hesitate to use the following mailing list avispa users avispa project org You need to subscribe to the above list either by sending an empty e mail to avispa users join avispa project org or by following the link below http www avispa project org mailman listinfo avispa users All registered AVISPA tool users will also receive your message AVISPA Tool v1 1 User Manual 2 USER SECTION 9 2 User Section This section describes the easiest way to use the AVISPA tool to specify protocols in HLPSL then to run the avispa script for analysing it
38. ages one at the time A 1 1 The Transition System TLA specifies a transition system by describing its allowed behaviours by means of a single formula of the form A System A Inits A A ONeat A A where A is the set of state variables ranging on a domain D A refers to this set of variables in the next state Inits and Next are formulae representing the initial states and the next state relation respectively The above formula corresponds to a transition system T 2 7 gt where X the set of states is a set of total assignments o A gt D Z C Y is the set of initial states that is for each co T E Inits A finally C Y x X is the transition relation such that 01 gt 07 iff E ouo Next A A where o 2 d x d o For a sequence of states 7 00 01 we define r 1 0 T 0 0 41 and T lt 09 01 0 for i 0 1 and we say that m is a behaviour in T iff o 0 1 for each PO an A 1 2 Events and Actions A state predicate is a TLA formula on a role s state variables and constants Examples of valid state predicates include X 5 and S done A transition predicate is similar but may include primed variables If V is a tuple of state variables and V the correspondent tuple of primed state variables then we define the set of actions as those transition predicates p V V with the property that VV JV p V V Actions may therefore include s
39. als for secrecy and authentication PropertiesSection section properties PropertyDeclaration PropertyDeclaration property PropertyID VariableList LTL_Formula PropertylD AttackStatelD 1tl_ nat_ident LTL_Formula LTL_predicate lt gt LTL_formula LTL_formula LTL_formula LTL_formula LTL_formula LTL_formula LTL_formula LTL_formula gt LTL_formula LTL_formula LTL_formula LTL_predicate Fact PositiveCondition In such temporal formulas lt gt means sometimes in the past means one time in stant in the past means globally in the past The other symbols are standard logical connectives conjunction disjunction implication and negation respectively j Section for attack states This is a second goal section containing descriptions of states repre senting attacks The contents of this section comes from the HLPSL macro goals for authentica tion and secrecy AttackStatesSection section attack_states AttackStateDeclaration AVISPA Tool v1 1 User Manual 3 1 Generating an IF Specification 46 AttackStateDeclaration attack_state AttackStateID VariableList CState AttackStateID secrecy_of_ const_ident authentication_on_ const_ident weak_authentication_on_ const_ident k Section for intruder behaviour This section contains the descript
40. amely it reads every message that the agents write on these channels analyses the messages i e generates terms and messages based on them and inserts the composed messages into any receiving channel RCV Unlike knowledge of roles the knowledge of the intruder IK is made explicit in the formulae of Figure 5 and Figure 6 Namely the set K contains all the terms that the intruder may compose with respect to his knowledge The initial value of this TLA set variable is set explicitly in HLPSL it is the union of the sets defined in the intruder_knowledge declarations and monotonically increases according to the formulae of Figure 5 as the intruder reads a new message from a channel SND 14 as he analyses his knowledge by decomposing a pair into its components 15 or decrypting encrypted terms if he possesses the appropriate key 16 or as he composes new terms generating pairs 17 encrypting a message using a known key 18 or generating fresh terms 19 1 Part of the intruder behaviour is thus formalised by the formula of Figure 6 Read SNDi Amemsg A SND m A IK IK U m 14 ASplit Armiyn2eMsg A pair ml m2 IK A IK IK U m1 m2 15 AAdec Akmemsg acrypt k m IK A inv k IK IK IK U m 16 GPair Amimiems A m1 IK A m2 IK A IK IK U pair m1 m2 17 GAcrypt Akmemsg A k IK A me IK A IK IK Ufacrypt k m 18 GFresh JAsems WUsed A x
41. ansition sp gt act expresses that whenever we are in a state that fulfils state predicate sp we may make a transition labelled by the action act into a new state Note however that we do not require that this transition fire right away When and if it does fire we obtain the new state by taking the old state and applying any side effects that act might produce that is any state variables not affected by act remain the same We call such transitions spontaneous because although they are enabled whenever state predicate sp is true they convey nothing about when they must fire Immediate reaction transitions on the other hand have the form event gt act and relate a trigger event event on the LHS with an associated action act on the RHS This expresses that whenever we take a transition that satisfies the non stutter event predicate event then we must immediately more precisely simultaneously execute action act Hence as soon as event holds we obtain the new state by taking the old state and applying any side effects that act might produce that is any state variables not affected by act remain the same A 1 4 Communication Channels and Signals Communication takes place over channels which are themselves merely variables with values like any other By convention we generally assign channels convenient names like SND and RCV and then write SND Msg and RCV Msg This is however merely a shorthand The former action
42. are syntactically similar they differ only by the context in which they are used An action can be the assignment of a variable possibly with a fresh value e g Na new the call of a user defined predicate such as sending a message in a channel or the call of predefined goal predicates The expression assigned to a variable can be either a stutter one or a non stutter one In any transition the old value and the new value of a variable are syntactically distinguished the prime symbol has to be attached to the name of a variable for considering its new value Examples M M _K and Snd M M Reactions Actions Actions AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 16 Action Action Action var_ident Expression var_ident 2 new y const_ident Expressions_list var_ident Expression secret Expression const_ident Expression witness Expression Expression const_ident Expression request Expression Expression const_ident Expression wrequest Expression Expression const_ident Expression The four predefined goal predicates listed above contain the following information e secret E id S declares the information E as secret shared by the agents of set S this secret will be identified by the constant id in the goal section e w
43. at as we remarked above the translation performed by the HLPSL2IF translator defines a semantics for the HLPSL in terms of the IF which provides an alternative to the semantics of HLPSL based on TLA see Appendix A The basis of the semantics are terms which are built from the constants and function symbols of the prelude and the IF files As it is the case for HLPSL we assume that all terms are interpreted in the quotient algebra of the free algebra and the equational theory defined in the prelude file To smoothly integrate the existential quantifier we assume a set of fresh constants that is disjoint from all constants in the prelude and if file For these constants we assume a function fresh that maps a state and a set of variables to a substitution that replaces the variables with constants that do not appear in the given state Types Let type be a partial function that yields for every constant and variable the respective type that has been declared Note that our syntax allows also compound types see Section 2 1 1 e g M scrypt symmetric_key pair nonce agent Such a variable declaration is used when the receiver is not supposed to analyse a certain message part according to the protocol For instance in the case of the Otway Rees protocol A should send to B a message M that is encrypted with a key K 4s that is shared between A and a trusted server S B has to forward this message M to S and cannot read it himself Henc
44. ated file suffixed by hlpsl atk or if The changes also automatically add the path to the Emacs repository where the mode files are This repository does not have to be a global one 4 1 2 Usage a First steps The Avispa XEmacs mode permits to specify and analyse protocol specifications in an integrated environment The usual starting point of analysis is the opening of a hlpsl file The Avispa mode once correctly installed automatically detects this kind of files on account of its suffix hlpsl Several buttons then appear on the menubar AVISPA lt lt Process file gt gt Main Update These buttons have the following role e AVISPA permits to open the Avispa menu to customize the mode and change the backend as well as its options e lt lt and gt gt permit to navigate among the different files if atk related to the specification of a protocol One can customize whether the successor of a atk file is itself or the corresponding hlpsl file Process file permits to launch either the hlpsl2if compiler on the current HLPSL buffer or the current backend on the current buffer e The Main jumps to a buffer in which the status of all specifications in the repository is represented From this buffer it is also possible to launch action on the specifications e When a tool is launched asynchronously with XEmacs th
45. atically generating documentation of HLPSL specifications Thanks to the use of predefined notations in HLPSL comments sections and information are identified The two possible documents generated are AT fXand HTML with the respective scripts hlpsl2latex and hlpsl2html Their syntax is hlpsl2latex OPTIONS INPUTFILE hlpsl gt OUTPUTFILE tex hlps12html OPTIONS INPUTFILE hlpsl gt OUTPUTFILE html For more information about options and syntax conventions see the README file in the package And for installation instructions see the INSTALL file Note that a third script is also available for removing useless comments starting with hlpsl2clean INPUTFILE hlpsl gt OUTPUTFILE hlpsl AVISPA Tool v1 1 User Manual 74 A HLPSL Semantics A 1 Preliminaries The semantics of HLPSL is based on the Temporal Logic of Actions 13 TLA for short a powerful logic which is well suited to the specification of concurrent systems like security protocols TLA itself has an intuitive and easily understandable semantics making it a formalism that protocol designers and engineers can find accessible Although TLA allows for the description of parallel processes in the context of HLPSL we model protocols by providing an interleaving semantics The latter is obtained by restricting the capabilities of the Intruder see Section A 2 3 in the case of the Dolev Yao 11 intruder model for instance we make the intruder send mess
46. ays one of these roles in one session and legitimately learns the secret then he can re use this value in some other session where he does not play the role of a honest agent to masquerade as one of the honest agents while the other agents believe that the value is a shared secret between honest agent only and this attack cannot be detected Still this should not be a serious problem since it is indicative of an authentication attack which should be found nevertheless If a role played by A shares a secret T with some player U of another role and the identity of U is not accessible for A e g because of anonymity the predicate secret T t U cannot be given in the role of A In this case it should be given in the role of U instead right after the transition that sends T to U has been authenticated e Authentication is modelled by means of several goal predicates witness A B id T1 request B A id T2 and wrequest B A id T3 The protocol designer should respect the following criteria suppose you want to express that agent X playing role rX weakly authenticates agent Y playing role rY on some information T then it is expected that in the HLPSL goal section this property is written authentication_on id resp weak_authentication_on id where id is a label of type protocol_id for uniquely representing this goal in role rX agent X states a request X Y id T1 resp wrequest X Y id T1 predicate in the r
47. b_nb A2Goal A1Goal MGoal SID1 SID2 request A1Goal A2Goal alice_bob_nb MGoal SID1 request A1Goal A2Goal alice_bob_nb MGoal SID2 amp not equal SID1 SID2 amp not equal A2Goal i attack_state authentication_on_bob_alice_na A1Goal A2Goal MGoal SID request A1Goal A2Goal bob_alice_na MGoal SID not witness A2Goal A1Goal bob_alice_na MGoal amp not equal A2Goal i attack_state replay_protection_on_bob_alice_na A2Goal A1Goal MGoal SID1 SID2 request A1Goal A2Goal bob_alice_na MGoal SID1 AVISPA Tool v1 1 User Manual 3 2 Analysing a IF Specification 54 request A1Goal A2Goal bob_alice_na MGoal SID2 amp not equal SID1 SID2 amp not equal A2Goal i 3 2 Analysing a IF Specification This section contains the description of the use of each back end provided by the AVISPA tool 3 2 1 Using CL AtSe The CL based Model Checker CL AtSe 17 provides a translation from any security protocol specification written as transition relation in the IF into a set of constraints which can be effec tively used to find attacks on protocols Both translation and checking are fully automatic and internally performed by CL AtSe i e no external tool is used In this approach each protocol step is modeled by constraints on the adversary s knowledge For example a message received by an honest participant is a forgeability constraint for the adversary Conditions like equality inequality non
48. cation and the cause of the errors e Back end execution problems the printed message should be explicit 2 2 3 Interpreting the Output When the analysis of a protocol has been successful by finding an attack or not the output describes precisely what is the result and under what conditions it has been obtained The first printed section is SUMMARY it indicates if the protocol is safe unsafe or if the analysis is inconclusive AVISPA Tool v1 1 User Manual 2 USER SECTION 37 In any case a second section titled DETAILS will either explain under what conditions the protocol is declared safe or what conditions have been used for finding an attack or finally why the analysis was inconclusive The next sections PROTOCOL GOAL and BACKEND recall the name of the protocol the goal of the analysis and the name of the back end used respectively After some possible comments and statistics the trace of the attack if any is printed in an Alice amp Bob notation More information on the format of the output produced by the AVISPA Tool is given in Section 3 3 2 2 4 Example For running the AVISPA tool on the NSPK Key Server protocol with the back end CL AtSe the command is avispa NSPK KS hlpsl cl atse ns short Note that we have given two options to CL AtSe ns for no simplifications the output prints all the steps short for getting one of the shortest attacks The output is listed hereafter and shows that a
49. ce state Acceptance is used for sequential composition to mark the stop states after which the following instantiation may begin AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 14 Accept_declaration accept Predicates However since sequential composition is not fully handled in the current version of the AVISPA tool accept declarations are useless k Declaration of intruder knowledge The knowledge given to the intruder is defined by a set of constants assigned variables either parameters or initialised local variables or messages build with constants and assigned variables IKnowledge_declaration intruder_knowledge Stutter_expressions_list This knowledge is given to the intruder in a role but the full knowledge of the intruder is the union of all the knowledge given to him in all instances of basic and composition roles However in general intruder knowledge is only defined in the main role ex environment l Transitions in basic roles The transitions in a basic role are either spontaneous actions enabled when the state predicates on the left hand side are true or immediate reactions fired immediately whenever the non stutter events that is events based on the change of some variables values on the left hand side are true Transition_declaration transition Transition Transition Label Predicates gt Actions spontaneous action Label Event
50. cl atse runs the translator no particular option then CL AtSe ofmc runs the translator no particular option then OFMC satmc runs the translator no particular option then SATMC ta4sp runs the translator no particular option then TA4SP Default hlps12if AVISPA Tool v1 1 User Manual 2 2 Analyzing a HLPSL Specification 36 e MOPTION help display the module help and exit version output module version information and exit e MOPTIONS options given to the selected AVISPA sub module Default no particular option e FILE the HLPSL file or IF file when no hlpsl2if is used to be analyzed Not all combination of the above settings are allowed The allowed combinations are indicated in the following table typed model yes no strongly cl atse y vy ofmc Y yv satmc y J ts4sp y All options for backends are detailed in the files cl bash ofmc bash satmc bash and ta4sp bash in the directory AVISPA_PACKAGE bin backends For some backends a file satmc config ta4sp config lists the default options 2 2 2 Generated Errors If some errors are detected during the execution of the avispa script a message will indicate the encountered problem The most standard errors are e HLPSL specification problems the name of a log file is given usually in the directory AVISPA_PACKAGE 1logs this file contains information about the lo
51. d to be applied on transitions in which the channel macro has been replaced with its appropriate conjunction of predicates see section A 1 4 Intuitively formula 1 of Figure 4 states that initially Init B holds and in every step the above conjunction of formulae denoted with Next B must be satisfied Namely 2 states that if an event is triggered then the changes specified by the corresponding action take place the fresh variables updated by the transition are assigned to different values that have never been used as fresh value by this transition although it is not explicitly stated the player s knowledge is implicitly extended with all the terms that can be derived by analysing the messages received and SHowever it is recommended to avoid ownership of channels since it can be cause of clashes with the TLA formulae declared for the intruder For instance if an agent knows a symmetric key k and receives a cyphertext M then M is added to the knowledge AVISPA Tool v1 1 User Manual A 2 Formal Semantics 78 TLA B Init B AU Nezt B 1 where Nezt B is defined as A As eu A act 2 A A v1 v2 in Y trj B vr va A Nw in Y 8 Y E Used Av Usedyg tr A izj Used 8 tr N Used 5 tr 0 A w in Q B w w gt Mod w B Usedg ls Used 8 tr Usedg C Usedg with Mod B Vo ev x occurs in tr 7 Figure 4 Translation of a basic role in into TLA we assume th
52. e Update permits to refresh the content of the current buffer once the tool has terminated b The Avispa menu The Avispa menu permits to change the behavior of the tools when analyzing a specification Before describing the possible options its first use is to select a specific backend for the analysis of a IF specification button Backends AVISPA Tool v1 1 User Manual 4 CONTRIBUTIONS 69 Options _Backends CL Atse Customize v Ofime Help ur satMC v TAASP The Customize item permits to access to the customization of the variables in the avispa tools group the most useful ones The customization permits to change some default values permanently see Section 4 1 3 for more information on this topic The Help permits to launch a small help file c The options This submenu is accessed via the Options of the Avispa menu There are two kinds of options e The Avispa options which relate to all backends and have to be handled by all tools e The tool specific options each related to a specific backend The former are immediately accessible in the Options submenu while the latter are accessible via the More Options button Both kind of options are described in previous sections of this manual but for the Verbose option which if unselected suppresses the hlpsl2if compiler warnings on the type of
53. e an intruder impersonating A can send any message in the place of M since B will not try to analyse it For a typed model however we want B to accept M only if it is of the proper format according to the protocol i e if it is an encryption with a symmetric key and the contents after decryption are also of the proper format In other words even though B cannot decrypt the message we assume that he can check whether the received message is of the correct type and pattern and reject it if not Semantically let op be an n ary IF operator M a variable and t t types atomic or themselves composed Then the declaration M op ty tn is equivalent to the declarations Mi 1 Mn tn AVISPA Tool v1 1 User Manual 84 if M with i 1 n are fresh variables that do not appear in the IF file and every occurrence of M in the IF file is replaced with the term op M4 Ma One may hence see composed types as syntactic sugar but they allow us to write the rules for an IF file independent of the question of typing so that the same IF specification can be analysed with respect to both the typed and the untyped model simply considering or not the signature and types sections Unification We define E unification on IF terms in the standard way i e unification modulo the algebraic the ory E defined by the equations of the prelude file only that types have to be respected Formally a unifier of two terms is
54. e equivalent of the Protocols Hlpsl Repository Path variable with regards to the resulting result files suffixed by atk It is also used to determine the full path to the auxiliary output files of a backend Currently only samtc and ta4sp generate such files that contain statistics on the analysis The second subset of variables in the avispa tools group concerns the behavior of XEmacs when calling the translator or a backend e Synchronous Compilation This variable controls whether XEmacs shall spawn a new concurrent process to compile an HLPSL specification or if it should wait the result of the compilation before resuming execution If it is set to a non nil value e g t it enables the automatic jump to the corresponding Intermediate Format buffer if Fetch Result is also non nil AVISPA Tool v1 1 User Manual 4 1 XEmacs mode 72 e Synchronous Validation Set this value to true if you want XEmacs to wait for the result of the backend before resuming execution This enables the automatic jump to the corresponding Result buffer if Fetch Result variable is also set to true When a backend or the compiler is launched asynchronously one need to use the navigation buttons lt lt and gt gt to go to the result buffer Once in the right buffer one should use Update to see the result This should be done only once the tool has terminated Fetch Result Set this value
55. e player to be always able to compose the messages he is going to send Conjunction 3 imposes that the sets of fresh values issued by different transitions are disjoint Besides this 4 states that if one of the variables owned by the role changes then the variable is actually modified by this role It is our convention that if a role owns a variable then this variable is never modified by any role outside the current one Finally 5 defines a TLA variable representing all the fresh values used by the role B and 6 imposes that such a set grows up monotonically An agent may simultaneously participate both in different roles and in different sessions of the protocol In this case the two role instances could share some internal variables of the agent This variable sharing is not done through channels but it is a straightforward consequence of using the same TLA variable in both the formulae representing the roles that share the variable In this version of the AVISPA Tool only the sharing of variables of type set is allowed Note that a transition that has to refer to the already known value of a variable will use the name of this variable without prime sign in any side of the transition Viceversa when a transition has to assign a value to a variable will use the name of this variable with prime Lastly let B be a basic role With B we denote the role obtained from B by replacing the variable U with the value p and by replacing eac
56. en different server requests it is useless to declare KeyRequest of type message You can use a constant keyrequest of type protocol_id in the topmost level role e g Environment and accordingly you can declare a variable KeyRequest of type protocol_id in the ap propriate roles j Knowledge The knowledge of a honest agent A playing the role alice is intended 1 to contain all the parameters of the role alice 2 to contain all the local variables of the role alice 3 to be sufficient to execute all its transitions For instance if you declare for alice a transition St 0 RCV M _Ka gt St 1 SND M every time the event in the left hand side is fired then it is assumed that A has enough information to get M e g A may know the inverse key of Ka Suppose the intruder is playing the role alice then the intruder s knowledge is supposed to contain all the terms given as parameter of the corresponding instance of the role alice But this knowledge is not automatically given to the intruder all intruder s knowledge will have to be declared as a set of terms in the intruder_knowledge declaration of roles As a rule of thumb the whole intruder s knowledge should be put in one single intruder_knowledge declaration in composition roles In case there are more than one intruder_knowledge declarations e g one per basic role the total intruder knowledge is intended to be the union of the sets defined in those decla
57. ep step_5 B A Kb Ks KeyRing Dummy_Na Nb Dummy_Ka Set_48 SID Na state_bob B A Kb Ks KeyRing 2 Dummy_Na Nb Dummy_Ka Set_48 SID iknows crypt Kb pair Na A not contains pair A Ka KeyRing gt state_bob B A Kb Ks KeyRing 3 Na Nb Dummy_Ka Set_48 SID iknows pair B A step step_6 B A Kb Ks Dummy_KeyRing Na Nb Dummy_Ka Set_48 SID Ka state_bob B A Kb Ks Dummy_KeyRing 3 Na Nb Dummy_Ka Set_48 SID iknows crypt inv Ks pair A Ka AVISPA Tool v1 1 User Manual 3 1 Generating an IF Specification 52 gt state_bob B A Kb Ks Dummy_KeyRing 2 Na Nb Ka Set_48 SID contains pair A Ka Dummy_KeyRing step step_7 B A Kb Ks KeyRing Dummy_Na Dummy_Nb Dummy_Ka Dummy_Set_48 SID Na Nb Ka state_bob B A Kb Ks KeyRing 2 Dummy_Na Dummy_Nb Dummy_Ka Dummy_Set_48 SID iknows crypt Kb pair Na A contains pair A Ka KeyRing exists Nb gt state_bob B A Kb Ks KeyRing 5 Na Nb Ka Dummy_Set_48 SID iknows crypt Ka pair Na Nb secret Nb snb Dummy_Set_48 witness B A alice_bob_nb Nb contains A Dummy_Set_48 contains B Dummy_Set_48 contains pair A Ka KeyRing step step_8 B A Kb Ks KeyRing Na Nb Ka Set_48 SID state_bob B A Kb Ks KeyRing 5 Na Nb Ka Set_48 SID iknows crypt Kb Nb gt state_bob B A Kb Ks KeyRing 7 Na Nb Ka Set_48 SID request B A bob_alice_na Na SID section properties property secrecy_of_sna MGoal ASGoal Csecret MGoal sna ASGoal
58. exity as SAT i e NP complete Usage SATMC can be invoked by typing on the command line satmc lt filename gt prelude lt fileprelude gt max lt number gt encoding lt encoding gt mutex lt number gt solver lt solver gt sc lt bool gt ct lt bool gt oi lt bool1 gt where lt filename gt and lt fileprelude gt are respectively the IF problem to be analysed and the prelude file and each option is described as follows e max maximum depth of the search space up to which SATMC will explore the parameter max can be set to 1 meaning infinite but in this case the procedure is not guaranteed to terminate by default it is set to 30 AVISPA Tool v1 1 User Manual 3 2 Analysing a IF Specification 60 encoding the selected SAT reduction encoding technique The techniques currently imple mented are the linear encoding 1 value set to linear and two graphplan based encodings one using the backward chaining schema 3 value set to gp bca and the other one apply ing the explanatory frame schema value set to gp efa the default value for this option is gp efa Some values for this option are supported for backward compatibility with the IF v 1 specifications 7 mutex level of the mutex relations to be used during the SAT reduction if set to 0 then the abstraction refinement strategy provided by SATMC see 2 for more details is en abled otherwise the abstraction refinement strateg
59. ey will be given a value according to the standard layout of the avispa package e More specific variables can be given by the installer of the package to customize the instal lation AVISPA_XEMACS_DIR directory where the elc files will be installed The user must be able to create and write into this directory AVISPA_BIN_DIR directory relative to which the tools hlpsl2if compiler and back ends can be found Must be user readable since the presence to the tools is checked AVISPA_HLPSL_DIR AVISPA_IF_DIR AVISPA_RESULTS_DIR variables denoting respectively the directories where the HLPSL and the IF specifications are and where the backends results are stored When one of the above variables is set it has precedence over the default layout of the installation If none of the above variables is set in the environment of the avispa mode bin program the values are requested from the user In case of an independent installation under a unix system we suggest to use the env command to set the variables For example one can use env AVISPA PACKAGE usr local avispa avispa mode bin AVISPA Tool v1 1 User Manual 4 1 XEmacs mode 68 It is assumed that one has a working version of XEmacs to compile the mode files This means that it is currently not possible to install the mode on a server that does not have XEmacs The init el file of the user is changed to auto load the avispa mode when opening an avispa rel
60. f options help Display this list of options 3 1 2 The IF Specification Language In the following we give the entire BNF of the IF with the usual conventions a Lexical entities In IF the conventions are the same as in HLPSL all variables start with a capital letter and constants start with a small letter natural numbers can also be used as constants without any specific interpretation var_ident A Z A Za z0 9_ const_ident a z A Za z0 9_ nat_ident 0 9 Comments start by the symbol and finish at the end of the line b Prelude and IF files The grammar has two start symbols Prelude and IF_File The first one permits to describe the pre defined file prelude if containing general information about protocols specifications in IF available types super types signature of functions and predicates variables and constants declaration equations and the intruder behaviour For more information on this file see Section 3 1 3 The second start symbol corresponds to the description of a protocol specification in IF signature of role states variables and constants declaration initialisation transition rules properties to satisfy and attack states to reach Prelude TypesymbolsSection SignatureSection TypesSection AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION Al EquationsSection IntruderSection IF_File SignatureSection TypesSection InitsSection RulesSection PropertiesSection
61. gs creates a template for a goal section AVISPA Tool v1 1 User Manual 4 CONTRIBUTIONS 71 e The predefined hlpsl keywords currently defined are ao authentication_on keyword wa weak_authentication_on keyword s_o secrecy_of keyword ik intruder_knowledge keyword To use an abbreviation just write its three letters and then a space b The avispa tools group A first subset of the variables in the avispa tools group concerns the directories where the files are to be found e Tools Path This is the repository where the tools of the Avispa Project are Note that the full path to the executable used is constructed dynamically from the value of this variable and from the name of the executable e Protocols Hlpsl Repository Path This variable specifies the repository containing the HLPSL specifications It is used when calling the hlpsl2if compiler to construct the full path to the protocol specification It is also used when navigating among files see Section 4 1 2 This path should not end with a slash otherwise XEmacs may get confused during the navigation and opens the same file twice which is unnecessary e Protocols If Repository Path This is the equivalent of the Protocols Hlpsl Repos itory Path variable with regards to the Intermediate format files It is also used by the hlpsl2if compiler to determine the full path to the output file compiler e Protocols Results Repository Path This is th
62. h function apply F Arg apply message message gt message intruder knowledge iknows ki iknows message gt fact set element contains a set_1 contains message set gt fact witness for authentication witness A B id Msg witness agent agent protocol_id message gt fact request for strong authentication request B A id Msg RoleID request agent agent protocol_id message nat gt fact request for weak authentication wrequest B A id Msg RoleID wrequest agent agent protocol_id message nat gt fact secrecy secret Msg id AgentSet secret message protocol_id set agent gt fact section types declaration of the pre defined constants true false bool declaration of the variables used in this file PreludeK PreludeM PreludeM1 PreludeM2 PreludeM3 message section equations associativity of concatenation pair PreludeM1 pair PreludeM2 PreludeM3 pair pair PreludeM1 PreludeM2 PreludeM3 identity of double inverse inv inv PreludeM PreludeM AVISPA Tool v1 1 User Manual 3 1 Generating an IF Specification 48 section intruder commutation of exponents exp exp PreludeM1 PreludeM2 PreludeM3 cancellation of inverse exponents exp exp PreludeM1 PreludeM3 PreludeM2 exp exp PreludeM1 PreludeM2 inv PreludeM2 PreludeM1 associativity of xor xor PreludeM1 xor PreludeM2 PreludeM3
63. h variable A A with Ap On composed roles P denotes P itself acting as the identity function This is done in order to keep same basic role instances distinct when they are involved in parallel compositions AVISPA Tool v1 1 User Manual A HLPSL SEMANTICS 79 The TLA translation of the parallel composition of R1 Re Rm is as follows TLA P A AZ TLAR A Init P ADA VARO in P w Zw gt Mod w P A NNa in apy X A gt Mod P A N y Used A Usedp J Used where p1 P2 Pm are the positions of TLA R TLA R3 TLA R respectively in the tree of the main role at the topmost level of the HLPSL hierarchy and 1 Mod x P V Mod x R It is thus defined as the conjunction of each component role TLA R see 8 and some terms accounting for extra initial constraints see 9 taking ownership of variables see 10 and freshness see 12 Namely 10 states that if a variable is owned by P then the value of such variable can be modified only by applying transitions of any of the component roles R Same goes for local variables 11 a local variable can be modified only by any of the component roles For what concerns freshness 12 imposes that the sets of fresh values issued by all roles R are disjoint and 13 defines a TLA variable that keeps track of those fresh values that have already been used by P i e the union of the fresh values used by each R Moreover it is im
64. he value of term T is a secret shared only between agents A and B The secrecy property is AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 26 violated everytime the intruder learns a value that is considered as secret and that he is not allowed to know Note that if in a certain session the intruder plays the role of a honest agent that is allowed to know the secret value then the intruder is allowed to know it and no attack is reported for this value The label id of type protocol_id is used to identify the goal In the HLPSL goal section the statement secrecy_of id should be given to refer to it The set of agents sharing the secret has to be written as a constant set and not by using a variable of type agent set The secrecy events should be given as early as possible i e right when the secret term has been created in the respective role s because the secrecy check takes effect only after the events have been issued and it will stay in effect till the end of the protocol run If a value T that should be kept secret is determined by a single role in particular if it is an atomic value like a nonce produced by new then the secrecy statement should be given in and only in the role introducing the value If the secret is a combination of ingredients from several roles then secrecy predicates should be given in all roles contributing to the non atomic secret value Unfortunately if the intruder pl
65. his information is then used to reduce the step interleaving CL AtSe is able to take advantage of the algebraic properties of the XOR operator and most properties of the exponential More precisely e XOR CL AtSe implements both the unification of messages modulo XOR and the intruder deduction rules over terms with the XOR operator This implementation is both correct and complete that is CL AtSe fully support the XOR operator AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 55 e Exponential CL AtSe also implements both the unification of messages modulo the expo nential and the intruder deduction rules over terms with exponential just like XOR but with the single exception of the rule g g This means that for CL AtSe an exponential over g which product of exponents evaluates to 1 is not equivalent to g alone Note that this rule is anyway meaningless in practice as soon as some header identify the exponen tials in messages and as soon as the intruder knows g from the beginning very realistic hypothesis In order to model the algebraic properties of certain operators like Xor CL AtSe implements a variant of the Baader and Schulz unification algorithm optimized for XOR and usable for the exponential Please visit the CL AtSe s web site http www loria fr equipes cassis softwares AtSe for updates of CL AtSe Finally CL AtSe produces nice human readable attack descriptions when one is found In partic
66. his section we will show how to express a security protocol specified in HLPSL asa TLA formula We will formally give the meaning of checking that a security protocol achieves its security properties under an hostile environment A 2 Formal Semantics A 2 1 Messages We begin by specifying the structure of messages and the properties of the operations on the set Msg of all messages Particularly we will focus on pairing pair M M2 M M and asymmetric encryption acrypt K M M x but we can easily extend this model of messages to include other operators like symmetric encryption exponentiation XOR and their associated properties In general HLPSL allows for the declaration of algebraic equations that specify an equa tional theory Let Q be the signature from which Msg is constructed the interpretation of HLPSL is required to be a quotient interpretation of a free term algebra Zo modulo the equa tional theory see 18 For instance could include an equation stating that pairing is associative Pair Pair m1 m2 m3 Pair m1 Pair m2 m3 equations expressing properties of cryptographic algebraic operators e g the associativity and commutativity properties of the XOR operator properties on the inverse of an asymmetric key like inv inu k k etc A 2 2 HLPSL Roles In this subsection we show how HLPSL roles are mapped into TLA Figure 3 shows the structure of a basic role denoted with B and of a composed role deno
67. ic techniques to represent the state space as described in more detail in 10 9 Thanks to these techniques OFMC can be employed not only for efficient falsification of protocols i e fast detection of attacks but also for verification i e proving the protocol correct for a bounded number of sessions without bounding the messages an intruder can generate The most significant new feature of OFMC in this release is that the user can specify an alge braic theory on message terms modulo which the analysis of the protocol is performed For more information on using algebraic theories see the file user guide algebraic pdf in the docs ofmc directory included in this distribution Example theories and sample IF specifications that em ploy algebraic theories can be found in the directory testsuite algebraic Usage OFMC is invoked by typing on the command line ofmc lt filename gt theory lt theoryfile gt sessco untyped d lt number gt p lt number gt e lt filename gt is an IF file to be checked e The theory option allows the user to specify a custom algebraic theory given in the file lt TheoryFile gt See the file user guide algebraic pdf in the docs ofme directory for more information including details about the default algebraic theory used by OFMC See also the examples in the directory testsuite algebraic Note that user defined theories are currently only supported for protocols specified directl
68. ight hand side of some of its transitions x in role rY agent Y states a witness Y X id T2 predicate in the right hand side of some of its transitions AVISPA Tool v1 1 User Manual 2 USER SECTION 27 Note that T1 and T2 may be different terms but they should have the same value such that the two events match the protocol ID that appears in the third position of witness request and wrequest facts must be declared of type protocol_id in a const declaration For example authentication_on nb should use witness request facts with nb in the third slot and the following declara tion should appear in the specification const nb protocol_id you should not use variables for protocol identifiers inside goal predicates otherwise this would be impossible to run the analysis on one specific goal one option of the AVISPA tool when used by an expert user This means that for instance you should not write witness A B ID Term even if the constant value term is passed to the role as value for the variable ID You should write directly witness A B term Term The same applies for request wrequest and secret f Transitions e In the left hand side of a transition learned information is represented by primed vari ables So primed variables can only be used when receiving a message in a channel when decomposing a message or when searching for some information in a set For instance Rev X X X1 X2 means to ass
69. ign X to the message sent on the channel Rev and this message is a pair whose elements are assigned to X1 and X2 e Variables intended to be fresh must be written as primed in the right hand side of a transition assigned to new and they should not occur as primed in the left hand side For instance the following transition 1 State 0 Rev start gt State 1 Nb new Snd Nb Text1 shows that Nb is assigned with a fresh value g Initial value In every role a variable such that e it occurs inside the local declaration therefore it does not occur in the parameter list of the role and AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 28 e it is not of type channel and e there does not exist a left hand side of a transition in which the variable occurs primed and e it is not assigned in a right hand side of a transition with a fresh value should be given an initial value For summarising a local variable has to be initialised if its first use is unprimed h Constants e In HLPSL it is not mandatory to declare the types for constants However not all the types of constants can be uniquely inferred by the translator For instance suppose you declare a constant intended to be of type text but without to specify its type and suppose you use such a constant only inside a message Then the translator can only infer that this constant is of type message Hence for
70. ion of the intruder behaviour represented by transition rules IntruderSection section intruder RuleDeclaration In the current version of the AVISPA tool this section is unique because only the Dolev Yao model is supported In a close future it should be parametrised by the model to consider 3 1 3 IF Prelude File The IF prelude file prelude if contains some information about the IF syntax for back ends It also contains the description of equational properties of some operators such as pair exp and xor and the intruder s behaviour in the Dolev Yao model section typeSymbols agent text symmetric_key public_key hash_func message fact nat protocol_id bool set section signature message gt agent message gt text message gt symmetric_key message gt public_key message gt hash_func message gt nat message gt protocol_id message gt bool concatenation pair Msg1 Msg2 pair message message gt message AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 47 asymmetric encryption crypt Key Message crypt message message gt message inverse of a public key private key inv Key inv message gt message symmetric encryption scrypt Key Message scrypt message message gt message exponentiation exp Base Exponent exp message message gt message exclusive or xor N1 N2 xor message message gt message application of a has
71. itness A B id E for a weak authentication property of A by B on E declares that agent A is witness for the information E this goal will be identified by the constant id in the goal section e request B A id E for a strong authentication property of A by B on E declares that agent B requests a check of the value E this goal will be identified by the constant id in the goal section e wrequest B A id E similar to request but for a weak authentication property n Composition of roles Roles basic and or composition can be composed in parallel or sequen tially Such scenarios are described in the composition section of so called composition roles Definition of the composition section for composed roles Composition_declaration composition Compositions_list Compositions_list Composition Composition Bracketed_par_compositions_list parallel Composition Bracketed_seq_compositions_list sequential Compositions_list Note that in the current version of the AVISPA tool sequential composition of roles is not handled yet AVISPA Tool v1 1 User Manual 2 USER SECTION 17 Composition Role_instantiation _ Parameters_instance Bracketed_compositions_list Parameters_instance in Concatenated_variables_list Stutter_expression Concatenated_variables_list Concatenated_variables Concatenated_variables Concatenated_variables
72. itutions p for the remaining variables i e those variables that appear only in negative facts and in negative conditions see 23 we postulate that none of the negative facts under gp is contained in the state and none of the conditions is satisfied for ap see 24 We recall that the right hand side of the rule can only contain variables from the positive facts of the LHS and the existentially quantified variables which will be replaced by fresh constants below therefore all substitutions that result from matches are ground and so are all successor states Note also that matches is applied in the same way for attack states which are syntactically the same as a rule s LHS Figure 10 describes the semantics of a rule as a state transition function In there we use the applicability check matches Besides for this check the conditions and the negative facts of the rule do not play any role the transition itself is concerned only with the positive facts of the LHS of the rule the existentially quantified variables and the right hand side Intuitively if the rewrite rule is applicable to state s see 25 then its application leads to a state s obtained from s by removing the facts in the LHS of the rule and by adding those in the right hand side to the result see 26 where a different fresh constant is generated for any existentially quantified variable of the rule see 27 Note that here the semantics of a rule is defined as a sta
73. mediate to see that UZOR E AP UM ARP C ACP and UT Y RP C T P The TLA translation of sequentially composed roles which we omit here is analogous One must augment the translation with an auxiliary variable recording which of the roles is executing and take into account the acceptance conditions A 2 3 Intruder Model We formalise the capabilities of the intruder as a set of rules the intruder may execute We focus here on the well known Dolev Yao DY intruder model of 11 but note that the definition of alternate intruder models is a simple matter of axiomatically describing their capabilities In this way we can easily model a system in which the intruder has full DY capabilities over certain communication channels can only listen on others and has no access to a third set of channels The DY intruder controls any channel tagged with the dy attribute Let S and R be the number of sending and receiving DY channels used in a given protocol In the sequel SND and 10Notice that the sets of basic and composed roles are disjoint Therefore it is immediate to select the appropriate Mod predicate to be applied on a given role Notice that the monotonicity of Usedp simply follow by the monotonicity of each Used AVISPA Tool v1 1 User Manual A 2 Formal Semantics 80 RCV with 1 lt i lt S and 1 lt k lt R refer to sending and receiving DY channels respectively The DY intruder reads every sending channel SND n
74. more precise specifications it is better to specify the type of each constant used e The type of a constant cannot be a compound type For instance suppose you declare X text agent then you cannot declare x text agent and trying to instantiate X with x What you should do is to declare two constants x1 text x2 agent and then you can instantiate X with x1 x2 1 Messages e Please try to avoid variables of type message For variables please use compound types as much as possible Namely do not use compound types when the variable is assigned with a term that makes use of algebraic equations use compound types in the other cases E g when Na_Nb is a message that would represent a pair of texts declare Na_Nb text text instead of Na_Nb message AVISPA Tool v1 1 User Manual 2 USER SECTION 29 e When the form of the message is not important you can use the types protocol_id or text instead of message This is for instance the case in those protocols in which control messages like Failure Success etc are sent over the channels In this case it is useless to declare Failure and Success of type message since they will be used merely as constant messages instantiated in the topmost level role Please declare them of type protocol_id For instance in a protocol like A gt S A B KeyRequest S gt A B Kb where KeyRequest is just a predefined constant control message for distinguishing betwe
75. mputer Security Foundations Workshop IEEE Computer Society Press 2001 16 SAT The SAT Live Web Site http www satlive org 17 M Turuani The CL Atse Protocol Analyser In F Pfenning editor Proceedings of 17th International Conference on Rewriting Techniques and Applications RTA Lecture Notes in Computer Science Seattle WA August 2006 Springer 18 Sperschneider V and Antoniou G Logic A Foundation for Computer Science Addison Wesley 1991 19 zChaff The zChaff Web Site http www princeton edu chaff zchaff html 20 H Zhang SATO An Efficient Propositional Prover In W McCune editor Proceedings of CADE 14 LNAI 1249 pages 272 275 Springer Verlag 1997 AVISPA Tool v1 1 User Manual
76. n cons const def delete dy end exp goal hash hash_func iknows in init intruder_knowledge inv local message nat new not ota played_by protocol_id public_key request role secrecy_of secret set start symmetric_key text transition weak_authentication_on witness wrequest xor Some other constant names are reserved and will be automatically renamed if used in a specifi cation apply attack_state attack_states contains crypt dummy_agent dummy_bool dummy_chnl dummy_chnl_dy dummy_chnl_ota dummy_hash dummy_msg dummy_nat dummy_nonce dummy_pk dummy_set dummy_sk equal equations initial_state inits intruder leq pair properties property rules scrypt section step types In a HLPSL specification comments and separators e g white space new line and tabulation characters are ignored comments n spaces n r t b Structure of a HLPSL specification A HLPSL specification is composed of three parts a list of definitions of roles a list of declarations of goals if any and the instantiation read call of the main role usually without arguments SpecHLPSL Role_definition Goal_declaration Call of the main role ex environment Role_instantiation AVISPA Tool v1 1 User Manual 2 USER SECTION 11 c Definition of roles The roles in a specification are of two kinds basic roles played by agents and composition roles describing the scenario to co
77. n analyze IF specifications CL AtSe the Constraint Logic based Attack Searcher see Section 3 2 1 OFMC the On the Fly Model Checker see Section 3 2 2 SATMC the SAT based Model Checker see Section 3 2 3 TA4SP the Tree Automata tool based on Automatic Approximations for the Analysis of Security Protocols see Section 3 2 4 AVISPA Tool v1 1 User Manual 2 USER SECTION 35 2 2 1 Running avispa The syntax of the avispa command is one of the following avispa OPTION avispa MODULE MOPTION avispa FILE OPTIONS MODULE MOPTIONS where e OPTION can be h help display this help and exit v version output version information and exit e OPTIONS can be typed_model TM IF specifications can be generated both in an untyped variant set TM to no in a typed variant set TM to yes and in a strongly typed one set TM to strongly Default yes output DIR set the output directory to DIR Namely the IF file and any other file generated by the selected back end will be written in such a directory Notice that DIR must be an absolute path Default AVISPA_PACKAGE testsuite results nowarnings do not display warnings when executing the hlps12if transla tor no hlps12if do not call the hlps12if translator this option is useful for passing IF files directly to the tool e MODULE selects a specific AVISPA sub module Accepted values are hlps12if runs only the translator
78. nce if you plan to add your own verification tool to the AVISPA tool we recommend to follow the following output syntax AVISPA output format BNF Ree the following symbols are assumed ident a string int an integer number float a floating point number msg a string describing a message goalDescription a string describing a goal msg_ident a constant initial lower case letter or a variable initial capital letter o De comment uyi msg Output Summary Protocol Goal BackEnd Comments Statistics Trace Summary SUMMARY Result Result Conclusive Inconclusive AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 65 Conclusive SAFE ConclusiveDetails UNSAFE ConclusiveDetails ConclusiveDetails DETAILS ConclusiveExplanation ConclusiveExplanation ATTACK_FOUND STRONGLY_TYPED_MODEL TYPED_MODEL UNTYPED_MODEL BOUNDED_NUMBER_OF_SESSIONS BOUNDED_NUMBER_OF_SYMBOLIC_SESSIONS BOUNDED_SEARCH_DEPTH BOUNDED_MESSAGE_DEPTH Inconclusive INCONCLUSIVE InconclusiveDetails InconclusiveDetails DETAILS InconclusiveExplanation InconclusiveExplanation TIME_OUT MEMORY_OUT NOT_SUPPORTED OVER_APPROXIMATION UNDER_APPROXIMATION Comments COMMENTS msg Protocol PROTOCOL ident Goal GOAL ident BackEnd AVISPA Tool v1 1 User Manual 3 3 The Standard Output Format 66
79. nsider during analysis for example describing what is a session of the protocol or what instances of sessions should be used Roles may be either basic or compositional Role_definition Basic_role Composition_role d Definition of a role Roles are independent processes they have a name receive information by parameters and contain local declarations Basic roles are played by an agent whose name is received as parameter The actions of a basic role are transitions describing changes in their state depending on events or facts Basic roles must include a player definition and generally contain a transition declaration section Basic_role role Role_header Player Role_declarations Transition_declaration end role Used to bind the role and the identifier of the agent playing the role Player played_by var_ident Note that all the information of a basic role parameters and local variables represents the knowledge of the player of the role A composition role combines other roles either in parallel or in sequence Composition roles have no transition section but rather a composition section in which they call other roles Composition_role role Role_header Role_declarations Composition_declaration end role AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 12 e Declarations in roles The first element in a role is its header It contains the
80. on system accepts satisfies the formula as defined in HLPSL AVISPA Tool v1 1 User Manual REFERENCES 87 References 1 A Armando and L Compagna Automatic SAT Compilation of Protocol Insecurity Problems via Reduction to Planning In Proceedings of FORTE 2002 LNCS 2529 pages 210 225 Springer Verlag 2002 2 A Armando and L Compagna Abstraction driven SAT based Analysis of Security Pro tocols In Proceedings of SAT 2003 LNCS 2919 Springer Verlag 2003 Available at www avispa project org 3 A Armando L Compagna and P Ganty SAT based Model Checking of Security Protocols using Planning Graph Analysis In Proceedings of FME 2003 LNCS 2805 Springer Verlag 2003 4 Alessandro Armando and Luca Compagna An optimized intruder model for sat based model checking of security protocols In Proceedings of the IJCARO4 Workshop ARSPA 2004 To appear in ENTCS available at http www avispa project org 5 Alessandro Armando and Luca Compagna Satmc a sat based model checker for security protocols In Proceedings of the 9th European Conference on Logics in Artificial Intelligence JELIA 2004 LNAI 3229 Lisbon Portugal September 2004 Springer Verlag 6 AVISPA Deliverable 3 2 Assumptions on Environment Available at http www avispa project org 2004 7 AVISS Deliverable 1 3 Final project report For more information on the AVISS project see http www avispa project org theproject html 2002
81. p 0 An exception is raised if a path to a non existing node is specified 3 2 3 Using SATMC The SAT based Model Checker SATMC 5 builds a propositional formula encoding a bounded unrolling of the transition relation specified by the IF the initial state and the set of states representing a violation of the security properties The SAT compilation of IF specifications results from the combination of a reduction of security problems to planning problems and SAT encoding techniques developed for planning The propositional formula is then fed to a state of the art SAT solver and any model found is translated back into an attack In implementing SATMC we have given a great deal of care on design issues related to flexibility modularity and efficiency The result of such an effort is an open and flexible platform for SAT based bounded model checking of security protocols For instance improvements of SAT technology can be readily exploited by integrating in a plug and play manner state of the art SAT solvers e g the best performers in the SAT competition 16 Similarly advancements and novelties in AI planning SAT reduction techniques can be promptly implemented in SATMC SATMC can be employed not only for discovering attacks on protocols but also for verifi cation i e proving that the protocol satisfies its security requirements of a bounded number of sessions a problem that has been proved see 15 to belong to the same compl
82. ped by Th Genet IRISA Rennes France and available at http www irisa fr lande genet timbuk to perform the computation of the intruder knowledge over or under approxi mated An over approximation may lead to positive proofs of secrecy properties on the studied pro tocol for an unbounded number of sessions but TA4SP requires a special initial state and abstrac AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 61 tions presented in Paragraph 3 2 4 Otherwise in the over approximation context TA4SP can only conclude that secrecy properties are safe for the given initial state In an under approximation context without any optional abstractions the tool may show that the protocol is flawed for a given secrecy property To verify a protocol with TA4SP the empirical strategy to apply is the following 1 The user computes an over approximation and check secrecy properties 2 If the first step does not allow to ensure secrecy then the user successively computes under approximations until obtaining an attack in a reasonable time However this empirical strategy does not always lead to the expected result Indeed an inconclusive result using an over approximation does not imply that there exists a real attack Up to now TA4SP does not handle sets and conditions and verifies only secrecy properties with a typed model The following paragraph describes the TA4SP options which are very useful to specify precisely the
83. preted protocol specification Role server played by s 7 First instance of the role server start gt s ks n26 Ns First step receives start and send a nonce n26 Ns Choice Point Second step chose one branch or the other Csus 27 i ki _Cinv kca gt n27 SeID Third step assumes 2 kt inv kea Was received Other steps Or Csus 31 fs ks _ inv kca gt n31 SeID n31 Ns Third step other choice assumes 5 ks inv kca Was received Other steps IF Facts Each protocol step contains all the facts found for this step in the IF file except the state While their syntax might look a bit different than original IF facts due to CL AtSe s internal fact representation their semantic is identical Major differences are e contains term set facts are changed into Test term in set Test term not in set Add term to set and Remove term from set depending on the position of the contains fact in the rule and following the semantic of contains facts Tests are preconditions for the protocol step containing them e secret term mark set becomes Secret term set AVISPA Tool v1 1 User Manual 3 2 Analysing a IF Specification 58 3 2 2 Using OFMC The On the Fly Model Checker OFMC builds the infinite tree defined by the protocol analysis problem in a demand driven way i e on the fly hence the name of the back end It uses a number of symbol
84. r provides the hlpsldoc tools for documenting HLPSL specifica tions in 4 TfXand HTML format To set them up follow the instructions below cd AVISPA_PACKAGE contrib hlpsldoc tar xzf hlpsldoc tgz Then follow the instructions in the local INSTALL file Usage of the hlpsldoc tools is explained in the local README file The current distribution has been tested on several Linux platforms please refer to the global README file but if you encounter any difficulty in installing and running AVISPA on your machine please send us a message to avispa users avispa project org 1 2 How to use the AVISPA tool The typical interaction with the AVISPA tool is as follows 1 You start by specifying the protocol in HLPSL the AVISPA specification language includ ing the properties that you want to check then 2 you invoke AVISPA by issuing the avispa command at the prompt and by specifying which analyser back end you want to use AVISPA Tool v1 1 User Manual 1 3 About this Manual 8 3 you look at the output and maybe shout Yeahhhhh if you will see that the AVISPA tool has declared that your protocol is safe maybe under some conditions or Ups when you will see that an attack has been found In the latter event you may decide to modify your protocol specification and interaction continues at step 2 Note that you can use the HLPSL XEmacs mode provided in the AVISPA package its syntax highlighting and menus are very pr
85. r_expression Non_stutter_expression Non_stutter_expression Non_stutter_expression Stutter_expression lt Non_stutter_expression Non_stutter_expression lt Non_stutter_expression Inclusion test in Elt Set in Non_stutter_expression Non_stutter_expression in Stutter_expression Non_stutter_expression Syntactic sugar for inequality Non_stutter_expression Stutter_expression Stutter_expression Non_stutter_expression Non_stutter_expression Non_stutter_expression Non_stutter_formula Non_stutter_expression lt Stutter_expression Stutter_expressions_list Stutter_expression Stutter_expression Non_stutter_expressions_list Non_stutter_expression Non_stutter_expression Expressions_list Stutter_expression Non_stutter_expressions_list u Stutter and non stutter expressions Expressions are composed with variables and constants combined by concatenation or encryption or used with functions or sets Stutter_expression Stutter_expression Variable_or_constant_or_nat Inverse of a public private key inv Stutter_expression AVISPA Tool v1 1 User Manual 2 USER SECTION 23 Concatenation right associative Stutter_expression Stutter_expression Function application Variable_or_constant Stutter_expressions_list h Set yn wgn Stutter_expressions_list Encryption
86. rations k Sessions generation Each HLPSL specification should have a special role called session for example which represents a single session of the protocol This role is parametrised by all variables necessary for one session BTW channels can be declared as local variables inside a session role instead of being in the parameters list For instance in NSPK a session might look like this AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 30 role session A B agent Ka Kb public_key def composition alice A B Ka Kb bob A B Ka Kb end role 2 1 3 Example As illustration of HLPSL we describe in this section the specification of the well known Needham Schr der Public Key NSPK protocol This example is usually considered as very simple and far away from real protocols But here we will consider a more complex variant of the NSPK protocol the NSPK Key Server NSPK KS This protocol is given as follows using an Alice amp Bob based notation if A does not know Kp A gt 5 A B S gt A B Kio AS gt B ANA Alx if B does not know K a B gt S B A S gt oB A Ka gz BoA Na Neh AB AN glx The main difference to NSPK is that agents A and B needing to know the public key of each other for running the protocol may ask the server S to supply the key if they do not already know it This means that some steps of the protocol are conditional The specification is therefore decomposed into
87. ression Bracketed_expression Bracketed_stutter_expression Bracketed_non_stutter_expression Variable_or_constant var_ident const_ident Variable_or_constant_or_nat var_ident const_ident nat_ident v Predefined equational theories In HLPSL specifications several specific operators have prede fined equational properties e concatenation this operator is associative A B C A B C e exclusive or this operator xor A B is associative commutative and nilpotent xor xor A B C xor A xor B C xor A B xor B A xor xor A A B B e exponential this operator exp E N representing EY can commute exponents and admits an inverse for exponents exp exp E M N E exp exp E N M exp exp E N inv N AVISPA Tool v1 1 User Manual 2 USER SECTION 25 Those operators can be used in any expression concatenation is explicitly recognised in the grammar xor and exp are part of the function applications in expressions 2 1 2 HLPSL Guidelines This section will guide you for writing in a good way a HLPSL specification a Variable constant names Do not use the same variable constant name in different roles with different types b Arithmetic Do not use arithmetic operators relations e g lt They are not supported by the trans lator c Old new values of variables A primed variable eg X represents the new value of
88. role name a constant and its parameters a list of declarations of variables with their type Role_header const_ident Formal_arguments Formal_arguments Variable_declaration Variable_declaration A role may contain numerous declarations e local declarations declarations of variables with their type e constants declarations declaring constants with their type is not local to the role any constant in one role can be used in another one e initialisations initialisation of local variables e accept declarations conditions for which the role can be considered as done e intruder knowledge declaration a set of information that is given to the intruder at the beginning of the role execution Role_declarations tdef Local_declaration Owns_declaration not handled yet Const_declaration Init_declaration Accept_declaration not handled yet IKnowledge_declaration f Declaration of local variables Declarations of variables are grouped by type separated by a comma Declaration of local variables Local_declaration local Variables_declaration_list Variables_declaration_list Variable_declaration Variable_declaration Note that even if variables are local to roles the same variable declared in different roles has to have the same type for avoiding automatic renaming that could bother the understanding of the result by the user AVISPA Tool v1 1 User Manual
89. rong authentication of agents on some information e the weak authentication of agents on some information Each goal is identified by a constant referring to predefined predicates secret witness request and wrequest added in transitions by the user For more details on those predicates see the description of actions page 15 Goal_declaration goal Goal_formula end goal Goal_formula secrecy_of Constants_list authentication_on Constants_list veak_authentication_on Constants_list LTL_unary_formula LTL_unary_formula LTL_unary_predicate lt gt LTL_unary_formula LTL_unary_formula LTL_unary_formula 2 LTL_unary_formula LTL_formula LTL_formula LTL_predicate lt gt LTL_unary_formula LTL_unary_formula LTL_unary_formula 2LTL formulas are handled by the translator but in the current version of the AVISPA tool no backend does use them AVISPA Tool v1 1 User Manual 2 USER SECTION 19 LTL_formula LTL_formula LTL_formula LTL_formula LTL_formula gt LTL formula 7 LTL_unary_formula LTL_formula LTL_unary_predicate const_ident Stutter_expressions_list in Stutter_expression Variable_or_constant not LTL predicate LTL_predicate LTL_unary_predicate Stutter_expression Stutter_expression Stutter_expression lt Stutter_expres
90. s gt Reactions immediate reaction Label const_ident nat_ident Note that each transition starts with a label a constant or a natural number followed by a dot The condition for applying a spontaneous action is a conjunction of predicates representing a state of the role all the information in those predicates is already known Predicates Predicate Predicate AVISPA Tool v1 1 User Manual 2 USER SECTION 15 Predicate Stutter_formula not Predicate const_ident Stutter_expressions_list var_ident Stutter_expression A predicate of the last form has to correspond to the reception of a message in a channel for example Rev M _K Contrarily to spontaneous actions immediate reactions happen when the player of the role is in a given state and has to react to some events a reception of a message for example that will change the value of some variables Events Predicate Event Event Predicate Event Event Non_stutter_formula not Event const_ident Non_stutter_expressions_list var_ident Non_stutter_expression var_ident start start message for Dolev Yao models The start message is used as a signal sent to the player of the role for asking him to start a session of the protocol In the last two cases the variable has to be a channel m Actions and reactions Actions and reactions
91. secrecy attack has been found on this protocol SUMMARY UNSAFE DETAILS ATTACK_FOUND TYPED_MODEL BOUNDED_SEARCH_DEPTH PROTOCOL NSPK KS if GOAL Secrecy attack on n23Nb BACKEND CL AtSe STATISTICS Analysed 2660 states Reachable 1567 states AVISPA Tool v1 1 User Manual 2 2 Analyzing a HLPSL Specification 38 Translation 0 10 seconds Computation 4 50 seconds ATTACK TRACE i gt a 6 start a 6 gt i a i i gt s 2 X1A i s 2 gt i i ki _ inv ks i gt s 2 X2A a s 2 gt i a ka _ inv ks i gt a 6 i ki _ inv ks a 6 gt i n33Na a _ ki i gt b 5 n33Na a _ kb b 5 gt i b a i gt b 5 a ka _ inv ks b 5 gt i n33Na n23Nb _ ka i gt a 6 n33Na n23Nb _ ka a 6 gt i n23Nb _ ki 2 2 o 2 eS Fe Fe eS TestNotInSet i X32Kb _ set_93 TestInSet i ki _ set_91 TestInSet a ka _ set_91 Secret n33Na set_124 AddToSet i ki _ set_93 AddToSet a _ set_124 AddToSet i _ set_124 TestNotInSet a X22Ka _ set_94 Secret n23Nb set_117 Witness b a nb n23Nb AddToSet a ka _ set_94 AddToSet a _ set_117 AddToSet b _ set_117 The description of the attack is not very difficult to understand but a detailed study of the output of the AVISPA tool is given in Section 3 3 AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 39 3 Advanced User Section AVISPA users
92. set Used rote of those fresh values that have already been generated by itself In doing this Role also guarantees the freshness of these values for what concerns its execution The intruder makes the same for itself too and therefore we can guarantee the freshness of the whole system simply by enforcing the following Nonce Prop O Used TR MIUsed 0 where TR is the name of the role at the topmost level of the HLPSL hierarchy A 2 5 Goals In HLPSL goals are specified as temporal formulae built on top of goal facts that are explicitly asserted by basic roles in executing their transitions To assert a goal fact corresponds to assigning the truth value to a HLPSL boolean variable representing the goal fact Let I be the collection of such boolean variables TR be name of the role at the topmost level of the HLPSL hierarchy and 7 2 7 gt the transition system represented by the following TLA formula A TLA TR A A y in T A y FALSE 20 A O y TRUE amp Mod y TR where 20 states that a goal fact i is initially false and ii holds only in those states reached by those transitions that assert it 13Let for instance RCV X gt act and RCV Z gt actz be two transitions defined within the same role In that case if the intruder sends a message on channel RCV both RCV X and RCV Z become enabled and both transitions fire at the same time To avoid such parallelism one needs to rewrite the tran
93. sion Stutter_expression Stutter_expression In the temporal formula lt gt means sometimes in the past means one time instant in the past means globally in the past The other symbols are standard logical connectives conjunction disjunction implication gt and negation 7 Note that LTL formulas always start by the always temporal operator An example of goal section is the following goal authentication_on nb weak_authentication_on na secrecy_of na nb lt gt has_seen A B M gt has_seen B A M iknows M B i end goal Note that the last LTL formula is just an example without any serious meaning It is given only to show that user defined predicates such as has_seen can be used so as iknows for representing intruder s knowledge q Declaration of types of variables All variables must be declared with the most precise type if possible or at least with the generic type message Variable_declaration Variables_list Type_of AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 20 Variables_list var_ident var_ident Type_of Subtype_of gt Subtype_of Subtype_of Simple_type l won Subtype_of yu Compound_type Note that a variable can be of type function using gt for separating the types of the arguments and the type of the result More generall
94. sitions as TRIG1O ARCV X gt act and TRIG2 ARCV Z gt acta 14 Alternatively we could enforce that all the set of used fresh values are disjoint AVISPA Tool v1 1 User Manual A 2 Formal Semantics 82 Besides this let m be a behaviour in 7 and a generic safety temporal formula then holds in 7 at time 7 denoted with r i E is inductively defined as in Figure 8 15 A safety temporal m p iff p holds in z t r i 761 iff r i 4 Q r i 01 V bo iff T i Q or 1 i da r i 2 iff T i 1 and T i Q2 m i O iff i gt 0and r i 1 Ed 7 1 0901 iff exists 0 lt j lt i s t m j For Figure 8 The semantics of safety temporal formulae formula is valid on a behaviour 7 in 7 denoted with 7 iff 7 0 A safety temporal formula is universally valid in 7 written 7 Do iff m for every behaviour 7 in T Let G be the HLPSL safety formula the security protocol is required to satisfy then we say that the security protocol specified in HLPSL achieves its security properties expressed in HLPSL too if T H No ing VG 15In Figure 8 and are safety temporal formulae and p is a goal fact 16Let be a safety temporal formula then V is its universal closure AVISPA Tool v1 1 User Manual B IF SEMANTICS 83 B IF Semantics In this section we formally describe the semantics of the IF Recall th
95. some macros Note that in contrast with e g C or other languages these macros are not HLPSL citizens They are interpreted xemacs mode but the underlying tools know nothing about them a How to define a macro The syntax is macro name arg list gt expansion For instance one can define the macro storedpwd macro storedpwd salt user pass gt sha salt sha user pass Note here that the user has the responsability of ensuring that the symbol sha is defined by the AVISPA Tool v1 1 User Manual 4 CONTRIBUTIONS 73 b Expansion Once a macro with n arguments is defined it can be used in the sequence of the HLPSL file One might e g employ in a message the sequence storedpwd Salt Client Pwd Before compiling a specification containing macros one must first expand those using either M x avispa apply macros or the shorter C c C m If this feature proves proves successful enough it is also planned to define a Zinclude token 4 2 Library of Protocols The AVISPA library of protocols is available online at http www avispa project org library It describes all the protocols that have been studied Notethat this description has been generated by the hlps12html1 script The avispa library tgz contribution permits to get all the HLPSL specifications at once You can uncompress it in the testsuite hlps1 directory or anywhere else 4 3 HLPSL documentation This contribution provides two scripts for autom
96. t Initp transition composition Ib ev 1 gt act Ri A A Rm sa end role lba evn gt act end role a Definition of a basic role b Definition of a composed role Figure 3 HLPSL roles generic structure possible name clashes with the environment To aid readability we still denote with A B A P the sets of local renamed variables Since immediate reactions can also be used to express spontaneous actions we focus here only on the formers We will proceed inductively translating to TLA starting with basic roles B and then giving the translation of the composed role P in terms of the translation of its components R Ro Rm In order to describe the TLA translation of a basic role let us first define tr to be the j th transition rule of the basic role i e tr ev 1 gt act T tr B to be the set of variables that are freshly generated by the transition tr in B i e Y tr B v v in Y B v occurs in tr and Used g ir with j 1 n be TLA variables each one devised to model a set that keeps track of those fresh values that have already been generated in executing the transition tr with j 1 n of B Moreover let Usedg be the TLA variable representing the set that keeps track of those fresh values that have already been generated by the role B The TLA translation of a basic role is then given by Figure 4 Notice that also a channel Ch can be owned by a role In such a case Mod Ch B is intende
97. t of roles one for each state fact in the initial state This instantiation actually runs the participant role generate new variable names and extract a minimal set of constraints representing this role For example a variable GX in role Server might become GX 1 and GX 2 in two role instances of this Server Also any nonce say Na generated in the specification is replaced by a different constant in each role instance say n1 Na and n2 Na For readability the set of constraints representing each role instance is displayed in the following Send Receive syntax Step Received Msg gt Sent Msg sigma amp Inequalities amp IF Facts where sigma is a unification constraint i e a set of equalities For conciseness the amp symbol is only written for new lines Any non determinism in the role execution is represented by a choice point on a set of roles When a choice point is executed the system in fact the intruder chooses what branch will be run Finally a role consists in a tree where unary nodes are protocol steps and n ary nodes are choice points An execution of a role is a path in this tree An output example follows AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 57 Intruder state Intruder Knowledge start i i ki _ inv kca inv ki ki kca List of initial intruder knowledges Unforgeable terms inv ks inv kca Computed list of term that the intruder cannot forge Inter
98. te transition function 17Note that 2 denotes the power set of a set S AVISPA Tool v1 1 User Manual 86 Rule gt State oot 1 exVar r s 5 do p o0 matches ls 25 p fresh s exVar 26 s s PF Do U rpo 27 Figure 10 Semantics of a IF rewrite rule operating only on ground terms i e s cannot contain variables otherwise the definition of the transition relation may not behave as one would expect the resulting s is then also ground as the rules cannot introduce any new variables Attack States and Properties The ground initial state s and a transition relation together define an infinite state transition system There are two ways to formulate the goals of the protocol in IF The first is to specify attack states which are syntactically built like the LHS of a rule We define that a protocol is secure for an attack state g iff there is no reachable state s such that matches g s holds The second way which is newly added to the IF format and not yet supported by the back ends is to specify temporal formulae Due to the syntax all permissible formulae are safety properties and can thus be checked on finite traces of events To define the semantics we therefore label all transitions of the transition system with the set of goal relevant events e g secret that occurred in that transition The protocol is secure for the formula iff every finite word w that the transiti
99. ted with P in HLPSL where Ypg and Yp are the sets of parameters pl Wz is the agent playing B Ri Ra Rm are the component roles for brevity sequential composition the loop construct and the acceptance conditions are not discussed Ag and Ap are the sets of local variables and Qg and Qp are the sets of owned variables Moreover even if it is not depicted explicitly by Figure 3 let Tg Tp be the sets of fresh variables which are updated by the role In the rest of this section given a role named R we denote with R its entire HLPSL definition which includes the roles signature the name R and the parameters that we denote with W R the player for basic roles the local and owned variables that we denote with A R and 2 R respectively nit a that we denote with Init R and the set of transitions or the compositions defined therein Same goes for the set of fresh variables denoted with Y R Moreover if R is a basic role in R the set Y R of its parameters is augmented with a new variable U that will later be instantiated with a unique number For instance in a parallel composition this allows to distinguish between two or more identical instances of the same basic role As a first preprocessing step we uniformly rename the roles local variables in order to avoid AVISPA Tool v1 1 User Manual A HLPSL SEMANTICS TT role B VWg played_by pl def role P Wp def local Ap local Ap owns Qp owns Qp init Init ini
100. tuttering steps A basic event is a conjunction of transition predicates at least one of which is of the form p V 4 p V where V is a tuple of variables and p V is a state predicate This definition ensures that events are non stuttering i e at least one state variable changes 4For simplicity we consider a single domain for all the variables However what follows can be easily extended to multi domain 5Notice that the satisfaction of this property causes the transition relation to be total SNotice that p V 4 p V V V can be simply derived from V V gt p V p V by means of contraposition AVISPA Tool v1 1 User Manual A HLPSL SEMANTICS 75 A 1 3 Transitions The next state relation of basic roles is defined through a set of transi tions rules within the transition section HLPSL distinguishes between two different types of transitions respectively called spontaneous actions denoted by the gt arrow and immediate reactions specified using the gt arrow Both kinds of transitions are preceded by a label which may be an alphanumeric string starting with a lower case letter and ending with a period It is worth pointing out that these labels carry no information about the order in which the transitions fire They are merely names Spontaneous actions relate a state predicate on the left hand side LHS with an action on the right hand side RHS Intuitively a spontaneous action tr
101. ular choice points are identified by keywords and step indent both a short and detailed attack are given and the simplified protocol specification analyzed by CL AtSe is provided on demand Usage CL AtSe can be invoked by typing on the command line cl atse lt filename gt nb n v ns noexec notype help short light out help in any order where each option is described as follows e help Print the full list of options e nb n Maximum number of loop iteration in any trace Only used when the protocol specification contains loops The default is 3 e v Verbose mode In this mode CL AtSe displays the analyzed maybe simplified protocol specification and more details in the attack trace Otherwise CL AtSe only displays a compact attack trace with the summary e ns No simplification Not recommended With this option the simplification step is skipped e noopt No optimisation Not recommended With this option the optimisation step is skipped e noexec Do not analyse the protocol Usually only used to see the protocol specification v without spending time in the analysis AVISPA Tool v1 1 User Manual 3 2 Analysing a IF Specification 56 notype No type mode In this mode CL AtSe considers all variables to be of generic type or no type ie the typing constraints described in the IF file are not checked This option is very useful to discover type flaw attacks light Force the
102. umbers E PAW iff c dando E Y where and y are conditions ad iff not o where is a condition qaqa q AVISPA Tool v1 1 User Manual B IF SEMANTICS 85 For the LHS of a rule we define the functions PF 1 for the positive facts NF 1 for the negative facts PC I for the positive conditions i e without not and NC 1 for the negative conditions Figure 9 defines when a rule is applicable to a ground state by the function matches that takes as argument the LHS of the rule and yields a function that maps a state s to the set of substitutions o such that lo can be applied to s this set is empty if the rule is not applicable In there the predicate ground checks that a given substitution is ground the function dom returns the domain of a given substitution and the function v returns the variables occurring in a given term The intuition behind this definition is as follows we consider every ground matches Rule_LHS State 24 wbsitiuiton matches s a ground o 21 dom a v PF D UvV PC D PRES o H PO 22 Vo dom p u NF 1 U v NC 1 dom o 23 NF l opNs 9 op ENC D 24 Figure 9 Applicability of a IF rewrite rule substitution see 21 such that under the positive facts can be unified with a subset of the current state hence PF I o is necessarily ground and the positive conditions are satisfied see 22 Furthermore for all ground subst
103. ws for the specification of compound types Compound types allow the protocol designer to declare HLPSL variables of sorts restricted and specialised in a particular way and permit to provide a detailed description of the contents of a variable using concatenation sets encryption inverse of keys and result of the application of a hash function to an expression of the given type Compound_type Subtype_of Subtype_of Subtype_of set Subtype_of 3 _ Bracketed_subtype_of l iny won Subtype_of wyn hash Subtype_of nyu Bracketed_subtype_of Simple_type l iny won Subtype_of myn won Subtype_of mya t Stutter and non stutter formulas A stutter formula is a formula that does not use the new value of a variable such formulas can be comparisons set membership tests Stutter_formula Stutter_expression Stutter_expression Stutter_expression lt Stutter_expression Inclusion test in Elt Set AVISPA Tool v1 1 User Manual 2 1 Specifying Protocols HLPSL 22 in Stutter_expression Stutter_expression in Non_stutter_expression Stutter_expression Syntactic sugar for inequality Stutter_expression Stutter_expression Stutter_formula A non stutter formula uses the new value of at least one variable represented by priming the variable example Na Non_stutter_formula Non_stutter_expression Stutter_expression Stutte
104. y types are either simple or compound r Declaration of types of constants To declare constants is similar to declaring variables except that the type of a constant cannot be compound Constant_declaration Constants_list Simple_type_of Constants_list const_ident const_ident Simple_type_of Simple_subtype_of gt Simple_subtype_of Simple_subtype_of Simple_type Simple _typenof s Types and compound types The types proposed are the standard ones agent key text chan nel and also more advanced ones like hash functions and enumerations Types nat and bool do not have any predefined semantics The generic type compatible with all the others is message Variables representing channels have an additional attribute indicating the level of protection dy for no protection ota for forbidding divert actions of the intruder Simple_type agent 3In the current version of the AVISPA tool only Dolev Yao channels are supported AVISPA Tool v1 1 User Manual 2 USER SECTION 21 channel channel qu dy 5 channel ota public_key symmetric_key text used for nonces message generic type protocol_id kind of label l nat l bool hash_func hash function Constants_or_nat_list Y enumeration Constants_or_nat_list const_ident nat_ident const_ident nat_ident HLPSL also allo
105. y in IF The no hlps12if option can be useful when passing IF specifications directly to the AVISPA Tool e When using the sessco option OFMC will first perform a search with a passive intruder to check whether the honest agents can execute the protocol and then give the intruder the knowledge of some normal sessions between honest agents In the case certain steps cannot be executed by any honest agent OFMC reports that the protocol is not executable and stops If the executability check is successful then the normal search with an active intruder is started with the only difference that the intruder initially knows all the messages exchanged by the honest agents in the passive intruder phase e The untyped option forces OFMC to ignore all types specified in an IF file This is equivalent to specifying no types at all in IF or to give atom and variable the type message e Using the d option one can specify a depth bound for the search the default being un bounded depth In this case OFMC uses a depth first search while the standard search strategy is a combination of breadth first search and iterative deepening search AVISPA Tool v1 1 User Manual 3 ADVANCED USER SECTION 59 e Using the p option one can manually browse the search tree e g p is the root node p 0 is the first left most successor of the root node p 0 1 is the second successor next to left most successor of the node obtained by
106. y is disabled and the static mutexes are generated moreover if mutex is set to 2 and the encoding gp bca has been selected then also the dynamic mutexes are computed solver the selected state of the art SAT solver zChaff 19 mChaff 14 SIM 12 and SATO 20 are currently supported it ranges over the values chaff default value mchaff sim and sato e sc a Boolean parameter for enabling or disabling the step compression optimization by default it is set to true e ct a Boolean parameter for enabling or disabling the compound typing assumption pre sented in Deliverable 3 2 6 see also section 2 1 1 by default it is set to true The value of this parameter is overridden by the AVISPA option typed_model when SATMC is run as a backend of the AVISPA Tool e oi a Boolean parameter for enabling or disabling the optimized intruder model presented in 4 by default it is set to false Enabling such an option can be useful to experiment the effectiveness of the optimized intruder model Notice that expert users can change the default values associated to the above options by acting on the bin backends satmc config configuration file 3 2 4 Using TA4SP Given an initial state the TA4SP tool computes either an over approximation or an under approximation of the intruder knowledge by means of rewriting on tree languages in a context of unbounded number of sessions The TA4SP tool uses the tree automata library Timbuk 2 0 develo

AVISPA v1.1 User Manual

Contents

Download Pdf Manuals

Related Search

Related Contents