Home

ASLan++ specification and tutorial

1. 10 2 1 3 Formalizing Behavior 43 0 e a oe ee Ge ne Be we 11 2 1 4 Specifying Security Goals 0 2 020000024 13 2 1 5 Modeling the Overall Problem 16 2 1 6 Validating the Model 0 o 22 2 1 7 Clauses Deductions and Recursion 22 Modelmge Hints 4 4 4 6446244 be 2 e Ew A eR Ee oe ee OE e 36 2 2 1 Debugging wrt executability problems 36 2 2 2 Detecting uninitialized variables o 38 2 2 3 Improving efficiency 64 a2 455 be eee e eee ee 40 2 3 Set operations iaa AA e GE 41 2 3 1 Basic Commands os 0 252 a OES 42 2 3 2 ForAll and Copy sc o a RR A a a 42 2 3 3 Union and Intersection 4 2s 64 ese oe eae ee eae nes 44 2 3 4 IsSubset and IsEqual rs a2 e med Ee EA ERS 45 2 3 0 EXErCISES gt Aea amp or ed Be a Se FWP Ke eae we A ee ee G 47 24 Ord Data e o a ro A E A Ra te E 47 2 4 1 Global variables 64 4444644424648 444423 404 45 48 2 4 2 Implementation via facts ooo a sua e os 49 2 4 3 Shared databases caca A 51 2 5 Set communication 2 ba pisada ae heen we 55 2 5 1 Shared set variables and synchronization 55 2 9 2 Referentes e s re 6 a ade ed A ee y eR ER A 58 2 5 3 Concatenated elements a a 60 220 TIME 44 5 ona ER E ERRADA ee Ea a a 62 A F 24 eR AS SEAS EH ERE EERE EG SSS GORE 64 2 8 Communication in different channel models
2. 101 3 Properties channel facts and their informal meaning 102 4 Linked channel fact and its informal meaning 104 5 Properties channel facts and their informal meaning 104 6 LTL operators for specifying goals 0 o 106 7 Channel goal symbols in ASLan 0 0000000004 107 8 Translation from ASLan to the CCM 137 9 Translation from ASLan to the ICM 138 10 Translation from ASLan to the ACM 00 138 11 Substitutions done by the adaptGuard function 151 12 Trapslati n OL gols 4a dn tora 6 he ee ee ee ee oS ew we ek k 153 13 Events used in the translation of channel goals and rules used for deriving the protocol ID from the name of channel goals 155 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 7 190 1 Introduction This document introduces and describes ASLan the AVANTSSAR specification lan guage ASLan is a formal language for specifying security sensitive service oriented ar chitectures their associated security policies and their trust and security properties The semantics of ASLan is formally defined by translation to ASLan the low level specifica tion language that is the input language for the back ends of the AVANTSSAR Platform This is an update of Deliverable D2
3. D2 3 update ASLan specification and tutorial 143 190 4 7 9 Branch Branch stmt rest sl return_sl stmt p_1 p_n n_1 n m if Guard then LeftStmt else RightStmt positiveGuards Guard negativeGuards Guard apply adaptGuard to p_1 p_n and n 1 n_m positive branches i e for i from 1 ton 4 LHS state fact for this state facts for the p_i RHS state fact for this branch sl 0 state facts for the p_i add Guard satisfied entity with step label sl owners of variables appearing in entity with step label owners of variables appearing in LHS p_i gt RHS renewPositiveFactsIn p_i to section rules in the negative branches i e for i from 1 tom 4 LHS state fact for this state facts for the n_i RHS state fact for this branch sl 1 state facts for the n_i add translation Guard not satisfied entity with step label sl owners of variables appearing in entity with step label owners of variables appearing in LHS n_i gt RHS renewPositiveFactsIn n_i to section rules in the translation ParseCode LeftStmt branch sl 0 succ sl ParseCode RightStmt branch sl 1 succ sl ParseCode rest succ sl return_sl FP7 ICT 2007 1 Project No 216471 a SEVENTH FRAMEWORK PROGRAMME A ANTSSAR D2 3 update ASLan specification and tutorial 144 190 Conceptually an if statement corresponds to two rewri
4. any A B Session A B where A B B where A B any A B Session A q Figure 5 Nested Entities Environment its Sessions and their Actors session instantiates one actor Alice and one actor Bob based on the parameters handed to it by the environment Each entity first declares its symbols and other items it requires This declaration is followed by the entity s body which specifies the entity s behavior The body is executed when the entity is instantiated An entity may also specify security goals entity Alice Actor B agent symbols Na Nb text body In our example Alice is defined as an Actor by the keyword Actor in the entity s parame ter list As additional parameter she gets told which agent B is her communication partner She declares that for NSPK she will need two variables indicated by the keyword symbols Na and Nb of type text In the body part Alice s behavior is specified Note that within The ASLan standard prelude defines some fundamental types like fact anything that can be intro FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 18 190 A B A B 4 5 x4 4 1 1 i B i B Figure 6 Two parallel sessions Multiple Interference Facilities that body whenever Alice herself is referenced this is done by using the keyword Actor ASLan Session Instantiation In the body of
5. Vars Formula AttackStates attack_state ConstId Vars PNFacts Conditions Formula Fact equal Term Term not Formula and Formula Formula or Formula Formula implies Formula Formula forall Vars Formula exists Vars Formula LTLOpi Formula LTLOp2 Formula Formula neXt Yesterday Finally Once Globally Historically LTLOp1 a OL yn p o qu H Until Release Since LTLOp2 y R gn Equation Term Term The number and types of Terms must match the declared arity of Opld Term Const VarId OpId Terms In TypeDecl of the form VarId Type Type cannot be fact TypeDecl VarConsts Type Type Typeld Opid Types Conste SuperType Typeld gt Typeld OpDecl Opld TypeStar gt Type TypeStar Type Type TypeStar Var Varld Vars Var Var x VarConsts Var Const Var Const Terms Term Term Types Type Type Opld Constld FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 171 190 Typeld Constld Varld A Z_ a zA Z0 9_ ConstId a z a zA Z0 9_ Numeral 0 1 9 0 9 Const Numeral ConstId Consts Const Const x A 2 2 St
6. new Thread Actor C SessID Sessions The Thread s Actor is the same as for the Server FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 83 190 body all sessions are with the same server iknows 0 workaround should not be needed ServerSessions new Server server ServerSessions any C Session C server where C server any C Session C server where C server To demonstrate the guarantees we obtain by the construction just explained this model uses the goal Server_TLS Client for the channel between the server and the client and Client_TLS_ Server for the opposite direction Moreover there is a new secrecy goal secret _SessID indicating that the session ID is a secret shared between the client and the server Due to limitations of the translation of the current ASLan channel and secrecy goal syntax we had to resort to an earlier form of stating such goals that is more cumbersome but on the other hand more flexible to cope with the nested Thread entity and the global server instance The channel goals for each direction involve integrity authenticity replay protection and confidentiality of the session ID sequence number and payload Note that in comparison to the model mentioned in 2 9 3 there is now additionally authentication of the client to the server and freshness of messages in the same directi
7. gt state_Alice Actor IID 4 B Req Resp iknows Resp some_fact Req Resp FP7 ICT 2007 1 Project No 216471 a SEVENTH FRAMEWORK PROGRAMME A ANTSSAR D2 3 update ASLan specification and tutorial 166 190 5 Conclusion We have presented ASLan the AVANTSSAR specification language The low level lan guage ASLan given in Appendix A is the input to the back ends of the AVANTSSAR Plat form ASLan has the look and feel of procedural and object oriented programming languages and thus can be employed by users who are not experts in formal specification languages The semantics of ASLan is defined by translation to ASLan Both ASLan and ASLan are supported by the AVANTSSAR Platform ASLan allows us to formally specify services and their policies in a way that is close to what can be achieved with specification languages for security protocols and web services The flexibility and expressiveness of ASLan and the underlying low level language ASLan is demonstrated via the formalized and validated problem cases reported in Deliverable D5 3 7 As discussed in the AVANTSSAR description of work Annex I the refined versions of ASLan and ASLan as presented in this document cover static and dynamic ser vice and policy composition aspects The specification languages and the entire AVANTS SAR Platform 6 support full fledged specification and analysis of the case studies and the industrial strength applicati
8. D2 3 update ASLan specification and tutorial 132 190 To this end we create a rule that adds to the current state the state fact for the new instance with a fresh instance ID to make it distinct from any other already in the system and step label s1_0 from which execution of its body can start Its parameters p_1 p_n are assigned the terms passed namely t_1 t_n while its internal variables v_1 v_m are assigned the value dummy_T standing for an uninitialized value of the respective type T Example 5 Imagine that during the parsing of the entity Env at step label sle the following instantiation for BidM is encountered new BidM bm bp The rule generated will be state Env 0ID sle exists IID gt state Env 0ID succ sle state BidM bm IID sl_0 bp dummy_message child OID IID that will create the fact for the BidM instance with step label s1_0 O Recall that as we remarked in 3 3 above we assume that the modeler is responsible to ensure for each entity that may also be played by a dishonest party that with the sufficient knowledge of secrets the intruder has enough information to perform every legal step of the entity so that the behavior of that entity is subsumed by what the intruder can do Therefore we can block as described in 4 10 any entity instances with a dishonest player i e where dishonest Actor This is safe because all transitions that the dishonest agent can pe
9. Decls EntityDecl Body ConstrDecls GoalDecls UpperLetter A Z LowerLetter a z NonZeroDigit 1 9 Digit 0 NonZeroDigit Numeral 0 NonZeroDigit Digit Alphanum UpperLetter LowerLetter Digit _ 7 UpperName UpperLetter Alphanum LowerName LowerLetter Alphanum Name LowerName UpperName FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 114 190 Var Vars Params Imports Decls TypeDecls TypeDecl Type Types SymbolDecls SymbolDecl MacroDecls MacroDecl ClauseDecls ClauseDecl Condition EquationDecls EquationDecl Term UpperName Var Vars n Type q E import UpperName TypeDecls SymbolDecls MacroDecls ClauseDecls EquationDecls types TypeDecl LowerName lt LowerName note the optional supertype LowerName simple type name Type set note the actual type parameter Type Type tuple Type Type tuple compound Type gt LowerName Types general compound Type Type concatenation compound Type 19 Type symbols SymbolDecl Vars Type nonpublic LowerName nonpublic noninvertible LowerName Types Type constants Type func
10. If you dislike translator warnings and want to avoid problems with the model checkers you can also use the following version of our example specification SetsGlobal2 channel_model CCM entity Environment symbols syncil sync2 message a b el e2 agent SetGlobal agent set entity Alice Actor B agent SetGlobalA agent set body B gt Actor syncl if SetGlobalA gt contains el1 SetGlobalA gt remove el Actor gt B sync2 entity Bob A Actor agent SetGlobalB agent set body SetGlobalB fei e2 May NOT be used here SetGlobalB gt add e1 Only possible assignment method SetGlobalB gt add e2 Only possible assignment method Actor gt A syncl A gt Actor sync2 assert no_alarm SetGlobalB gt contains el1 F body SetGlobal Initialize global set new Alice a b SetGlobal new Bob a b SetGlobal FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 58 190 Here we use the same method as we already have used for the shared database in 2 4 3 In fact it is an equivalent example What are the differences here compared to the previous example In the shared DB style example we pass the reference to the global set as parameter to both Alice and Bob They may both use this reference to query add and remove elements to and from the global set Please be aware of what her
11. These goals are sketched in the annotated message sequence chart in Figure 4 The corresponding input to Web Sequence Diagrams is note left of A Na fresh goal secret_Na Na A B Kb assumed known end note FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 16 190 A gt B Na A _Kb note right of B Nb fresh goal secret_Nb Nb A B Ka assumed known end note B gt A Na Nb _Ka note left of A Check if Na is the same goal A_auth_B Na B gt gt A end note A gt B Nb _Kb note right of B Check if Nb is the same goal B_auth_A Nb A gt gt B end note 2 1 5 Modeling the Overall Problem ASLan Entities So far everything we have discussed in this example is more or less independent of ASLan We have clarified and to a certain degree formalized our problem Now we make the transition to modeling the problem in ASLan An ASLan specification of a system and its security goals has a name which should be consistent with the name of its file and contains the declaration of a hierarchy of entities as sketched in Figure 5 The major ASLan building blocks are entities similar to classes in Java or roles in the context of security and communication protocols Entities declare various symbols macros goals and other items required by the entity and describe the entity behavior Entities may have parameters and contai
12. 4 7 we presented a procedure for translating ASLan statements into ASLan transi tions but we did not apply any translation of terms There are two reasons behind this e Split the translation into a higher level of statements and a lower one of terms contained in them allowing for cleaner exposition and ease of understanding e In most cases ASLan terms can be easily replaced by equivalent terms in ASLan by means of semantically equivalent predicates However there are a few exceptions e g set literals and assignment of variables by pattern matching that can not be handled by simply replacing the term with another as they affect the entire resulting rule for the statement that contains the term The approach followed is therefore to defer translation of terms carrying over the original ones during translations of statements and guards included in them and then apply a term translation procedure to the generated rule which we describe in the following Consider a rule R of the form LHS exists E gt RHS and let us apply the procedure to R Suppose that R is now in an intermediate state where both ASLan and ASLan predicates namely transmission events may appear of which only the latter need be translated but all need be processed recursively for contained terms For each predicate in R we recursively traverse each sub term T according to its syntactic form obtaining the following cases e T c i e T
13. GoalDecl GoalDecl Name Formula ChanGoal SecrGoal ChanGoal Name _ Term ChannelProps Term SecrGoal Name _ 4 Term 3 Formula FuncApp 1 Formula LTLOpi Formula LTLOp2 Formula Formula Term Term Term Term Formula amp gt Formula foral1 exists Var Formula Formula neXt Yesterday Finally Once Globally Historically LTLOp1 yx nyu lt gt lt gt O Until Release Since LTLOp2 ses y R gu FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 117 190 3 13 ASLan prelude The syntax of ASLan gives the user some freedom in declaring new symbols such as functions and facts For instance one may declare an encryption function as crypt public_key message message Their meaning may be specified using Horn clauses and equations In fact it is an important feature of the semantics of ASLan that we need only a few built in symbols with a hard wired meaning but can express the meaning of most symbols in ASLan itself For instance we use the symbol iknows to specify that the intruder knows a particular value of type message or a subtype of it or also of any set type and to define the deductions of the intruder in the style of Dolev Yao by a set of
14. are tree levels of verbosity of an Avispa like output format which gives more and more information on the way the specification was understood by the tool if gives a condensed view of an attack found if any and brief gives an even more elementary view of the result Advanced Horn Clause Use For more advanced users Cl AtSe allows you some control on the strategy used for horn clauses Even if the strategy remains backward only you can control the kind of recursivity used to help the tool to analyze your specification more efficiently That is three variants of the horn clauses strategies are available 1 Backward with Top Down recursivity h c are used to produce the facts required by a transition an attack state or the RHS of an other h c in a Depth first mode That is first finish the deductions of the first fact in the list before doing deductions for the next one Facts are taken in the order they were written in the ASLan file Activated by option hc btd for BackwardTopDown 2 Backward with Top Down recursivity but with modified ordering default This is the same as above but the tool choose himself the ordering of facts to use i e the tool FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 186 190 choose which fact must be deduced first This will reorder the lists of facts so that the more interesting facts are tried first This is an heuristic
15. gt CP reflects nonce to same C only Nc Payloads goals client_link forall C C IID IID M 1 Cclient_sent C IID M amp the private key associated with the client s alleged name Thus the server can check that in subsequent transmissions the client side whoever this really is uses the same private key matching the client s name FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 74 190 client_rcevd C IID M gt C C amp IID IID Here the client_link goal given as an LTL formula expresses that the client receiving the response is the same client who sent the request The property actually achieved is even a bit stronger the response can not be received by any party except the client who crafted the request i e the pseudonymous security It is possible to use a similar pseudonymous secure channel on the goal side 18 but currently such goals are not supported by ASLan In this example we have just one request response pair If we model applications with several transmissions this kind of channel achieves another interesting property even though the client is not authenticated the server can be sure that all messages come from the same sender This also called sender invariance This is also captured by our model of pseudonymous secure channels because they behave exactly like normal secure channels except that authentication i
16. lt new value gt See the following example verbatim Modifiable shared variable implemented via facts specification SharedFact_Unsafe channel_model CCM entity Environment symbols succ nat nat entity Session A B agent symbols shared protocol_id nat fact SharedVarId protocol_id entity Alice Actor B agent SharedVarId protocol_id Alice and Bob does not inherit SharedVarld but get a copy of the reference to SharedVar as parameter symbols ValueOfSharedVar nat body read and remove the old value and set a new value select FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 51 190 on shared SharedVarId ValueOfSharedVar 4 retract shared SharedVarId ValueOfSharedVar shared SharedVarld succ ValueOfSharedVar Actor gt B i handover to B entity Bob A Actor agent SharedVarld protocol_id body A gt Actor i handover from A assert test_SharedVar_still_1 shared SharedVarld 1 reads the current value should report violation because now shared SharedVarild suwee 1 holds body SharedVarld fresh shared SharedVarId 1 sets the initial value new Alice A B SharedVarld new Bob A B SharedVarld body any A B Session A B where A B amp dishonest A This model uses all the mechanisms just described to achieve essentiall
17. FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 162 190 state_responder Actor IID 1 dummy_agent dummy_message iknows A exists N gt state_responder Actor IID 4 A N iknows N Whenever feasible the translator actually produces such compressed rules since it makes verification easier for the back end tools As mentioned above this is sometimes a complex procedure e g if the sequence of actions contains branches and there are cases when this is not possible e g the compression of an entire loop We have chosen not to complicate our semantics exposition with a complete description of the compression procedure but to regard it as an optimization step that must be semantics preserving as in the above example of the translation from ASLan to ASLan See also 4 15 2 4 15 Optimizations The translation procedure presented so far produces a set of transition rules that quickly increases in size even for small ASLan specifications In order to ease the work of the verifier tools in the following we introduce two optimization techniques for the translation The optimizations decrease the number of generated transition rules 4 15 1 Elimination of empty transitions and redundant guards Intuitive explanation The first level of optimization aims at eliminating empty transi tions and redundant guards An empty transition does not change the state except for the ste
18. Similarly to represent the abstract syntax A m gt B M for ACM channel assump tions in ASLan we use the concrete syntax A ch gt B M 38 Table 1 and Table 2 show the syntax notations that ASLan supports for CCM ICM and ACM respectively Channels may be specified in OO style notation as well as in the annotated channel notation For sends and receives if the first argument is Actor like in send Actor B M or Actor gt receive B M it may be omitted such that only send B M or receive B M respectively is written The sender and receiver terms in the channel notation must be of type agent or a subtype of it CCM and ICM In CCM and ICM we allow agents to be identified by pseudonyms rather than by their real names We denote this as A _ P where A denotes the real name and P is the pseudonym Authentication and confidentiality of a pseudonymous endpoint is only with respect to the pseudonym and not with respect to the real name When the real name is not used at all one may also write 7 _ P In order to make pseudonyms directly applicable for asymmetric encryption they have type public_key We regard public_key as a subtype of agent such that pseudonyms can be used in place of an agent real name By default every agent will create a fresh pseudonym upon instantiation we can write simply Actor to denote the current agent acting under this default pseudonym For instance to model transmissions over a TLS ch
19. Stmt Assign FreshGen EntityGen SymbEntityGen symbolic session Transmission IntroduceFact RetractFact Branch Loop Select Assert Stmt Assign Var Name Var Term FreshGen Var Name Var freshQ 3 EntityGen new Entity SymbEntityGen any Var Entity where Guard Transmission Term gt send receive Terms over Term where Actor gt is optional Term ChannelProps Term Term annotated channels for CCM and ICM Term Term gt Term Term annotated channels for ACM h set literals are not allowed in transmissions ChannelProps gt gt gt x Entity UpperName Terms IntroduceFact FuncApp only for iknows and facts not in any clause head RetractFact retract FuncApp only for iknows and facts not in any clause head Branch if GuardNoRcv Stmt else Stmt Loop while GuardNoRcv Stmt Select select on Guard Stmt Guard may include receive Assert assert GoalDecl ConstrDecls constraints ConstrDecl only allowed in the root entity ConstrDecl Name Formula FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 116 190 GoalDecls goals
20. but in the worst case still everything is tested If you want to control the ordering yourself please use the other option above This one can be activated with hc btd and it is the default Backward with Breadth first recursivity Assume you have a set of facts to test In this mode the tool with make one elementary deduction for each fact storing the subsequent new facts to produce and iterate only after all facts have been processed The advantage is that the ordering is not important anymore in this mode since you move layer by layer The bad consequence however is that if you are unlucky today one of your facts may explodes into a huge set of facts before the deductions on an other fact could add the right constraints However such conditions are quite particular and in that case the modeler should choose his fact ordering carefully with hc btd or thrust the tool with the default hc btd This option is activated with the option he blr for BackwardLeftRight To conclude about horn clauses please note also the existence of an option called not _hc Due to structural constraints inside the horn clauses functions in Cl AtSe sometimes false attacks might appear where negative tests inside horn clauses was validated while they should not This is due to the fact that testing such negative tests might require to perform an inversion of a formal state which is a very complex and costly operation Thus until n
21. e As a consequence for instance exclusive or denoted should be a function of type msg x msg msg and not a polymorphic one of type a x a gt a The reason is the type of the neutral element e it must be of type msg e Polymorphic types are disallowed for constants or variables and only allowed for func tions e g contains a set a fact This affects the definition of all where 7 is an instance of the return type f ti tn L for every t L tn La for all E Te OF Finally we allow for a special kind of typing that is merely a syntactical abbreviation compound types This concept has been first introduced in HLPSL IF 9 and allows one to specify the format of message terms as a type For instance we may declare M crypt public_key pair agent msg This constrains the set of values that can be substituted for M to those of the appropriate message format More generally the declaration X f t1 tn is just an abbreviation for X1 t1 Xn tn for new variables Xi and replacing all occurrences of X in its syntac tical scope with f X1 Xn This replacement must of course be repeated recursively if any of the ti is itself a compound type A 3 5 Micro and Macro Steps For the translation from ASLan to ASLan we consider a concept of micro steps and macro steps where the micro steps represent the intermediate states of an honest agent in a longer computation that we like to abs
22. gt send B M iknows M A gt receive B M iknows M A gt send B M over authCh athCh A B M A gt receive B M over authCh athCh B A M A gt send B M over confCh cnfCh B M A gt receive B M over confCh cnfCh A M A gt send B M over secCh secCh A B M A gt receive B M over secCh secCh B A M Table 9 Translation from ASLan to the ICM Like for CCM the subterms A B and M stand for the translation of A B and M respec tively including any pseudonyms Also the pseudonyms in the sending role are transmitted in an analogous way In the translation table the following auxiliary symbols are used iknows message gt fact message on insecure channel athCh agent agent message gt fact message on authentic channel cnfCh agent message gt fact message on confidential channel secCh agent agent message gt fact message on secure channel As specified in 2 4 1 4 Standard Channels as Assumptions and 20 18 where more details on these symbols may be found the following intruder rules are given at ASLan level for sending and receiving on ICM channels iknows B iknows M dishonest 4 athCh A B M athch A B M iknows M iknows B iknows M cnfCh B M cnfCh B M dishonest B iknows M iknows B iknows M dishonest A gt secCh A B M secCh A B M dishonest B iknows M ASLan p
23. purpose etc clauses Horn Clauses deduce new facts trusted_pk_direct C Direct trust C s pk trusted_pk C A If C is a trusted trusted_agent C certificate authority trusted_pk_cert_chain A B Indirect trust C s pk trusted_pk A If we trust B s pk trusted_pk B amp and know a certificate issued B gt cert A pk A where B accredits A B A hhh CL AtSe no self signed certs allowed hhh SATMC and OFMC can handle certificate chain loops entity Session A B agent entity Alice Actor B agent symbols Na Nb text an example of the latter method FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 35 190 body if trusted_pk B A talks to B if B s pk is trusted secret_Na Na fresh Actor gt B Na Actor _pk B B gt Actor Alice_authenticates_Bob Na secret_Nb Nb _pk Actor Actor gt B Bob_authenticates_Alice Nb _pk B entity Bob A Actor agent 4 symbols Na Nb text body gt Actor Na A _pk Actor Bob learns A here if trusted_pk A B talks to A if A s pk is trusted secret_Nb Nb fresh Actor gt A Alice_authenticates_Bob Na Nb _pk A A gt Actor Bob_authenticates_Alice Nb _pk Actor secret_Na Na Na Goal can only be given here because A certainly is not authenticated before b
24. without giving a variable name which is treated as a wildcard When a guard is evaluated variables are handled as follows e A variable name without is evaluated according to the current value of the variable e A not followed by a variable name matches any value e For a variable name with it is checked if there is a value that can be con sistently replaced for all occurrences of this variable name such that the condition holds To this end variables that occur at least once positively are treated as existentially quantified while variables that occur only negatively are treated as universally quantified Thus the above example guard is logically treated as exists A peer A B dishonest A whereas for example N M is treated as forall M N M FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 113 190 If the guard cannot be satisfied according to these rules no variable assignment occurs Otherwise each implicitly existentially quantified variable is assigned to a value such that the condition holds If there is more than one solution then each of them is a possible successor state Note that an ASLan specification may give rise to many different possible behaviors of the described system and the verification covers all of these behaviors To avoid interference with negation and implicit quantification there are furthe
25. 1 new Alice A B new Bob A B body any A B Session A B Here both Alice and Bob have access to the variable named SharedVar When Alice changes it Bob can observe this such that the given assertion assert test_SharedVar_still_1 SharedVar 1 does not hold anymore When translating this example with java jar aslanpp connector jar hc all gas SharedVariable1_Unsafe aslan 0o SharedVariable1_Unsafe aslan the ASLan connector warns WARNING at line 20 column 26 Variable SharedVar defined in the scope of Session is used in the scope of Alice This may cause problems to some of the backends WARNING at line 20 column 18 Variable SharedVar defined in the scope of Session is used in the scope of Alice This may cause problems to some of the backends WARNING Variable SharedVar defined in the scope of Session is used in the scope of Bob This may cause problems to some of the backends WARNING at line 31 column 39 Variable SharedVar defined in the scope of Session is used in the scope of Bob This may cause problems to some of the backends And indeed OFMC terminates abruptly stating ofmc core multiple waiting terms in lhs of a rule descendant x201 x202 i state_Alice x203 1 x204 x202 state _Session x205 x206 x207 x208 x209 x201 SATMC without the need for special options confirms the expected violation of the assertion CL AtSe also does this but needs to be called with
26. 14 3 Translation of compressed steps The compression of several rules would in many cases considerably complicate the exposition of this translation process and is in some cases impossible e g when an entire loop is compressed Therefore we describe the translation by using the fine grained transitions but with annotations specifying what should be compressed as follows These annotations are the special state facts of ASLan see A 3 5 like standard state facts they represent the local state of honest agents where the exclamation mark expresses an intermediate state of a compressed transition Recall that the semantics is to consider macro transitions that compress all the intermediate micro transitions where honest agents are in a local state denoted by a state fact In the translation from ASLan to ASLan the compression can now be straightfor wardly integrated into the normal translation process Consider a transition rule that is produced by the translation and that has the following form FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 161 190 state _X MSGs IID facts conditions gt state _X MSGs IID facts where IID is the identifier of the current entity instance To add the compression the translator would replace the left hand side or right hand side state fact or both with a state fact depending on the location of this transition with respect to th
27. 190 One method to sketch such behavior in message sequence charts are annotations as depicted in Figure 3 The input of Web Sequence Diagrams corresponding to Figure 3 is note left of A Na fresh Kb assumed known end note A gt B Na A _Kb note right of B Nb fresh Ka assumed known end note B gt A Na Nb _Ka note left of A Check if Na is the same end note A gt B Nb Kb note right of B Check if Nb is the same end note 2 1 4 Specifying Security Goals We want to model our protocol in such a manner that an automated model checker can look for attacks However the model checker needs to be told what are the desired protection requirements in order to be able to search systematically for ways an attacker may violate these requirements To this end we must explicitly specify security goals And we name our goals so the model checkers can refer to them when printing which goals they have found violated In our NSPK example primary security goals are that Alice authenticates Bob and vice versa agreeing on two secret nonces There are secondary security goals expressing that the values of both nonces are secrets shared between Alice and Bob only Thus we face two main types of security goals secrecy goals and authentication goals as representatives of a message communication security goal Typical communication security properties are authenticity integrity and confidentiality as well as replay p
28. 190 secret_Na Na fresh Actor gt B Na Actor _pk B B gt Actor Alice_authenticates_Bob Na secret_Nb Nb _pk Actor Actor gt B Bob_authenticates_Alice Nb _pk B entity Bob A Actor agent 4 symbols Na Nb text body gt Actor Na A _pk Actor Bob learns A here secret_Nb Nb fresh Actor gt A Alice_authenticates_Bob Na Nb _pk A A gt Actor Bob_authenticates_Alice Nb _pk Actor secret_Na Na Na Goal can only be given here because A certainly is not authenticated before body of Session new Alice A B new Bob A B goals Zsecret_Na _ A B Okay Asecret_Nb _ A B Attack found hhh Commented out the above goals such that hhh the attack is printed on authentiation Alice_authenticates_Bob _ B gt gt A Okay Bob_authenticates_Alice _ A gt gt B Attack found body of Environment Two sessions needed for Lowe s attack any A B Session A B where A B any A B Session A B where A B In this specification two sessions of the protocol are launched each involving one instance of Alice and Bob The Alice entity used to describe her behavior and security requirement FP7 ICT 2007 1 a SEVENTH FRAMEWORK PROGRAMME Project No 216471 A AN T SSAR D2 3 update ASLan specification and tutorial 90 190 as long as she is played by an honest agent has two parameters
29. 3 Generation of fresh values FreshGen stmt rest sl return_sl stmt Var fresh N is fresh variable name declare N of same type as Var in section types in the translation LHS state fact for this entity with step label sl state fact for owner of Var RHS state fact for this entity with step label succ sl state fact for owner of Var with Var set to N add LHS exists N gt RHS to section rules in the translation ParseCode rest succ sl return_sl Generation of a fresh value is straightforward transparently to the modeler a new variable N is created and a rewrite rule is added that substitutes Var in its owner s state fact with N instantiated by the exists of the rewrite rule and advances the step label Like for regular assignments since Var may belong to an ancestor of the entity we need to change its state fact rather than the current entity s for which we will update the step label nonetheless Yet in case Var belongs to the current entity the two state facts in the LHS are collapsed into one and there is only one state fact on the RHS that combines the changes to the step label with the assignment to the variable Example 4 Let s extend the above Bid Manager specification by adding in its body the following instruction to instantiate variable M of type message with a fresh value of agreeing type FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specificatio
30. 41 Currently the translator only supports channel goals where both the sending and the receiving entity are direct sub entities of the entity in which the goal is declared a SEVENTH FRAMEWORK PROGRAMME FP7 ICT 2007 1 Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 109 190 e g due to different variable names but their actual values evaluated when the send or receive statement is executed should of course be equal Note that it is allowed to declare channel goals that state e g authentic indirect trans mission for instance from Alice via Bob to Charlie entity Session A B C agent entity Alice Actor B C agent Actor gt B authentic_Alice_Charlie Payload entity Bob A Actor C agent entity Charlie A B Actor agent 4 B gt Actor authentic_Alice_Charlie Payload goals authentic_Alice_Charlie _ A gt C So far the translator accepts as agent terms in channel goals only constants or variables In case a more complex term is needed one may write e g body B peer A new Alice A B new Bob A B goals secure_Alice_Payload_Bob _ A gt B currently cannot write peer A instead of B here In case a more complex channel goal cannot be expressed given the above syntactic restrictions advanced users may directly use the formulation using witness and request facts as described in 4 12 2 3 9 4 Secrecy g
31. 66 25 ECM 4 24 484 2406 a a a ii e da 67 28 2 AUN ar Ee ad io a a a A 68 2 9 Modeling TLS sm em race ar a 70 2 9 1 Security Properties of TLS aoaaa a a 70 2 9 2 HTTP Request and Response Pairing 70 2 9 3 Server Authenticated HTTPS a 71 2 9 4 Weak Client Authentication 2 0000 72 2 9 5 Strong Client Authentication 0 000000 0 0a To 2 9 6 Dynamic sessions and message order preservation 80 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 3 190 3 ASLan concepts and syntax 88 3 1 Introductory example e y a a a Le ee heed ee eed we eo 88 3 2 Specifications ed ten dhe tee hae whee ere hee ce hee 2 90 3 3 Entities and agents bea hus a bk dR Ok ROR Re PS ee eS 90 3 4 Dishonest agents and the intruder 0 e 91 3 5 Facts and Clauses ra a Ee EO A 92 3 6 Declarations sd ee a 94 SR ETS ea oe ares ps a ee as ee OG a 95 39 MAMA CS tat eS enon E A O a 96 3 8 1 Channel models esa sicrpiele psa a 96 3 8 2 Channel security notions 2 84 lt 02 5540 eee Ee ee REO 97 3 8 3 Channel syntax e dis eed a9 48 AAA AA 99 BQ GOES esa ere roda de Sate e eed Bae A 105 add nv ri nts iaa ke ORE Re OEE AAA a 106 3 9 2 ASserlione Sue SEER eG EEG ESM ERED ER SE RSS BS 106 3 9 3 Channel 2008 s cs ss Shee oe Oo RO EER DEES EEE ER GO 106 gue secrecy goals e ss eee ed RS MECRE WEEE Shee weds
32. A not s V not r A not s Therefore the obtained rules will be state _BidM Actor IID s1 BP M p not s gt state _BidM Actor IID branch sl 0 BP M p state BidM Actor IID sl1 BP M not r not s gt state BidM Actor IID branch sl 0 BP M state BidM Actor IID branch sl 0 BP M gt state _BidM Actor IID succ branch sl 0 BP M q Actor state BidM Actor IID succ branch sl 0 BP M gt state _BidM Actor IID succ sl BP M as to the case where the guard holds For the opposite case i e guard evaluation fails we will proceed similarly but considering the negated guard whose DNF is not p Ar Vs generating the following rules FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 146 190 state _BidM Actor IID s1 BP M not p r gt state BidM Actor IID branch sl 1 BP M r state BidM Actor IID s1 BP M s gt state BidM Actor IID branch sl 1 BP M s state BidM Actor IID branch sl 1 BP M gt state _BidM Actor IID succ branch sl 1 BP M q Actor state BidM Actor IID succ branch sl 1 BP M gt state _BidM Actor IID succ sl BP M O Note finally that before any actual translation of the statement is put in place the function adaptGuard which we will present in detail in 4 8 is applied to each clause of the guard s DNF to convert all logical connectives into ASLan equivalent predicates This approach will be app
33. Actor ch2 gt authentic_on Actor A ch1 gt Actor M1 Actor ch2 gt B M2 The final translation into ASLan in the three models is as follows CCM FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 136 190 iknows crypt ck Actor ctag M1 L R iknows sign inv P atag B M2 Here ck is the confidentiality key of the receiver and ctag and atag are tags de scribing confidentiality and authenticity respectively The agent name B given for authentic transmissions after the atag identifies the intended receiver which captures directedness only for authentic CCM channels ICM cnfCh Actor M1 L R athCh P B M2 Here cnfCh indicates a confidential channel where its first argument is the receiver Here athCh indicates an authentic channel where its first argument is the sender and the second argument identifies the intended receiver which captures directedness ACM rcvd Actor A M1 ch1 L R sent Actor Actor B M2 ch2 Here the fact chi gt confidential_to Actor given earlier captures confidentiality to the receiver while ch2 gt authentic_on Actor captures authentiticy of the sender and the third argument of the sent fact identifies the intended receiver which captures directedness In the following paragraphs one for each channel model the translation of each channel security property is listed in detail CCM Table 8 shows the translation of sen
34. Actor ch_c2s SessID gt S Counter PayloadC channel_goal Client_TLS_Server Actor gt gt S Counter PayloadC S ch_s2c SessID gt Actor Counter PayloadS channel_goal Server_TLS_Client S gt gt x Actor Counter PayloadS assert finished false for excutability testing If the model checker does not find an attack at least here the model has an executability problem Once this pseudo attack has been shown the assertion can be commented out to check for the other goals body of Session new Client C S ChS entity Server Actor agent ChS channel Sessions agent text nat set symbols C agent SessID text entity Thread Actor C agent SessID text Sessions agent text nat set symbols N nat PayloadC PayloadS text body while true select on C ch_c2s SessID gt Actor N PayloadC amp Sessions gt contains C SessID N channel_goal Client_TLS_Server FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 87 190 C gt gt Actor N PayloadC PayloadS fresh Actor ch_s2c SessID gt C N PayloadS channel_goal Server_TLS_Client Actor gt gt C N PayloadS Sessions gt remove C SessID N Sessions gt add C SessID succ N body of the Server while true select on ChS gt Actor C SessID 0
35. Actor which is similar to this or self in object oriented programming languages The value of Actor is the name of the agent playing the role defined by the entity This is important for defining the security properties of the entity Actor must be of type agent or a subtype of it If an entity does not have a formal parameter Actor this parameter is defined implicitly The root entity must not have explicit parameters Its implicit Actor parameter has the value root 3 4 Dishonest agents and the intruder The attacker is known as the intruder and can be referred to by the constant i of type agent Yet we allow the intruder to have more than one real name To this end we use the predicate dishonest that holds true of i and of every pseudonym i e alias name A of i Once an agent has become dishonest for instance because it has been corrupted it can never become honest again Therefore a dishonest fact may not be retracted We will use dishonest also for pseudonyms freshly created by the intruder for pseudony mous channels which are discussed in more detail in 3 8 3 below see also 18 19 nb 2 to handle them correctly the translator gives a warning in this case 26 This is so far supported only by SATMC and not yet implemented in the translator 27The intruder may have several names that he controls in the sense that he has for instance the necessary long term keys to actually work under a particular name This ref
36. B stands for an agent different from Actor or any pseudonym of it i e B _ P for any P In the translation pattern in the right hand column e akP X stands for inv X if X is a pseudonym and inv ak X otherwise e ckP X stands for X if X is a pseudonym and ck X otherwise e A stands for the translation of A e B stands for the translation of B and e M stands for the translation of M where the translation of the agent pseudonym and message subterms is as defined in 4 9 In cases where a pseudonym P and is in the sending role i e for transmissions of the form P gt send B M or the equivalent P gt B M and the form B gt receive P M or the equivalent P gt B M the value of the pseudonym is additionally transmitted in unprotected fashion For instance Actor gt B M gets translated to iknows pair defaultPseudonym Actor IID crypt pk B sign inv defaultPseudonym Actor IID pair stag pair B M The transmission of the pseudonym is needed so that the receiver can send an answer or recognize different messages sent by the same pseudonymous sender ICM Table 9 shows the translation of send and receive terms obtained by replacing the predicates with the corresponding encoding for the ICM FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 138 190 ASLan predicate ASLan translation for ICM A
37. ConstraintsSection GoalsSection TypeSymbolsSection section typeSymbols Types SignatureSection section signature SuperType OpDecl TypesSection section types TypeDeclx EquationsSection section equations Equation InitsSection section inits initial_state ConstId Facts RulesSection section rules Rulex ConstraintsSection section constraints Constraint GoalsSection section goals Goal IntruderSection section intruder Clause Rule ClausesSection section hornClauses Clause Clause hc Constld Vars forall Vars Fact Fact Conditions Fact Conditions Rule step ConstId Vars PNFacts Conditions ExistsVars gt Facts Facts Fact Fact Conditions amp Condition Condition AtomicCondition not AtomicCondition AtomicCondition equal Term Term leq Term Term h PNFact stands for Possibly Negated Fact PNFacts PNFact PNfact PNFact Fact not Fact A Fact must be a Term of type fact Fact Term ExistsVars exists Vars Constraint constraint Constld Vars Formula FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 170 190 Goal LTLGoal AttackStates LTLGoal goal ConstId
38. IID n22 IID SL 1 B Req 1 Na dummy_text Nb dummy_text Bob Actor Req 1 IID n22 IID SL 4 A Wit 1 Na n7 Na Nb n20 Nb CLAUSES STATEMENTS of Alice n6 IID r i gt Wit 1 n7 Na n20 Nb _pk Wit 1 on line 16 m Nb n20 Nb from matching on line 16 request Wit 1 i auth_Alice_authenticates_Bob n7 Na n6 IID on line 16 request Wit 1 i fresh_Alice_authenticates_Bob n7 Na n6 IID on line 16 s Wit 1 gt i n20 Nb _pk i on line 18 witness Wit 1 i auth_Bob_authenticates_Alice n20 Nb on line 18 witness Wit 1 i fresh_Bob_authenticates_Alice n20 Nb on line 18 STATES Environment Actor root IID 0 SL 3 Session Actor dummy_agent IID n4 IID SL 3 A A 4 B Req 1 Session Actor dummy_agent IID n5 IID SL 3 A Wit 1 B i Alice Actor Wit 1 IID n6 IID SL 5 B i Na n7 Na Nb n20 Nb Bob Actor i IID n6 IID SL 1 A Wit 1 Na dummy_text Nb dummy_text Alice Actor A 4 IID n22 IID SL 1 B Req 1 Na dummy_text Nb dummy_text Bob Actor Req 1 IID n22 IID SL 4 A Wit 1 Na n7 Na Nb n20 Nb CLAUSES STATEMENTS of Bob n22 IID r Wit 1 gt Req 1 n20 Nb _pk Req 1 on line 31 request Req 1 Wit 1 auth_Bob_authenticates_Alice n20 Nb n22 IID on line 31 request Req 1 Wit 1 fresh_Bob_authenticates_Alice n20 Nb n22 IID on line 31 a Na n7 Na from assignment on line 32 STATES Environment Actor root IID 0 SL 3 Session Actor dummy_age
39. In our framework this boils down to adding the following constraint in the ConstraintsSection of the ASLan prelude forall Ch forall P forall A forall B forall M G implies confidential_to Ch P G implies rcvd B A M Ch equal B P The other definitions are treated in a similar way Weak confidentiality is translated as the LTL constraint forall Ch forall A forall B forall M forall A forall B forall M G implies weakly_confidential Ch G implies and rcvd A B M Ch F rcvd A B M Ch equal A A A channel provides authenticity if its input is exclusively accessible to a specified sender Authenticity is translated as the LTL constraint forall Ch forall P forall RS forall A forall B forall M G implies authentic_on Ch P G implies sent RS A B M Ch and equal A P equal RS P Weak authenticity is translated as the LTL constraint forall Ch forall RS forall A forall B forall M forall RS forall A forall B forall M G implies weakly_authentic Ch G implies and sent RS A B M Ch F sent RS A B M Ch and equal A A equal RS RS FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 141 190 In ACM resilience amounts to requiring that every message sent over the channel will be eventually delivered to the intended recipient This is translated as the LTL constraint forall C
40. _pk Wit 1 Wit 1 gt lt i gt n20 Nb _pk i lt Wit 1 gt gt Req 1 n20 Nb _pk Req 1 This attack trace demonstrates that our NSPK protocol is vulnerable to a man in the middle attack which was initially detected by Lowe 13 If we input this attack trace to Web Sequence Diagrams we obtain Figure 7 As described below it would be logically more adequate to place the node lt Wit 1 gt just right of lt gt but apparently the tool does not do this in order to avoid arrows overapping with vertical lines Wit 1 is an honest instance of Alice and Req 1 is an honest instance Bob The angle brackets lt gt around a party denote the intended or assumed communication partner of whose identity however the honest communication peer cannot be sure In other words it may be actually the intruder acting in the name of the party given Here lt i gt is the intruder in the name of himself lt gt is for Bob at least an hitherto unknown party and lt Wit 1 gt is the party that Bob assumes to be Alice which however he cannot be sure of until proper authentication and here in fact it is the intruder in the name of Alice Lowe s attack is sketched in a slightly more compact form in Figure 8 There the different forms of the intruder namely lt i gt lt gt and lt Wit 1 gt from Figure 7 all are subsumed under a single i If A initiates a session with the intruder i i e Alice wants to communicate with
41. a symbol and extend until the end of the line specification NSPK channel_model CCM entity Environment entity Session A B agent entity Alice Actor B agent symbols Na Nb text body secret_Na Na fresh Actor gt B Na Actor _pk B B gt Actor Alice_authenticates_Bob Na secret_Nb Nb _pk Actor Actor gt B Bob_authenticates_Alice Nb _pk B entity Bob A Actor agent 4 symbols Na Nb text body 4 gt Actor Na A _pk Actor Bob learns A here secret_Nb Nb fresh Actor gt A Alice_authenticates_Bob Na Nb _pk A A gt Actor Bob_authenticates_Alice Nb _pk Actor secret_Na Na Na Goal can only be given here because A certainly is not authenticated before FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 22 190 body of Session new Alice A B new Bob A B goals secret_Na _ A B Okay Asecret_Nb _ A B Attack found hhh Commented out the above goals such that hhh the attack is printed on authentiation Alice_authenticates_Bob _ B gt gt A Okay Bob_authenticates_Alice _ A gt gt B Attack found body of Environment Two sessions needed for Lowe s attack any A B Session A B where A B any A B Session A B where A B The Alice entity describing her behavior and
42. acknowledgement arrives How do we model non deterministic events in ASLan The language reference defines in 3 10 The select statement checks the guards given blocking as long as no guard is fulfilled then nondeterministically chooses any one of the fulfilled guards and executes the corresponding statement block Thus using select statements allows us to model non deterministic events This is reflected in the following ASLan specification specification TimeOut channel_model CCM entity Environment symbols alice bob agent ack message message FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 63 190 ackrcvd fact alarm fact entity Alice Actor B agent 4 symbols M message timeout fact body 4 M fresh Actor gt B M timeout select on B gt Actor ack M ackrcvd on timeout alarm entity Bob Actor A agent symbols Datum message body A gt Actor Datum Actor gt A ack Datum body new Alice alice bob new Bob bob alice goals A no_ackrevd ackrevd no_alarm alarm In this model timeout is set and therefore we expect that the fact alarm is at least in some of the executions of the model by a model checker introduced to the state For translation and model checking with Cl AtSe we simply use the following commands and options java jar asla
43. aed 109 a UN iiem sor a i a 24 od dO RoR EE A EES SOAS 111 A eae ce Se Geek les ete ces we es te fe See Shee hee a oe E E 112 3 12 Grammar in EBNF srta aa 113 3 13 ASLan prelude e amp how Gs ko a we Sow ee we SLR Ree AG we We Ee ios ha Hy 4 ASLan semantics 121 4l Preprocessing ok EA OP A E ee eS 121 4 2 Translation of Entities 00a o o 122 4 3 Translation of Types and Symbols 0 0 00 eee 124 4 4 Translation of Clauses xo yk oe ee bee a a he cd eS 125 4 5 Translation of Equations 4 0 4 21 24 6 ee Se ee Eee eS 127 4 6 Representing the Control Flow 2 0 0 eee es 127 4 7 Translation of Statements e 127 ATI RINE ses pes ease RENE eee Bee oe S 128 4 7 2 Variable assignment ooa a 44 eo e4e AA 129 4 7 3 Generation of fresh values sica ei Se YRS DRS 130 4 7 4 Entity instantiation A II 131 4 7 5 Symbolic entity instantiation cis seas ea era Bs 133 4 7 6 Send receive and channel models 134 Atel Factintrodu ctiot gt ss se ros ees e Ove Geom e oei e E 2 141 4 7 8 Fact retraction 4 cr ira a 142 10 Brito wee e e a Be ee ARA ee a de 143 AAW DODD AI 146 AIL Select ALEA AER AS A 148 4 7 12 ASS a a Ra a AA A A 149 4 8 Translation of Guards 2 lt ee ee 04 150 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 4 190 4 9 Translation of Terms 2 2 4 4844 boscosas 151
44. checker can be assigned options that are used whenever the model is analyzed For instance Oclatse hc blr sets options for CL AtSe whenever that model checker analyzes this The option gas can also be given more verbosely as goals as attack states It transforms as far as possible goal formulas as attack states which can be handled by the model checkers more efficiently than goals in LTL Linear Temporal Logic form FP7 ICT 2007 1 L Project No 216471 A ANTSSAR e Ne O O NQ 25 a SEVENTH FRAMEWORK D2 3 update ASLan specification and tutorial 24 190 model With satmc the model checker SATMC can be addressed for OFMC we must use ofmc An example for such server directives can be found below in 2 1 7 Interpreting the Model Checkers output The model checkers produce a rather abstract and low level output format called AVANTSSAR OF Each model checkers offers various options to tweak the output For instance one may launch CL AtSe with the option of if which results in a very de tailed message sequence chart like output of traces as ASLan level In traces produced by OFMC unexpected variables like x2602 may appear when an attack is possible for any non constrained value at the given term position s The ASLan connector can transform the low level AVANTSSAR OF back to a more or less ASLan level output For example the commands cl atse NSPK aslan gt NSPK atk java jar aslanpp
45. closure semantics enables us to model policy revocations in a natural way in ASLan A 3 3 Security goals A simple way to describe safety properties of a transition system is by defining a subset of so called bad states or attack states The attack states specification in ASLan is syntactically similar to a rule only that there is no right hand side The declaration of an attack state A amounts to adding a rule A A attack for a nullary fact symbol attack and defining every state that contains attack to be an attack state Another way to specify in ASLan the trust and security properties is by using LTL goals To this end we first consider the following definitions A path m is a sequence of states SoS1 such that S gt Si for i N We define a i S for alli N If Sy C T then we say that the path is initialized Let m be an initialized path of the execution model M H be a set of clauses and Y Ts An LTL formula is valid on 7 under o w r t H in symbols m F 6 if and only if 7 0 HE where 7 1 H is inductively defined as follows We suppress the superscript H when it is clear from the context H iff do r t for a fact rr 1 a equal t t2 iff tio tzo m i Ho not d if m i Eo mi Es or 9 0 if m i Ee 6 or m i Ho 4 m i Ke X 9 iff m i 1 boo m i Ho YO iff i gt 0 and r i 1 40 m i Fo F iff there exists j gt i such th
46. connector jar NSPK aslan ar NSPK atk produce the following output INPUT NSPK_Unsafe aslan SUMMARY ATTACK_FOUND DETAILS TYPED_MODEL BACKEND CL ATSE 2 5 7e_ December_27th_2010 COMMENTS CLAUSES coding internal intruder s actions are not shown EXPLICIT section shows only facts not removed by the simplification IMPLICIT section shows only facts needed for showing insecurity STATISTICS TIME 592 ms TESTED 2115 transitions REACHED 1110 states READING 0 02 seconds ANALYSE 0 57 seconds STATES Environment Actor root IID 0 SL 1 CLAUSES STATEMENTS g A 4 Req 1 on line 53 n Session Actor dummy_agent IID n4 IID SL 1 A A 4 B Req 1 on line 53 STATES Environment Actor root IID 0 SL 2 Session Actor dummy_agent IID n4 IID SL 1 A A 4 B Req 1 CLAUSES FP7 ICT 2007 1 Project No 216471 A AN T SSAR PROGRAMME 40 Al 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 a SEVENTH FRAMEWORK D2 3 update ASLan specification and tutorial 25 190 STATEMENTS g Wit 1 i on line 54 n Session Actor dummy_agent IID n5 IID SL 1 A Wit 1 B i on line 54 STATES Environment Actor root IID 0 SL 3 Session Actor dummy_agent IID n4 IID SL 1 A A 4 B
47. consider a further session adding the following statement in the body of the entity session line 41 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 105 190 new Session client server ch_c2s ch_s2c In this way the same pair of channels is shared between different sessions Alternatively the modeler can consider the following session new Session client server ch_c2s_new ch_s2c_new For instance in case of the unilateral_conf_auth channel relation the use of different channels allows to model different TLS sessions Channels may be created even dynamically by producing fresh channel names and using these new values when stating their security properties and when sending and receiving on these channels See 2 9 6 for an example Extensions It is important to note that we have designed ASLan so to allow the modeler to choose the particular channel model he wishes to consider We have therefore introduced the schematic notation considered above which can then be translated to different models and is open to the extension with other features such as further channel types e g like the ones considered in 10 a more fine grained definition of the nature of a pseudonym and so on which may be realized in a different way depending on the particular underlying channel model In other words as we will see in more detail below we deliberately did not fix the semantics o
48. declare a communication has special security properties without saying how they are achieved They just are assumed present by us and the model checker We use assumptions if we do not want to bother with implementation details We will not use communication security assumptions in our NSPK example but rather implement the security ourselves In the following we assume communication security implemented via encrypted and signed messages using the AVANTSSAR CCM cryptographic channel model For more detail and other channel models see 3 8 FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 15 190 Na fresh goal secret_Na Na A B Kb assumed known Nb fresh goal secret_Nb Nb A B Ka assumed known Check if Na is the same goal A_auth_B Na B gt gt A Check if Nb is the same goal B_auth_A Nb A gt gt B Figure 4 The Security Goals for the NSPK Protocol Thus they require as communication goals two secure and fresh message transmis sions one from Alice to Bob and one from Bob to Alice A_auth_B Na B gt gt A and B_auth_A Nb A gt gt Bare the primary authentication goals Their names are A_auth_B and B_auth_A The secondary secrecy goals for the transmitted nonces see above are secret_Na Na A B and secret_Nb Nb A B The respective nonces may not be disclosed to the attacker
49. does not support inherited variables and CL AtSe requires at least the option FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 91 190 with the same name However redeclaring elements of the same kind e g two function declarations or two sub entity declarations with the same name at the same level in the same entity is not allowed Entities may be instantiated to processes or threads executing the body of the entity which contains statements like in procedural programming languages see 3 10 for details Entity execution is usually compressed which means that the statements in its body are executed atomically except for certain breakpoints Immediately before these breakpoints compressed execution is broken up such that other entities and the intruder may interleave By default there is just one breakpoint action namely the reception of messages Optionally the modeler may specify for each entity a set of additional breakpoint actions before the entity s body This set is inherited to sub entities unless these declare their own set of additional breakpoint actions One can specify LTL constraints as assumptions in the root entity therefore it is possible to specify constraints on all goals of the model which from the security standpoint is equivalent to constraints on the execution of the overall system Each entity has an explicit or implicit formal parameter
50. formal semantics is provided at the ASLan level as defined in 4 7 6 using LTL constraints The facts indicating the assumed security properties of a channel must be introduced before the channel is used and should not be retracted They are typically stated in the body of the entity Environment or a session entity Note that the confidentiality and authenticity properties defined in the table refer to a pair of agents In principle multiple senders and or recipients can be defined for a channel but currently they are not supported Further note that the weak form of confidentiality and authenticity are obtained in CCM by using pseudonyms For any given channel the properties of weak confidentiality weak authenticity and resilience etc may be combined freely To give an example of ACM channels let us consider the following specification Two entities and the respective agents client and server are involved and two channels are defined lines 7 ch_c2s and ch_s2c The channel ch_c2s is confidential to the server line 43 while the channel ch_s2c is authentic for the server line 44 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR FOoOWOOnNnN oor wh Fe SFE BBP BP KBRWWWWWWWWWwWnNnN nD nN NN NNN N PHP E ppp OoPrPwNnNrFrFoPnrooOonNtoaoow trwNrFoOwPOoOonNntoaorhwWNrF OO OND OK W DH a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 103 190 specification ACM_example channel_
51. from A Nonce fresh SharedDB gt add Actor Nonce 1 add entry to DB Actor gt A Nonce handover to A A gt Actor handover from A assert test_sharedDB_B SharedDB gt contains Actor Nonce 1 should report violation because now A has removed B s entry from the shared DB body 4 SharedDB 4 new Alice A B SharedDB new Bob A B SharedDB body any A B Session A B where A B Q dishonest A dishonest B In this example the Session provides an empty shared database to Alice and Bob a reference to which they obtain as parameter The contents of the shared database are common to both Alice and Bob call by reference semantics Alice puts an entry with her name into the database and hands over to Bob Bob puts an entry with his name into the database and hands back to Alice Alice checks whether Bob has entered an entry with his name into the database and in case he did removes that entry Then she hands over to Bob Bob checks whether his entry is still in the database and complains if this is not the case any longer In fact once you translate and checkt this model with java jar aslanpp connector jar hc all gas 19For more information on connector and model checker options please see Appendix B FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 54 190 SharedDB_Unsafe aslan o Sha
52. in the translation of the receiving statement where IID is the instance ID of the ancestor entity E In this way the intruder is added to the set of agents allowed to know the secret because the confidentiality channel goal is required to hold only until reception of the secret Authenticity and freshness We can now define the semantics of authenticity and fresh ness as LTL formulae to be used as LTL goals or equivalently used in negated form as attack states over the given facts without referring to the particularities of the specified entities such as the message formats The built in LTL semantics of the authentication goal is forall A BM IID request B A P M IID gt lt gt witness A B P M dishonest A where P is the protocol ID of the goal as defined above This is a standard authentication goal non injective agreement 14 which includes directedness 45Tn the translation lt gt witness A B P M is simplified to witness A B P M which is equivalent because witness facts are stable i e they are never retracted FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 157 190 For the channel compositionality results of 18 it is necessary strengthen this with the additional condition that if the sender is dishonest then the intruder must know this message This involves negation of iknows facts which so far is supported by SATMC only The
53. know which agent variables inside the Bob entity the security goals given in the Session entity are connected to FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 23 190 java jar aslanpp connector jar gas NSPK aslan o NSPK aslan The gas option is recommended as it makes the goals easier to handle for the auto mated model checkers The error messages and warnings of the compiler should be largely self explanatory Only should you encounter a quite cryptic message like no viable alternative at then it is best to look in close proximity of the location indicated in the message for some trivial syntax error violating the grammar given in 3 12 Please note that due to the intentional commenting out of the secrecy goal templates in the Session entity you will on executing above command receive a list of warnings from the translator that undefined secrecy goals are referred to in the Alice and Bob entities This of course obviously is true but you at this point can safely ignore these warnings and use the resulting NSPK aslan file for analysis by the model checkers Checking the ASLan Model We can now submit the ASLan model to one or more of the back ends of the AVANTSSAR Platform namely CL AtSe OFMC and SATMC All three model checkers are available in both an online and offline version For directions please refer to the AVANTSSAR home page at http www a
54. must be disjoint from the variables appearing in the LHS The variables of the RHS must be a subset of the variables in the positive facts of the LHS excluding FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 173 190 those variables that occur only in the conditions or the negative facts of the rule and the existentially quantified variables Analogous restrictions apply for initial states Further variables cannot occur in an initial state as it can be seen as the RHS of a rewrite rule with an empty LHS For a clause declaration the variable list must contain exactly those variables that occur in the clause Variables on the LHS of the that do not appear in the RHS if any must be declared in the prefix forall var_list and they are interpreted as universally quantified over their type set A 2 5 Constraints on fact symbols We partition the set of predicates defined in SignatureSection into state predicates and policy predicates the predicates appearing in the head of clauses are called policy predicates the rest of the predicates are called state predicates In any ASLan specification we require that no policy predicate appears in the RHS of a rewrite rule We consider the predicate iknows used to model the intruder knowledge as the only exception to this restriction That is facts of the form iknows M can occur freely in rewrite rules and clauses Note that if a poli
55. n7 Na Nb dummy_text Bob Actor i IID n6 IID SL 1 A Wit 1 Na dummy_text Nb dummy_text Alice Actor A 4 IID n22 IID SL 1 B Req 1 Na dummy_text Nb dummy_text Bob Actor Req 1 IID n22 IID SL 1 A A 4 Na dummy_text Nb dummy_text CLAUSES STATEMENTS of Bob n22 IID r gt Req 1 n7 Na Wit 1 _pk Req 1 on line 28 m A Wit 1 from matching on line 28 m Na n7 Na from matching on line 28 f Nb n20 Nb from fresh on line 29 s Req 1 gt Wit 1 n7 Na n20 Nb _pk Wit 1 on line 30 witness Req 1 Wit 1 auth_Alice_authenticates_Bob n7 Na on line 30 witness Req 1 Wit 1 fresh_Alice_authenticates_Bob n7 Na on line 30 STATES Environment Actor root IID 0 SL 3 Session Actor dummy_agent IID n4 IID SL 3 A A 4 B Req 1 Session Actor dummy_agent IID n5 IID SL 3 A Wit 1 B i FP7 ICT 2007 1 Project No 216471 A AN T SSAR PROGRAMME 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 131 132 133 134 135 137 138 139 140 141 142 143 144 145 146 147 148 149 151 152 153 154 155 156 157 159 160 161 162 164 165 166 167 168 169 D2 3 update ASLan specification and tutorial 26 190 Alice Actor Wit 1 IID n6 IID SL 3 B i Na n7 Na Nb dummy_text Bob Actor i IID n6 IID SL 1 A Wit 1 Na dummy_text Nb dummy_text Alice Actor A 4
56. need to preserve the original sets we must use the copy strategy introduced in the previous paragraph This is left to the reader as simple exercise Intersection Analogously if we want to compute the intersection of two sets and do not need to preserve the original sets we can proceed as follows MySetIntersectionResult 1 Provide a fresh location MySetIntersectionResult MySeti MySet2 while MySet1 gt contains E if MySet2 gt contains E MySetIntersectionResult gt add E MySet1 gt remove E After this MySetIntersectionResult contains the intersection of MySet1 and MySet2 The latter set has been left unchanged whereas MySet1 is now empty Again if we need to preserve the original MySet1 we must use the copy strategy Minus If we want to subtract all elements of one set from another set not needing to preserve the original set we might do this as follows MySetMinusResult Provide a fresh location MySetMinusResult MySeti MySet2 while MySet1 gt contains E if MySet2 gt contains E MySetMinusResult gt add E MySet1 gt remove E FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 45 190 After this MySetMinusResult contains those elements of MySet1 not part of MySet2 The former set is now empty whereas the latter set is still in its original state If we need to preserve the original MySet1 we must tak
57. online versions of the AVANTSSAR Tools B 1 ASLan Connector This section sketches how to use the ASLan connector and the various options available to fine tune the behavior of the ASLan connector as well as the strategies to use special options for the connector with the targeted model checker Usage java jar aslanpp connector jar INPUT_FILE E preprocess ar analysis result ANALYSIS_RESULT gas goals as attack states gv graphviz DIR h help hc horn clauses level ALL NPI NONE o output OUTPUT_FILE opt optimization level NONE NOPS LUMP orch orchestration client CLIENT_ENTITY_NAME pp pretty print so strip output v version Available options INPUT_FILE Input file with ASLan specification that should be translated to ASLan or with the ASLan specification for which the analysis result should be trans lated to ASLan Read input from stdin instead of from a file E preprocess Perform only preprocessing of the ASLan specification Macros are expanded and a detailed representation of the specification is returned Hidden FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 180 190 symbols added automatically during the translation are also shown so the specifi cation that is returned cannot be used again as a valid ASLan specification This options is i
58. protection e A gt B M denotes confidential communication A sends some payload M that only B can read However B cannot be sure of the identity of A as long as A has not been authenticated so B cannot be sure this M has really been sent by A e A gt B M denotes authentic communication B can be sure of the identity of A as A has been authenticated The M that B receives here indeed comes from A It has not been altered in transmission i e integrity of M is granted Moreover the intended recipient B is included into the integrity protection so B can rely on the message being meant for him However the communication is not confidential thus any eavesdropper can access the contents in transit from A to B A gt B M denotes secure communication in the sense that A has been authenti cated the payload M is integrity and confidentiality protected and it is intended by A for B It does not protect against message replay re ordering suppression and delay as well as traffic analysis e A gt gt B M denotes replay protected fresh communication The message M sent by A is accepted only once by B This notation may only be used for communication including at least sender authenticity Goals for NSPK The main goal of Alice and Bob in our NSPK example is to authenticate each other After checking of nonces A and B assume that they have securely and freshly authenticated the other party 3With an assumption we
59. steps then there simply is no corresponding macro step according to our definition FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 179 190 B Connector and Model Checker Options This appendix gives a brief overview on how to fine tune the ASLan connector and the model checking back ends by using various options The ASLAN connector and the model checkers are available in both an online and offline version In the offline version you supply the options in the command line This method used in this chapter when describing the available options of the various tools In the online version you may set the required options in the Set Options form field In case of the model checkers you may also include the options in a model checker directive at the very beginning of the ASLan model definition Here as a kind of comment each model checker can be assigned options that are used whenever the model is analyzed For instance clatse hc blr sets options for CL AtSe whenever that model checker analyzes this model With satmc the model checker SATMC can be addressed for OFMC we must use ofmc For more details regarding the operation of the ASLan connector and the model checkers please refer to Deliverable 4 2 6 The AVANTSSAR Tools are available for download on the AVANTSSAR home page at http www avantssar eu Menu Item Avantssar Platform There you ll also find directions to
60. that NFoo is ground NCoo holds for all substitutions o such that NCoo is ground and S S PFo U Roo where o is any substitution such that for all v V vo does not occur in S or in any algebraic equation declared in the prelude specification oo F WwW N FR We remark that the closure of states w r t clauses is computed implicitly here in contrast to the explicit closure semantics which was given in Deliverable D2 1 1 The difference between the semantics is best shown via an example Let us consider a state s a and the clause c b with a b and c being ground facts Note that s a FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 175 190 w r t the clause above Now given the rewrite rule a b s is rewritten to s b with si b c in the implicit closure semantics and s is rewritten to s b c in the explicit closure semantics The difference between these semantics becomes evident now by considering the following rewrite rule b gt a Then s is rewritten to s2 a with s2 a in the implicit closure semantics while s is rewritten to s3 a c Note that in the implicit closure semantics c is removed from the closure of sg because the cause for c namely b is not contained in sg In explicit closure semantics however c is present in s even after b is removed This feature of the implicit
61. the AVISPA Tool and all of its back ends However the IF language has the following major shortcomings that make it unsuited for the analysis of complex services FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 168 190 e In IF the behavior of the system can only be described by means of transitions and this makes IF inadequate to express security policies which are usually best described as invariants e In IF security goals can only be expressed as reachability properties and this makes IF inadequate to express complex security goals e g fair exchange that occur in complex services To overcome these shortcomings we have defined ASLan by extending IF with the following two important features Horn Clauses In ASLan invariants of the system can be defined by a set of Horn Clauses Horn clauses allow us not only to capture the deduction abilities of the attacker in a natural way but also and most importantly they allow for the incorporation of authorization logics in specifications of services LTL In ASLan complex security properties can be specified in LTL As shown for instance in 3 this allows us to express complex security goals that services are expected to meet as well as assumptions on the security offered by the communication channels Moreover in IF the intruder can always overhear or intercept messages and fake new ones This is not always possible in re
62. to his public key pk Actor In line 9 Bob sends A s nonce Na and his freshly generated own nonce Nb from line 8 to that A that he has learned in line 2 encrypted with that A s public key In line 10 Bob receives back from A his nonce This nonce must have the same value as the one he sent to A Checking for equality is performed implicitly and indicated by the absence of the Again decryption is performed implicitly as Bob s private key is available within the Bob entity The security goal names secret_Nb line 8 Alice_authenticates_Bob line 9 Bob_authenticates_Alice line 10 and secret_Na line 11 refer to security goals that must be met and may not be violated We look this in more detail right now ASLan Goal Specification Conventions For reference by the model checker in ASLan every goal needs to be given a name Naming conventions propose to name a secrecy goal by the item that is to be kept secret and a channel goal a communication goal e g authentication integrity confidentiality replay protection by the sender receiver specific security characteristic such as authentication and within the respective sub entities the message value that is communicated Security goals are specified within entity definitions If more than one entity wants to require a given security goal to be met the security goal must be declared in the enveloping entity If not all parameters required in the security goal sp
63. tried out All models plus a number of benchmark tests for exploring various features of ASLan and the AVANTSSAR Tools are available for download on the AVANTSSAR home page at http www avantssar eu via the menu items Test Library and Avantssar Platform There you will also find directions to online versions of the AVANTSSAR Tools 2 1 Hello World This subsection describes the first steps with modeling in ASLan as well as using the translator and the AVANTSSAR Platform and its back end model checkers It is mainly targeted to those who are used to designing communication protocols and to application level programming in a contemporary language like Java Familiarity with formal modeling is not a prerequisite 2 1 1 The Problem As a running example we use variants of the simple well known Needham Schroeder Public Key NSPK Protocol 21 This protocol is intended to provide mutual authentication between two parties communicating over a network but in its proposed form is insecure There is an attack 13 that the tools can detect and the reader can correct the protocol suffers also from other weaknesses that are described in the literature but that are not of interest here We give a walk through the whole range of steps required from understanding the original protocol to correcting it based on the feedback provided by the model checkers The protocol runs between two parties A Alice and B Bob In the simple Alice and B
64. undecidable and thus the modeler should interactively increase the bound until an attack is found or the problem gets too big Level of Rebuilding As pointed out above Cl AtSe tries by default to extract coher ent sessions from the ASLan v1 specification A session for Cl AtSe is a longest sequence or tree of transitions that is played by one and only one agent and where each transi tion appears only once The kind of session used by ClAtSe is controlled by the option 1v1 level of rebuilding A 0 value is the safe mode where one transition is equal to one session The values 1 and 2 default are two rebuilding methods and should be equivalent Identifying sessions within an ASLan v1 file may fail due to the structure of the specification the syntax does not guarantee that simple sessions can be rebuilt and moreover sometimes building sessions is equivalent to enumerating all execution traces In such situation the tool will fallback to the default 1v1 0 option and write a mesage like Forced use of the lvl 0 option A successful session rebuilding often means better analysis performances Output Formats Many levels of verbosity or even output syntaxes are available with Cl AtSe Those kind of outputs are controlled by the of option which accepts many values ASLan for the standard ASLan output format as defined in the Avantssar s deliverables if if and ift
65. witness switness wwitness wrequest request srequest error B 4 Cl AtSe This section sketches how to use the model checker CL AtSe and the various options available to fine tune its behavior as well as the various specific characteristics and idiosyncrasies of this backend Properties and Limitations The Cl AtSe model checker analyzes Avantssar s ASLan vl files w r t a bounded number of sessions The tool supports associative assoc or non associative free pairing symbol as well as the algebraic properties of xor and exponential There is no need to include such properties in the specification these are hard coded in the tool Also both the typed typed and untyped untyped models are supported The tool is backward compatible with the Avispa project It has currently two main limitations w r t ASLan horn clauses with an intruder knowledge in the LHS are not supported except those coding composition or decomposition of functions and LTL goals are limited to those that the tool can automatically translate to attack states Besides that the support is complete Horn Clauses For horn clauses it is important to know what strategy the tool employ in Cl AtSe this is a backward strategy This means that horn clauses are used when and only when some fact is required to be build by e g the LHS of a transition Other tools may employ a forward strategy where the set of known facts is saturat
66. your ASLan file FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 38 190 loops If you require a loop to be executed a lot of times you might need to experiment a bit before finding the optimal nb value If you choose an insufficient one when exceeding the maximum number of iterations CL AtSe just quietly exits at that point and reports that no attack was found until then This however you will notice by an appropriately placed assert finished false The equivalent applies to situations in which you try to remove an element from a set that this element is not contained in Or if you attempt to retract a fact that has not been introduced before So again before actually starting to check your model for real attacks we strongly advise you first to make sure and double check that all parts of the modeled protocol system can in fact be reached and executed 2 2 2 Detecting uninitialized variables A problem easily overlooked is that variables might be used without being initialized first This typically leads to attacks not found or spurious wrong attacks being reported For example the following entity declaration contains four such mistakes entity Test implicit Actor parameter not initialized symbols U message S message set body send i U sends an uninitialized msg variable S gt add i uses an uninitialized set variable S 4 initialize
67. 1978 T Dierks and E Rescorla The Transport Layer Security TLS Protocol Version 1 2 IETF RFC 5246 Aug 2008 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR
68. 2 and f_1 f_2 V f1 2 or f 1 f 2 gt f_1 gt f2 implies f_1 f_2 Vv forall V_1 V_n f forall V_1 forall V_N f exists V_1 V_n f exists V_1 exists V_N f neXt X f X f Yesterday Y Y f Finally lt gt f F f Once lt gt f O f Globally 0 G f Historically H f Until U _1 _2 U f_1 f_2 Release Rf 47 2 R _1 f_2 Since sS f_1 f_2 S f_1 f_2 Table 12 Translation of goals 4 12 2 Channel Goals As we described above we can use the bullet annotations to specify different kinds of trans mission goals of a service Intuitively this means that the service should ensure the authentic A ANTSSAR FP7 ICT 2007 1 Project No 216471 a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 154 190 confidential or in other ways protected transmission of the respective message Note that all these goals are independent of the channel model which only affects the assumptions on channels These definitions are close to standard authentication and secrecy goals of security protocols e g 9 14 17 As we remarked we focus here on these kinds of channels as goals and to the kinds of channels as assumptions discussed above but of course additional kinds might be possible by extending the syntax and semantics we give here Auxiliary events In order to formulate the goals in a service independent way we use in the t
69. 3 5 It not only further consolidates ASLan and ASLan but also comes with a tutorial for the benefit of modelers learning how to use ASLan Background on ASLan The first version of ASLan initially called ASLan v 2 was introduced in deliverable D2 2 4 In deliverable D2 3 5 we built upon that previous version in particular by adding extensive support for using channels abstractions and also automating a number of optimization techniques The present document covers further minor extentions and clarifications We have developed ASLan to achieve the following design goals e The language should be expressive enough to model a wide range of service oriented architectures while allowing for succinct specifications e The language should facilitate the specification of services at a high abstraction level in order to reduce model complexity as much as possible e The language should be close to specification languages for security protocols and web services but also to procedural and object oriented programming languages so that it can be employed by users who are not experts of formal protocol service specification languages In order to support formal specification of static and dynamic services and policy com position ASLan introduces a number of features e Control flow constructs e g if and while enhance the readability and conciseness of the specifications and make the specification job easier for modelers who a
70. 4 10 Translation of the Body Section o oo aa a 6 4624 ea wees 152 4 11 Translation of the Constraints Section ooo o 2008 153 4 12 Translation of the Goals SectioN a 0202 eee ee 153 4 12 1 Wee 2 oh eee ete ek ee ee hee ee RBS ee 153 4 12 2 Channel Ones eibar Se OE A 153 4 12 3 Secrecy Goals ciertos rra a eS ee RA A 157 4 13 Assignment of numbers to step label terms 158 4 14 Step COMPS SION sos i ai e a e ee ee SE 159 4 14 1 Motivation and example 242 44 mi fa eae oe eae nee 159 4 14 2 Step granularity and breakpoints 2 645 24 ebb ee ees 160 4 14 3 Translation of compressed steps o 160 MERO eta o oo pk eed eee ee aw hee See ee BOGE ee 162 4 15 1 Elimination of empty transitions and redundant guards 162 4 15 2 Merging of transitions sia edad yee de See eho 164 5 Conclusion 166 A ASLan 167 sI 167 A 2 ASLan IN a a AA RU A A PE ee O es A 168 A 2 1 GrammarinBNF 168 A 22 Structure of an ASLan File 4 4 lt i 404 boas OH ee OH OS 171 A 2 3 Constraints on identifiers 4 44 amp 4 8 4 ace Gee Hace ee i A 2 4 Constraints on variables eses esa KR aw KH TA A 2 5 Constraints on fact symbols ce 4 hee os aah a a 173 Awa ASLan Semantics y e io e as PU a RARA 173 Al Egualiti s xes es ads a A Depia a 173 A 3 2 Execution model us aoaaa aaa ed ds eed and edad uE x Iro A 3 3 Security goals i
71. A ANTSSAR Automated VAlidatioN of Trust and Security of Service oriented ARchitectures FP7 ICT 2007 1 Project No 216471 WWW avantssar eu Deliverable D2 3 update ASLan specification and tutorial Abstract This updated deliverable introduces ASLan the AVANTSSAR specifica tion language ASLan has been designed for formally specifying dynam ically composed security sensitive web services and service oriented architec tures their associated security policies as well as their trust and security properties at both communication and application level We introduce ASLan by means of a tutorial and a formal definition The semantics of ASLan is defined by translation to ASLan the low level input language for the back ends of the AVANTSSAR Platform Deliverable details Deliverable version v2 0 Classification public Date of delivery March 2011 Due on Editors SIEMENS ETH Zurich UNIVR IBM and all Total pages 190 Project details Start date January 01 2008 Duration 36 months Project Coordinator Luca Vigano Partners UNIVR ETH Zurich INRIA UPS IRIT UGDIST IBM OpenTrust IEAT SAP SIEMENS SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 2 190 Contents 1 Introduction T 2 ASLan tutorial 9 2 1 Hello World cos ie nee Keene e ee oR OS OER a EHS 9 2 130 The Problem ses Peace eee de we dee oes e es 9 2 1 2 Automated Security Analysis
72. B 1 we can query the database if an entry of a certain form is present or not SharedDB gt contains B 1 For more details on sets and how to use them see the ASLan syntax definition in 3 and the set examples in 2 3 To make our database shared between the entities Alice and Bob we declare it in the entity immediately enclosing these two entities which is the Session entity Session passes the reference to the shared database to Alice and Bob as parameter For the complete example see the following listing Overbatim Modifiable contents of shared database ofmc NO specification SharedDB_Unsafe channel_model CCM entity Environment entity Session A B agent 1 symbols SharedDB agent text nat set Contents global for Alice and Bob entity Alice Actor B agent SharedDB agent text nat set symbols Nonce text body Nonce fresh SharedDB gt add Actor Nonce 0 add entry to DB Actor gt B Nonce handover to B B gt Actor handover from B if SharedDB gt contains B 1 4 SharedDB gt remove B 1 remove B from DB Nonce fresh SharedDB gt add Actor Nonce 2 add entry to DB Actor gt B Nonce handover to B FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 53 190 entity Bob A Actor agent SharedDB agent text nat set symbols Nonce text body 4 A gt Actor handover
73. BP M gt state _BidM Actor IID succ branch sl n BP M q_n state BidM Actor IID succ branch sl n BP M gt state _BidM Actor IID succ sl BP M 4 7 12 Assert Assert stmt rest sl return_sl stmt assert assertion name exists V_1 V_n Guard W_1 W_m intersection of variables of Guard but excluding V_1 V_n and the variables in the scope of the entity check fresh predicate the name of which includes assertion name on m variables of types agreeing with W_1 W_m plus the entity instance ID IID and the next step label succ sl LHS state fact for this entity with step label sl FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 150 190 state facts for the owners of W_1 W_m RHS state fact for this entity with step label succ sl state facts for the owners of W_1 Wm check W_1 W_m IID succ s1 add LHS gt RHS to section rules in the translation LHS state fact for this entity with step label succ sl check W_1 W_m IID succ s1 RHS state fact for this entity with step label succ succ sl add LHS gt RHS to section rules in the translation add check W_1 W_m IID SL gt exists V_1 V_n Guard to the section goals in the translation ParseCode rest succ succ sl return_sl An assert statement is translated into two rules one adding a fresh predicate check
74. Empty operator Yet the mentioned fact allows us to check whether the set is empty We have learned already that the statement MySet gt contains E returns a single random value as long as there is at least one element in the set Here we use just a since we are not interested in any specific element value Add add MySet E or equivalently MySet gt add E This statement adds the element E to MySet If the element is in the set already then the addition has no effect Remove remove MySet E or equivalently MySet gt remove E This statement removes the element E from MySet Here also you can use a like a wildcard with the element name If multiple elements would qualify this statement still removes just one single random element Please be aware if you try to remove a specific element from a set ensure first that this element really is contained in the set Otherwise execution simply block at this point The same applies for trying to remove a wildcard element from an empty set These basic commands allow us to query and manipulate sets 2 3 2 ForAll and Copy If we want to copy sets and or perform some actions on all elements of a set things get more complex As we have seen a set is merely a pointer to a location where the elements in the set are stored rather than the set itself Moreover we cannot access the elements in the set sequentially since set elements are not ordered so there is no next oper
75. FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 84 190 Sessions gt contains C SessID N we can query the database for an entry being present or not Sessions gt contains C SessID N For more details on sets and how to use them see the ASLan syntax definition in 3 and the set examples in 2 3 Note that the last statement in the client s body is used to test the specified protocol is fully executable The model checker should find an artificial attack on reaching this line If the model checker does not find this attack then the protocol can not be executed as intended In this case we need to eliminate the blocking point s making sure for instance that all messages sent match the expectations at the receiver s side etc For more details on executability please see 2 2 1 within this document If you want the check this model yourself you may copy the model into a file named TLS aslan and use the following command for translation java jar aslanpp connector jar hc all gas TLS aslan o TLS aslan To check the model with SATMC you need to set no special options For OFMC please use the options classic untyped When you want to use CL AtSe you must state the option nb 2 For instance to check the model off line with CL AtSe you can use the following commands cl atse TLS aslan nb 2 gt TLS atk java j
76. H variable used by Java For example if your imported aslan files are located in the common directory you can set the ASLANPATH variable by invoking java with the D argument like this java DASLANPATH common jar aslanpp connector jar The current directory is automatically included in the ASLANPATH so there is no need to manually add it B 2 SATMC This section sketches how to use the model checker SATMC and the various options available to fine tune the behavior of SATMC as well as the various specific characteristics and idiosyncrasies of this backend You can execute SATMC by issuing at the shell prompt Usage satmc OPTION satmc FILE OPTIONS satmc OPTIONS f FILE FILE is the ASLan file comprehensive of the path you want to analyze With SATMC you can use the following options h help display this help and exit v version output version information and exit n MAX max MAX MAX is the maximum depth of the search space up to which SATMC will explore it can be set to 1 meaning infinite but in this case the procedure is not guaranteed to terminate by default it is set to 80 enc ENC ENC is the selected SAT reduction encoding technique it can be set to either gp default value or 1t1 gp The 1t1 gp encoding supports the specification of security properties and constraints in linear temporal logic LTL mutex MUTEX MUTEX is an integer indicating the level of t
77. Horn clauses e g iknows crypt K M iknows K iknows M iknows M iknows crypt K M iknows inv K There are two reasons however to fix the meaning of some symbols with a kind of standard interpretation First some symbols like in the above examples have been con sistently used over a long time with a fixed meaning and serious misunderstandings may occur if somebody attaches a different meaning to them Second validation tools may have specialized techniques for some symbols such as intruder deduction with a predefined set of operators in order to capture the subclass of models for which some tools are specialized it is necessary to have fixed symbols For both these reasons we have defined an ASLan standard prelude that contains standard definitions such as the above ones and that is considered imported by all ASLan specifications The semantics section 4 assumes the declaration of several standard symbols in the prelude such as the type symbol agent The types and functions that all back ends should support are collected in a module with the name Prelude defined as follows entity Prelude 4 very basic types and related symbols types fact protocol_id message channel for ACM nat lt message symbols i root agent dishonest agent fact iknows message fact its argument may also be of any set type true false fact 0 1 2 3 nat succ nat nat message message m
78. Message Sequences Frequently communication protocols as NSPK are developed and discussed using message FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 12 190 Na fresh Kb assumed known Nb fresh Ka assumed known Check if Na is the same Check if Nb is the same Figure 3 The annotated Sequence Chart for the NSPK Protocol sequence charts as for instance depicted in Figure 2 For better efficiency it is advisable to use a text based sequence chart editor like the Quick Sequence Diagram Editor or Web Sequence Diagrams For instance Web Sequence Diagrams takes as input A gt B Na A Kb B gt A Na Nb _Ka A gt B Nb Kb and automatically produces as output the chart shown in Figure 2 Role Behavior Usually a communication protocol specification contains details not expressible in Alice and Bob notation or simple message sequence charts In our NSPK example such actions are for instance how and when values like nonces and agent names are computed and checked That is Na fresh and Nb fresh are newly created random values public keys Ka and Kb are assumed as known and Na and Nb are checked for equality by their respective issuers Ihttp sdedit sourceforge net 2http www websequencediagrams com FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 13
79. Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 126 190 hc h A A 1 A n A A1 amp An amp state do 1 amp amp state fo m so that each variable in the clause that exists in the scope of E is bound to the value the variable currently has in its owning entity instance Example 2 Take the entity declaration for the BidM above extended with a clause asserting that the bid manager trusts the bidding portal on any message as follows entity BidM Actor BP agent clauses bmTrustBpOnAnyMsg X trusts Actor BP X saidTo BP Actor X The only free variable in the clause is X while Actor and BP are bound to the values of the parameters If this clause were transcribed to an ASLan specification as is hc bmTrustBpOnAnyMsg Actor BP X trusts Actor BP X saidTo BP Actor X then Actor and BP would be considered as universally quantified and the clause would change its meaning entirely anyone would trust any entity who says something Adding instead the state fact to the conditions of the clause hc bmTrustBpOnAnyMsg Actor BP X trusts Actor BP X saidTo BP Actor X amp state BidM Actor IID SL BP M Actor and BP are bound by the state fact state BidM Actor IID SL BP M to belong to an instance of the entity O We remark that variables which appear under the forall quantifier in a clause are interpreted universally For insta
80. Req 1 Session Actor dummy_agent IID n5 IID SL 1 A Wit 1 B i CLAUSES STATEMENTS n Alice Actor Wit 1 IID n6 IID SL 1 B i Na dummy_text Nb dummy_text on line 38 n Bob Actor i IID n6 IID SL 1 A Wit 1 Na dummy_text Nb dummy_text on line 39 STATES Environment Actor root IID 0 SL 3 Session Actor dummy_agent IID n4 IID SL 1 A A 4 B Req 1 Session Actor dummy_agent IID n5 IID SL 3 A Wit 1 B i Alice Actor Wit 1 IID n6 IID SL 1 B i Na dummy_text Nb dummy_text Bob Actor i IID n6 IID SL 1 A Wit 1 Na dummy_text Nb dummy_text CLAUSES STATEMENTS of Alice n6 IID f Na n7 Na from fresh on line 14 s Wit 1 gt i n7 Na Wit 1 _pk i on line 15 STATES Environment Actor root IID 0 SL 3 Session Actor dummy_agent IID n4 IID SL 1 A A 4 B Req 1 Session Actor dummy_agent IID n5 IID SL 3 A Wit 1 B i Alice Actor Wit 1 IID n6 IID SL 3 B i Na n7 Na Nb dummy_text Bob Actor i IID n6 IID SL 1 A Wit 1 Na dummy_text Nb dummy_text CLAUSES STATEMENTS n Alice Actor A 4 IID n22 IID SL 1 B Req 1 Na dummy_text Nb dummy_text on line 38 n Bob Actor Req 1 IID n22 IID SL 1 A A 4 Na dummy_text Nb dummy_text on line 39 STATES Environment Actor root IID 0 SL 3 Session Actor dummy_agent IID n4 IID SL 3 A A 4 B Req 1 Session Actor dummy_agent IID n5 IID SL 3 A Wit 1 B i Alice Actor Wit 1 IID n6 IID SL 3 B i Na
81. S2C C S This in particular implies via link Ch_C2S Ch_S2C that the client instance sending on the former channel is the same as the one receiving on the latter channel Therefore hhe client_link goal given for the CCM variant is automatically fulfilled Also the replay protection is automatically fulfilled via the implied weakly_confidential Ch_S2C property Thus for the ACM variant we do not need to construct these properties with the nonce Nc For more details on such channel types see Table 5 Finally observe so far our model does not include a mechanism to ensure ordering in which messages are sent and this is of course not necessary when every session contains only one message in each direction Modeling such an order preservation is more involved and we come back to this later in 2 9 6 2 9 5 Strong Client Authentication A very common application of the unilateral TLS channels with weak client authentication that we have just modeled is the use for a secure login i e the so far unauthenticated client sends his or her username and password to the server and thereby authenticates The idea is that now to use the aforementioned properties responses go to exactly the client who sent the requests whoever this is and sender invariance over several transmissions of a session it is ensured that it must be the same client Together with the authentication that the login provides it follows that all messages are securely transmitted
82. SAR D2 3 update ASLan specification and tutorial 128 190 symbEntGen SymbEntGen stmt rest sl return_sl transmission Transmission stmt rest sl return_sl introduceFact IntroduceFact stmt rest sl return_sl retractFact RetractFact stmt rest sl return_sl branch Branch stmt rest sl return_sl loop Loop stmt rest sl return _sl select Select stmt rest sl return _sl assert Assert stmt rest sl return_sl grouping Grouping stmt rest sl return_sl else No statement left to parse if return_sl null LHS state fact for this entity with step label sl RHS state fact for this entity with step label return_sl add LHS gt RHS to section rules in the translation The procedure analyzes the first statement in the list given calling the appropriate sub procedure according to the statement s type When no statements are left to parse either the execution of the main thread is finished or that of a branch is In the latter case a return step label is provided and a new idle rule will be added to the translation to redirect the control flow to the former thread s execution In the following sub paragraphs we will explain every sub procedure individually and use the first instruction stmt form to describe the syntactic form of statement stmt Furthermore it is necessary that in translating the guards facts from the state are not removed there
83. Server learns C here ISessions gt contains C SessID Jz Al secrecy_goal secret_SessID Actor C SessID Sessions gt add C SessID succ 0 new Thread Actor C SessID Sessions The Thread s Actor is the same as for the Server body all sessions are with the same server ch_server gt confidential_to server ch_server gt authentic_on server iknows 0 4 workaround should not be needed ServerSessions new Server server ServerSessions any C Session C server ch_server where C server any C Session C server ch_server where C server In analogy to the client authentication introduced above in 2 9 5 one could also model a variant for ACM as follows some unilaterally authenticated channel between the client and the server gets promoted to a fully secure channel by means of an explicit client authenti cation using some credentials FP7 ICT 2007 1 Project No 216471 A ANTSSAR SEVENTH FRAMEWORK PROGRAMME 3 D2 3 update ASLan specification and tutorial 88 190 3 ASLan concepts and syntax We have developed ASLan to achieve the following design goals e The language should be expressive enough to model a wide range of service oriented architectures while allowing for succinct specifications e The language should facilitate the specification of services at a high level of abstraction in order to reduce model complexity as much as possible e The language sho
84. _model CCM entity Environment symbols client server agent entity Session C S agent entity Client Actor S agent symbols Nc Ns text body Nc fresh Actor gt S Actor Nc S gt Actor Ns assert finished false F entity Server Actor agent symbols C agent FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 68 190 Nc Ns text body gt Actor C Nc Server learns C here Ns fresh Actor gt C Ns body of Session new Client C S new Server S body of Environment new Session client server Note that the server learns the name of the client on reception of the first message This is why in the receive statement gt Actor C Nc the sender side is marked with the dummy pattern and the agent name of the client C is prepended by to indicate that this value is received as part of the message sent by the client 2 8 2 ACM For the ACM we have recently introduced named channels at ASLan level The ASLan translator does not support this feature yet but we aim to add support for it soon At this point we present an illustrative example on how these named channels would be used when defining ASLan models In the ACM the example from the previous section would look as follows specification ACM_example channel_model ACM entity Environm
85. _set IID contains C secrecyGoalName_set IID secret Token secrecyGoalName secrecyGoalName_set IID state Actor IID where A B and C are the entity parameters corresponding to the set of agents specified in the secrecy goal IID is the instance ID of E and IID is the instance ID of its parent entity E Note that here A usually has the value of tA and similarly for B and C but they may have changed in case the entity parameters have been assigned to in the meantime On the ASLan level the secrecy goal is stated as an LTL goal over the secret predicate forall M P As O Csecret M P As amp iknows M gt contains i As Informally the meaning is that if a certain message M is a secret shared between a set As of agents and the intruder knows M then the intruder must be part of the set As of agents Note that this is possibly too strong if among the members of As there is a dishonest agent that is not the intruder itself For such cases spurious attacks can be avoided by the ASLan modeler stating just before any agent in As is declared dishonest select on child IID IID secrecyGoalName_set IID gt add i where the IID variable must be declared of type nat 4 13 Assignment of numbers to step label terms This phase of the translation generates and uses numbers for the step labels in the state facts of entities This is done because even for an relatively small number of
86. a high level protocol but for many applications result in a system so complex that it would be infeasible for automated verification The better way is using our channel notations for CCM ICM and ACM but special care must be taken to capture all relevant properties of TLS 2 9 2 HTTP Request and Response Pairing Let us first consider one of the most frequent application protocols that are run on TLS namely HTTP We model first how to ensure the correct pairing between requests and responses the client generates a nonce and sends it to the server along with the payload and with its own name such that the server knows whom to respond to The client then waits for a reply from that server containing the same nonce This is sketched in the following model fragment It shows how to model a very basic client server request response message exchange entity Client Actor S agent PayloadC lt gt Nc fresh generates nonce Actor gt S Actor Nc PayloadC S gt Actor Nc PayloadS checks nonce FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 71 190 entity Server Actor agent while true select on gt Actor C Nc PayloadC 1 learns C here PayloadS lt gt Actor gt C Nc PayloadS reflects nonce Since we use insecure channels with an intruder between client and server this is com pletely open to attacks 2 9 3 Se
87. above form can be replaced by single transitions of the form PF NF states C 4V R stategn or PF NF states C SV gt R stategm Redundant guards A transition rule is considered to be a redundant guard if PF NF C C true false V and R Intuitively this means that the transition does not change the state except for moving an entity from one step label to another and additionally the transition is guarded by a guard which is either always true either always false Such transitions can be written as states true gt stateg true or states not true gt states Such redundant guards can be introduced by the translation procedure when entering branches guarded by expressions which can be reduced to the logical constants true or false Transitions of the form states not true gt states can be eliminated if there exists no other transition taking the entity out of states It can happen that after dropping such a transition other transition rules will become unreachable in which case they can be also eliminated Transitions of the form states true gt stateg true are equivalent to empty transitions and can be eliminated under the same conditions as empty transitions 4 15 2 Merging of transitions Following the notion of step compression explained in 4 14 a second level of optimization is introduced Instead of generating the transition rules with the state facts and leaving the handling of atomicity
88. als any LTL formula can be given Free variables i e those not declared in the given entity nor inherited from any outer entity are implicitly universally quantified 3 9 2 Assertions Assertions are given as a statement in the body of an entity They are like invariants except that they are expected to hold only at the given point of execution of the current entity instance 3 9 3 Channel goals A channel goal has the form name _ Sender Channel Receiver A ANTSSAR FP7 ICT 2007 1 Project No 216471 a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 107 190 Symbol Explanation gt confidentiality gt authenticity and directedness gt gt authenticity and directedness plus freshness gt authenticity directedness and confidentiality gt gt the above plus freshness Table 7 Channel goal symbols in ASLan where the goal name is augmented with a parameter placeholder _ to indicate that in sub entities the goal name will appear again in the form of a goal label with a message term as its argument Similar to the syntax of message transmission Sender and Receiver can be real names or the pseudonym notation and Channel is a symbol for the kind of channel used For instance the goal of implementing TLS without client authentication to send a suitable payload message is Client gt Server A channel goal is usually stated at the l
89. also must be au thentically from Alice as otherwise an attacker can substitute Alice s reference by his own and trick Bob into using the attacker s set instead This attack you may provoke if you send the reference without ensuring authenticity removing the left to the gt in both Alice and Bob Please try it As usual with global variables the modeler needs to explicitly deal with synchronizing the access to sets shared using references If the modeler intends that Alice creates a set and that Bob should access after the reference to the set has been passed to Bob then the modeler should devise a proper synchronization mechanism Here before manipulating the set any further Alice should wait for an acknowledgement from Bob stating that he has finished accessing the set To this end in the above example we use of the constant message signal Note that the goal no_alarm could be violated if the signal was not sent over an authentic channel FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 60 190 2 5 3 Concatenated elements An further approach for communicating a set between agents is to send a copy of the set by concatenating all its elements This is comparable to marshalling and un marshalling pa rameters for remote procedure calls This approach is less efficient than the ones introduced above but allows for loose coupling of the agents without sharing memory of any kin
90. ample of how the reference method of set communication works may look as follows specification Sets_Sent_As_Reference channel_model CCM entity Environment symbols a b agent el e2 signal message setref message set message entity Alice Actor B agent symbols Seti message set body Seti fel e2 Actor gt B setref Seti FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 59 190 B gt Actor signal assert no_alarm Seti gt contains e2 entity Bob A Actor agent symbols Set2 message set body A gt Actor setref Set2 if Set2 gt contains e2 Set2 gt remove e2 Actor gt A signal body new Alice a b new Bob a b Note that in this specification Alice sends the set Set1 to Bob by passing the reference to the set namely setref Set1 After receiving the reference Bob removes the element e2 from the set This operation is visible to Alice That is the assertion no_alarm within Alice is not violated e2 does not belong to Set1 anymore when Alice checks it It is worth mentioning that in order to prevent the attacker from manipulating the set Alice sends the reference to the set to Bob both confidentially and authentic Actor gt B setref Set1 It must be confidential because if the attacker can read the reference the attacker may read and manipulate the set However it
91. and tutorial 121 190 4 ASLan semantics In this section we give a procedure for translating ASLan specifications into ASLan specifications This procedure therefore defines the semantics of ASLan in terms of ASLan and serves as a basis for the implementation of the translator which we call the ASLan connector described in 6 4 1 We provide a high level overview of the translation procedure which consists of a number of steps each focusing on different aspects of the mapping from the feature rich process based ASLan into the rewrite based ASLan The first step of the translation takes care of file imports and macro unfolding and the like This phase is known as the preprocessing phase and is described in 4 1 Next we have the static part of the specification that is everything that is not code is translated This translation step covers entities 4 2 types and symbols 4 3 clauses 4 4 equations 4 5 and security goals 4 12 Some preliminaries for the translation of code sections are described in 4 6 for control flow and in 4 14 for compression Then the code sections are translated in three sequential phases e translation of statements and guards described respectively in 4 7 and 4 8 where the rewrite rules for the ASLan specification are generated although in a temporary form allowing for ASLan terms e translation of terms 4 9 applied to the rules generated
92. annel without client authentication one can simply use Client gt Server M for a message M from the pseudonymous 38 This new ACM channel syntax is going to be supported by the translator soon FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 101 190 OO style notation Annotated channels notation ActorP gt send B M ActorP gt B M ActorP gt receive B M B gt ActorP M ActorP gt send B M over authCh ActorP gt B M ActorP gt receive B M over authCh B gt ActorP M ActorP gt send B M over confCh ActorP gt B M ActorP gt receive B M over confCh B gt x ActorP M ActorP gt send B M over secCh ActorP gt B M ActorP gt receive B M over secCh B gt ActorP M ActorP gt send B M over fresh_authCh ActorP gt gt B M ActorP gt receive B M over fresh_authCh B gt gt ActorP M ActorP gt send B M over fresh_secCh ActorP gt gt B M ActorP gt receive B M over fresh_secCh B gt gt ActorP M Table 1 Channel notations in ASLan for CCM and ICM OO style notation Annotated channels notation Actor gt send B M over ch Actor ch gt B M Actor gt receive B M over ch B ch gt Actor M Table 2 Channel notations in ASLan for ACM Client to the Server where either one of the end points is replaced by Actor This does not give all protections of TLS bu
93. anslation a fresh state predicate in the ASLan section signature The new predicate will be pa rameterized with respect to a step label an instance ID to uniquely identify every instance parameters and variables of the entity and will yield a fact Parameters are treated ex actly like local variables except that they are initialized at entity instantiation The state predicate has multiple purposes e record each instance of the entity e express the control flow of the entity by means of the step label e keep track of the local state of an instance namely the current value of its variables and will be used later in the generation of rewrite rules for the translation While such facts store the values of parameters and other variables local to the given instance of an entity these may be accessed read and written by children entities as well In these cases we will refer to the owner of a variable as the parent ancestor instance that declares this variable locally and therefore has the variable stored in its state fact By convention the state predicate for an entity E has the name state_E and will always have the first three parameters of fixed types and meanings as follows FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 123 190 The first parameter will be of type agent or a subtype of it and will represent Actor i e the agent who is playing the role of the
94. ar aslanpp connector jar TLS aslan ar TLS atk Online you select your model checker of your choice upload TLS aslan set the required options and execute the model Using ACM we can specify explicitly and very naturally that all payload messages among the client and the server are transmitted over the same pair of channels by the following variant of the above model The channel pairs are reflected by the functions noninvertible ch_c2s text channel client to server noninvertible ch_s2c text channel server to client that for any session ID yield a channel from the client to the server or vice versa respectively Using these functions we can dynamically create for each new session referred to by a fresh value stored in the variable SessID a new pair of channel names and the corresponding channels These channels are assumed to be confidential and authentic in both directions which we indicate by introducing the following facts bilateral_conf_auth ch_c2s SessID ch_s2c SessID Actor S For initiating a new session we use a unique public channel provided by the server ch_server channel public initiation ch of server where transmissions are confidential to the server and authentic at the server side 24 For more information on connector and model checker options please see Appendix B FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 85 190 ch_server gt con
95. at 7 7 Es 0 m i Fo O iff there exists j with 0 lt j lt i such that 7 7 Ho 0 m i Ulo Y iff there exists j gt i such that 7 7 o Y and r k o 0 for all k such that i lt k lt j m i Slo Y iff there exists j with 0 lt j lt i such that 7 7 Fs Y and m k o 0 for all k such that j lt k lt i 7 1 Es exists x iff there exists t Ty such that 7 1 Fofe a O The semantics of the remaining connectives readily follows from the following equiva lences and 4 not or not not w implies Y or not Y G not F not d R o V not U not 4 not 1 H 4 not O not 4 foral1 x 4 not exists x not Given an ASLan specification let be the set of all LTL goal formulas and Y1 Um be the set of LTL formulas occurring in the constraints section Let WV FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 176 190 be and w and Wm and be and G not attack and and m The ASLan specification is valid if and only if is valid on m under o w r t H under the as sumption Y in symbols m 4 implies W Dd for all interpretations o V gt Ty and all initialized paths 7 where H is the set of clauses defined in the specification Note that for the validity of a specification it makes no difference whether the constraints Y are interpreted as written ab
96. ata can be used without further ado in this and all enclosed sub entities FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 48 190 Things become a bit more involved when data may change over time and thus needs to be stored in a variable Here we show three methods of dealing with this global variables facts and shared sets used e g as global databases 2 4 1 Global variables A standard method is similar to the style using global constants mentioned before in the introduction to this section The shared variable is declared in an outer entity and may be used in any inner one See the following example verbatim Modifiable shared variable by inheritance clatse nb 2 ofmc NO specification SharedVariablei_Unsafe channel_model CCM entity Environment symbols succ nat nat entity Session A B agent symbols SharedVar nat entity Alice Actor B agent body SharedVar succ SharedVar this refers two times to the inherited shared variable does not work for OFMC Actor gt B i just an authentic signal to B entity Bob A Actor agent body 4 A gt Actor i assert test_SharedVar_still_1 SharedVar 1 should report violation because now shared SharedVarld succ i holds FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 49 190 body SharedVar
97. ate ASLan specification and tutorial 55 190 Actor 0 gt lt A 1 gt n7 Nonce A 1 gt lt Actor 0 gt n5 Nonce You can see nicely that both Alice and Bob see the same contents of SharedDB and that manipulations of either of them are immediately visible to the other party Synchronization of database access is the responsibility of the modeler 2 5 Set communication Since in ASLan one cannot send or receive sets directly we focus in this section on the different approaches to communicate sets between entities 2 5 1 Shared set variables and synchronization A simple way of communicating sets among entities in ASLan is to declare the sets as shared global variables This resembles the shared memory communication model in distributed computing The burden of synchronizing access to the shared sets is however left to the modeler We explain this method using a small example A more detailed example can be found in the ASLan specification of the Public Bidding scene 7 4 1 Suppose Alice and Bob wish to communicate a set The set is created by Bob and then Bob asks Alice to modify the set Alice then notifies Bob that she is done with her changes before Bob accesses the global set again specification SetsGlobal channel_model CCM entity Environment symbols syncil sync2 message a b el e2 agent SetGlobal agent set entity Alice Actor B agent 4 body B gt Actor syncl if S
98. ation and authorization the client sends along with his login message a password which is checked by the server Every client that sends a correct password is assumed to be authorized We model the passwords as shared secrets between a user and a server the most conve nient way to achieve this is to globally declare a function that maps every pair of agents to their shared secret nonpublic noninvertible password agent agent text This function is not public of course because the passwords are secret Every participant simply initially knows all passwords that it is involved in This allows us to model dishonest users and servers To model dishonest users we add the intruder knowledge facts iknows password i S intruder knows its own password for every server S We model the knowledge of dishonest servers as well iknows password C i dishonest server knows client passwords for every client C We do not discuss issues like weak passwords or password change protocols since we do not want to complicate things in this example If we want to model the credential handling more explicitly we might let the server make use of a credentials database in form of the server s session database which may contain also information on the authorization of clients how to model a database we have already seen in previous examples specification TLS_client_auth_CCM channel_model CCM entity Environment symbols login ok text nonpublic
99. ator for sets Consequently we must proceed somewhat more circumstantial to provide a set copy functionality and a ForAll operator FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 43 190 ForAll If we want to perform some action for all elements in a set and do not need to retain the set as such we can proceed as follows while MySet gt contains E perform the action for E MySet gt remove E Here we iterate though all elements Each element processed is simply removed from the set until the set is empty and all elements have been processed Copy If however we need to retain the original set we must copy the set either before or while iterating through it and performing the desired actions on the elements To copy all elements of a set into another set and still retain the original set of elements requires some organization as shown next MySetCopy 1 point to a fresh location MySetBackup 4 transfer elements to both MySetCopy and MySetBackup while MySet gt contains E MySetBackup gt add E MySetCopy gt add E MySet gt remove E move back the elements from MySetBackup to MySet while MySetBackup gt contains E 4 MySet gt add E MySetBackup gt remove E We first prepare two new locations for the elements one for the required copy and one for a backup of the elements of the original set Then we iterate throug
100. ay manipulate generate suppress delay reorder replay and divert arbitrary messages FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 11 190 Figure 2 The Sequence Chart for the NSPK Protocol However the attacker knows no keys unless they are disclosed to the attacker and he of course knows his own keys and in general cannot break cryptography e g he cannot un hash a hashed message An attacker may act using several different pseudonyms who all share the same knowledge The model checkers automatically simulate an attacker This attacker systematically tries to exchange messages with the lawful protocol parties following and corrupting the intended protocol message flow at will The attacker reads messages and impersonates honest parties The attacker may even exploit several simultaneous protocol sessions for instance by relaying messages from one session to the other session and vice versa The model checkers try automatically to evaluate every possible situation However complexity increases with every involved party and especially with every additional simultaneous session This may cause the model checkers to require a long time for evaluation Sometimes a model checker may even be overwhelmed by the problem complexity Therefore we must be careful about the number of involved parties and parallel sessions we request to be simulated 2 1 3 Formalizing Behavior
101. between client and server In other words the TLS channel is effectively upgraded to bilateral authentication Note that here and above we do not exclude the case of dishonest clients or servers e g we will include also the case that an attacker is a registered client at some server with his own username and password Note also that more complex matters may be attached to a login such as an access control policy based on user names FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 76 190 In order to model client authentication and authorization upon receiving a request from a prospective client for using a certain service the server should check an abstraction of the identity of the client and authorize the service use To this end the server needs to have a policy indicating which clients it is willing to serve and which credentials these clients have to supply We might model the authentication of the client with a challenge response protocol when the client requests a service the server sends a challenge that the client must correctly react to We could also use certificates at least for the server party where like above in the NSPK variant with certificates see 2 1 7 the peer checks if the party s certificate has been signed by some trusted authority Here extending the example given in 2 8 1 for simplicity we model a very basic and classic form of client authentic
102. c Select the output format and it s level of verbosity The default value is if and choices are Standard output format from the Avantssar project Standard output format from the Avispa project Same as if but also shows the protocol specification as it was understood Same as if but show things exactly as they were analysed i e after simplification Shows a quick view of the attack trace if any Shows an even more concise view of the attack trace and analysis result Write the attack to file atk string Output directory to use with out Do not simplify the input file complete trace Try to replace hashing by tokens slower or faster depending on the protocol Default for IF Do not try to replace hashing by tokens slower or faster depending on the protocol Default for ASLan Print more output informations same as of if Do not analyse only write the specification as it is Number of column in the output default 80 Benchmark output format very concise Expect AVANTSSAR s ASLan in input use ASLan for output Expect AVISPA s IF as input Not default anymore Level of protocol rebuilding see explanation above When an attack is found store the current state in a state file Create a directory with the spec s name and fill it with more than 300 sub state files so that many different instances of Cl AtSe can analyse them in parallel Choses a strategy for Horn claus
103. can utilize Horn Clauses to model recursion In this section we give an example of specifying a simple Role Based Access Control RBAC system with role hierarchy by using Horn Clauses Consider a file server which allows any user to read any file and any admin inherits the rights of a user and additionally may write files That is the RBAC system consists of two roles namely user and admin with admin gt user This scenario can be modeled using Horn clauses in ASLan can_write X forall Y can_write X Y is_admin X can_read X forall Y can_read X Y is_user X role_hierarchy X is_user X is_admin X We specify a file server with the RBAC system described above Note the use of explicit facts add_user and add_admin serve to introduce these rights as opposed to implicit facts is_user and is_admin see also 3 5 specification RBAC channel_model CCM entity Server 1 symbols Datum message FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 65 190 alice bob eve agent is_user agent fact is_admin agent fact add_user agent fact add_admin agent fact can_read agent message fact can_write agent message fact discloses_to agent message fact clauses write_right X forall Y can_write X Y is_admin X read_right X forall Y can_read X Y is_user X role_hierarchy X is_user X i
104. cations This procedure serves as a basis for the implementation of the ASLan con nector translator tool integrated into the AVANTSSAR Platform We conclude the main document in 5 In Appendix A we give a complete description of ASLan Appendix B gives a brief overview on the options of the ASLan connector and the various model checking back ends FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 9 190 2 ASLan gt tutorial In this section we aim to give a gentle introduction to ASLan to beginners We demon strate at small examples starting with the well known Needham Schroeder Public Key NSPK Protocol how to write specifications that can be successfully translated and checked using the back ends We give a number of practically important general hints and tricks and then provide and explain a number of useful typical specification patterns used e g in the AVANTSSAR Library 7 of industrial use cases The examples include set operations like union and intersection as well as checking properties like set inclusion and emptiness We introduce various approaches to handle shared data and to communicate sets in ASLan Moreover we demonstrate how to model a simple timeout mechanism a basic hierarchical Role Based Access Control RBAC system and various aspects of TLS style communication channels For each of these examples we give a complete ASLan model that can be
105. cedure is applied using the secret pred icate available in ASLan It has the following signature secret message protocol_id agent set gt fact ln the translation lt gt request B A P M IID IID IID is simplified to request B A P M IID IID IID which is equivalent because request facts are stable i e they are never retracted FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 158 190 The protocol ID is derived from the name of the secrecy goal while the message value is taken from the translation of the term which in our example is Token For rendering the set of agents the procedure for translating set literals described in 4 9 is applied as if the agents were specified using a set literal A new function symbol is introduced for the set The function symbol is parameterized by the instance ID of the parent entity E and has the type agent set The name of the function symbol is derived from the name of the secrecy goal by appending the suffix _set The signature of the function symbol is therefore secrecyGoalName_set nat gt set agent The membership of each agent to the set is stated using the contains predicate The following transition rule is generated within entity E child IID IID state_ Actor IID gt child IID IID contains A secrecyGoalName_set IID contains B secrecyGoalName
106. cent protocols and services which often assume for their proper functioning that communication is carried out over secure confidential and or authentic channels This issue is discussed in detail in Deliverable D3 3 Attacker models 2 ASLan natively supports various channels models as described in 3 8 We have opted for ASLan to be an extension of IF with Horn clauses and LTL because in that way ASLan is expressive enough that many high level languages can be translated to it Moreover defining ASLan as an extension of IF made it possible to extend the suite of tools provided in AVISPA rather than building new tools from scratch aiming thus at an already stable and effective tool support A 2 ASLan Syntax A 2 1 Grammar in BNF We first present the entire ASLan syntax in BNF with the usual conventions The grammar has two start symbols Prelude and ASLanFile Intuitively the prelude file contains all declarations that are service independent while the ASLan file contains only service specific declarations An example of a prelude file in ASLan is given in 3 13 The symbol for comments is both for ASLan and in the BNF below Prelude TypeSymbolsSection SignatureSection TypesSection EquationsSection FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 169 190 IntruderSection ASLanFile SignatureSection TypesSection InitsSection ClausesSection RulesSection
107. client uses a sequence number for each message which the server checks against its session database We model the sequence numbers in ASLan as terms of the form succ succ succ 0 of type nat An introduction on how to model a shared database has been given in 2 4 3 This example contains a single but multi threaded instance of the server A client requests a new session using a fresh session identifier by starting with message sequence number 0 recognizes a new session by the session identifier being unknown and the message sequence number being 0 The server then enters the new session into its session database and spawns a new thread handling that session The thread only accepts messages from the same client C that initially contacted the server using the same session identifier and a suitable consecutive message sequence number Thus a client may have several simultaneous sessions with the server each being handled by a different thread In this model unlike in the ones before we make use of the full power of channel assump tions regarding bilaterally authenticated channels and thus can simply assume that the client is authenticated to the server The server accepts requests for a new session by any client During a session the server will need to recognize the same client and the corresponding session such that the reply and all further communication in this session will be with the original client To implement this in CCM we
108. compositionality aspect behind channels mentioned below 3 8 1 Channel models For channels as assumptions we currently support three different channel models ACM CCM ICM see 2 as described in the subsequent sections All our channel models are based on certain events in the system execution trace implementing unidirectional message based communication from a single sender to a single intended receiver Abstract Channel Model ACM In ACM a channel is referred to by a name and provides a communication link relating all messages sent and received using this name The assumed properties of a channel are declared as LTL constraints over explicit send and receive events usually with the help of a set of predefined fact symbols Cryptographic Channel Model CCM In CCM channels are realized by individual transmission of messages via the Dolev Yao style intruder Multiple transmissions may be related using pseudonyms and user defined identifiers Assumed security prop erties are defined via concrete implementations like certain ways of encrypting or signing messages Ideal Channel Model ICM Like CCM the ICM focuses on individual message trans fers In contrast assumed security properties of channels are described by abstract fact symbols and special transition rules that model the intruder s limited ability to send and receive on those channels FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan sp
109. constant Similarly user defined functions are by default invertible in each argument as long as their result type and the respective argument type are subtypes of message or of some set type which means that the intruder can derive the arguments of a function call when he knows its result To avoid this default behavior the keyword noninvertible must be given before the function name when declaring the function The special function symbol iknows which is used to describe the knowledge of the intruder may also be used to describe special cases of invertibility For instance to specify that the intruder can invert the function f in its first argument one can write the following Horn clause involving iknows facts iknows_f1 X Y iknows X iknows f X Y Equations are used to define algebraic properties e g the property of exponentiation that exp exp g X Y exp exp g Y X is necessary for Diffie Hellman based key exchange They are only allowed at the root level i e in the outermost entity and thus are global All variables occurring in them are implicitly universally quantified 3 7 Terms Terms may consist of variables e g A constants e g b2 function applications or to be more precise function symbols applied to first order terms e g hash Msg and message concatenation tuples e g A b2 0 which are right associative and set literals e g A B C Terms as well as variables on the left hand side of assign
110. cret_Nb is concretized for Nb Besides Bob only A may learn of it Neither party may disclose Nb to any other party and it must of course be secured in transmission The equivalent applies to A s nonce Na as stated in secrecy goal secret_Na in line 11 The authentication goal Alice_authenticates_Bob in line 9 is concretized for the mes sage transmission of Na from Bob to A Bob s goal is to let A authenticate him via the reflection of Na The equivalent applies to Bob s nonce Nb that Bob expects to let him authenticate A on when she reflects Nb to him in line 10 Specified here as only at this point Bob finally feels confident about A s identity Before Bob could also have been talking to an attacker FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 21 190 The goal labels of a channel goal are written on both communication endpoints immedi ately in line the corresponding communication event the goal refers to The goal labels of a secrecy goal are also specified at each entity that share the secret value and as soon after generation or reception as possible The resulting redundancy i e duplication among the various knowers is intentional in order to fully capture also the cases where part of these parties are played by the intruder The complete ASLan Model In ASLan the complete protocol reads as follows where comments in ASLan as usual start with
111. ction rules for their analysis An alternative specification of analysis using algebraic equations is not considered here The agent constants i and root denote the intruder and the root entity instance respec tively The term pk A is used to denote the canonical public key of an agent A The type public_key is a subtype of type agent for convenience in models involving pseudonyms The term defaultPseudonym A IID stands for the default pseudonym of the agent A and entity instance IID i e when using pseudonymous channels without specifying a particular pseudonym The use of the instance ID is simply to use a fresh pseudonym for each instance of an entity that one plays in Note that the Horn clause analysis_sign is precise only for RSA like signatures where the signed part can be recovered by applying the public key For other signature implemen tations e g ElGamal it is too pessimistic in the sense that it may lead to false attacks because in general one can not recover M from sign inv K M Moreover in case M is the FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 120 190 hash of the actual payload with suitable padding e g following state of the art standards like PKCS the Horn clause is not helpful in the sense that knowing the value of M has no use apart from verifying the signature FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification
112. ctural con straints on terms These are mainly used for emphasizing the structure of messages sent or received This is also very helpful for the performance of SATMC For example a variable declaration X crypt public_key agent message is expanded to a set of declarations X1 public_key X2 agent X3 message and every occurrence of the variable X in a term is replaced by crypt X1 X2 X3 A compound type f T1 T2 where f has result type T is regarded as a subtype of T A compound type using the tuple constructor like T1 T2 is equivalent to T1 T2 Both forms of denoting a tuple type have higher syntactic precedence than general compounds and concatenation compounds The symbols section is used to declare constants and functions The names of symbols must be unique i e overloading is not permitted Macros are used to shorten and simplify recurring terms The function or constant name on the left hand side must not be declared in the symbols section or inherited from any enclosed entity FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 95 190 User defined symbols as long as their result type and all of their argument types are subtypes of message or of some set type are by default public which means they are known and usable by the intruder To avoid this default behavior the keyword nonpublic must be given before the symbol name when declaring the function or
113. cuted in that step together with the parameter values and makes references to the code line numbers in the ASLan file Once the model checker detects a security goal violation it stops model checking and under the heading VIOLATED prints out the violated security goal This is followed by a kind of core dump which lists all facts that are known at the time of the goal violation Here we have only EXPLICIT facts that have been introduced by declaring them fact explicitly for instance by instantiation of an entity or generation of a nonce As in our NSPK example we don t use horn clauses we have no IMPLICIT deduced facts The most interesting part of it however is the MESSAGES section with its compact message sequence chart like attack representation at the very bottom of this listing Wit 1 gt lt i gt n7 Na Wit 1 _pk i lt gt gt Req 1 n7 Na Wit 1 _pk Req 1 Req 1 gt lt Wit 1 gt n7 Na n20 Nb _pk Wit 1 12For an example containing Horn Clauses please refer to 2 1 7 below FP7 ICT 2007 1 Project No 216471 A AN T SSAR D2 3 update ASLan specification and tutorial 28 190 Wit 1 lt i gt lt gt lt Wit 1 gt n7 Na Wit 1 _pk i Req 1 422 Na n20 Nb pk Wit 1 n20 Nb _pk i lt i gt Req 1 lt Wit 1 gt Figure 7 An AVANTSSAR Model Checker found a Vulnerability in the NSPK Protocol lt i gt gt Wit 1 n7 Na n20 Nb
114. cy predicate appears on the LHS of a rewrite rule this cannot mean retraction of the fact but its usage as a condition cf ASLan execution model A 3 2 A 3 ASLan Semantics A 3 1 Equalities All terms in ASLan including facts are interpreted in the quotient algebra T g where E is the set of algebraic equations declared in the prelude specification Thus in the following we consider two terms as equal if and only if this is a consequence of the algebraic equations To distinguish from syntactical equivalence of terms we write t s for two equivalent terms t and s Also we assume in the following that the type declarations of the ASLan file are satisfied in all substitutions of variables e g variables of type agent are only substituted for constants or other terms of type agent A 3 2 Execution model Let F be the set of ground i e variable free facts An ASLan specification defines a transition system M S T gt where S is the set of states Z C S is the set of initial states and gt S x S is the reflexive transition relation We assume that the states in S are represented by sets of ground facts i e S 27 If S S then we interpret the ground facts in S as the propositions holding in that state all other ground facts being false closed world assumption Z is defined by the InitsSection in the obvious way FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification a
115. d and given as return step label the step label for evaluation of the guard so that it will be reevaluated Ultimately the remaining statements are parsed Example 8 Consider the following loop while p q We will create one rule leading inside the loop if p is satisfied state BidM Actor IID s1 BP M p gt state BidM Actor IID branch sl 0 BP M p and another leading outside of the loop if instead p is not satisfied state _BidM Actor IID s1 BP M not p gt state _BidM Actor IID succ sl BP M Parsing the inner statements of the loop we will obtain the following rules state BidM Actor IID branch sl 0 BP M gt state_BidM Actor IID succ branch sl 0 BP M q state_BidM Actor IID succ branch sl 0 BP M gt state_BidM Actor IID s1l BP M O FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 148 190 4 7 11 Select Select stmt rest sl return_sl stmt select on Guard_1 Stmt_1 on Guard_g Stmt_g ipn for i from 1 to g p_1 p_n positiveGuards Guard_i apply adaptGuard to p_1 p_n positive branches only i e Guard satisfied for j from 1 LHS state state RHS state state add LHS p_j to section to n fact for this entity with step label sl facts for the owners of variables appearing in p_j fact for this entity with step label branch sl i facts for the owners of variables appear
116. d thus not incurring any synchronization problems The sender first transforms the set to be sent into a complex message containing a concatenation of the elements of the set That is in order to send a set S A1 An we send the message SMsg A1 A2 An where denotes the concatenation operator In the following example Alice communicates the set NatSet 1 2 3 4 to Bob specification Sets_Concatenation channel_model CCM entity Environment symbols a b agent nil message box message message entity Alice Actor B agent symbols NatSet NatSetBackup nat set E nat NatSetMessage message body NatSet 1 2 3 4 NatSetBackup point to a fresh location NatSetMessage nil empty preserve elements in NatSetBackup while NatSet gt contains E NatSetMessage E box NatSetMessage NatSetBackup gt add E NatSet gt remove E move back the elements from NatSetBackup to NatSet while NatSetBackup gt contains E NatSet gt add E NatSetBackup gt remove E Actor gt B NatSetMessage FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 61 190 entity Bob Actor A agent symbols BNatSet nat set BE nat BMessage Rest message body A gt Actor BMessage BNatSet point to a fresh location while BMessage nil se
117. d and receive terms obtained by replacing the predicates with the corresponding encoding for the CCM In the translation table the following auxiliary symbols are used where the type slabel stands for security label atag slabel 4 authentication tag ctag slabel confidentiality tag stag slabel security A C tag iknows message gt fact send receive on CCM or unprotected ICM channel ak agent gt public_key noninvertible authentication key function ck agent gt public_key noninvertible confidentiality key function FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 137 190 ASLan predicate ASLan translation for CCM A gt send B M iknows M A gt receive B M iknows M A gt send B M over authCh iknows sign akP A atag B M A gt receive B M over authCh iknows sign akP B atag A M A gt send B M over confCh iknows crypt ckP B ctag M A gt receive B M over confCh iknows crypt ckP A ctag M A gt send B M over secCh iknows crypt ckP B sign akP A stag B M A gt receive B M over secCh iknows crypt ckP A sign akP B stag A M Table 8 Translation from ASLan to the CCM In the ASLan term pattern in the left hand column of the table A stands for Actor or any pseudonym of it i e Actor or Actor _ P for any P
118. d by the following rule hc f_invertible i M1 Mn iknows Mi iknows f M1 Mn where again the M are variables of type 7 respectively Note that most functions are typically public i e everybody can apply them to known terms To be on the safe side user defined functions are by default invertible This makes sense at least for message constructors which can be seen as operators in the free term algebra Few other functions are invertible for instance pair and inv in the prelude inv is an example of an invertible function that is not public 4 4 Translation of Clauses Although each clause is declared inside an entity it should be applicable globally if it does not refer to local variables including parameters of the entity or any enclosing ones Otherwise the clause will be applicable locally being inherently bound to the variables it refers to which might belong to the entity as well as to its ancestors Translating the clauses is therefore adjusted so to preserve this binding For each of the entities whose variables are referred to by the given clause we add to the conditions of the clause their state fact This means that if in an entity E we have a clause h A A 1 amp A_n such that if V is the intersection between the variables in the scope of E and the variables in A A_1 A_n and fo_1 o_m is the set of owners of the variables in V we add to the translation the clause FP7 ICT 2007 1 L
119. der cannot learn the contents of M sent on this channel Confidential channels do not however protect the message transmission against inter cepting messages and replacing them with different ones spoofing the intruder may introduce messages on the channel in the name of other parties disruption replay with CCM ICM or re ordering The behavior of a confidential channel can thus be thought of as an encryption with the receiver s public key e Ae eB denotes a secure channel from A to B in the sense that both end points are protected such that messages are transmitted authentically and confidentially All these kinds of channels can be considered also when one or both of the parties involved is identified by a pseudonym e g for sender and or receiver invariance as described in 2 4 1 4 For ACM there is the following abstract notation A gt B This notation denotes a communication between A and B over the channel ch The assumed properties of the channel ch can be specified using facts For doing so there is a set of predefined facts which are described along with their informal definitions in 3 8 3 Besides types of channels mentioned above we can consider further properties These are of interest for protocols such as TLS which additionally offers order preservation replay protection some limited protection against traffic analysis e g the number of messages sent and so on etc The following properti
120. e above example the sender is Alice the receiver is Bob and the enclosing role is Session The channel symbol arrow describes the property that the channel between the sender and the receiver is supposed to have for details please refer to Table 7 and 3 8 The agent term A occurring in the channel goal declaration must re appear as the actual argument given for the Actor parameter of the sending entity which in the above example is Alice and the agent term B must re appear as the actual argument given for one other parameter named B in the above example of the sending entity In this entity there must be a send statement that contains the given goal label The values of the two parameters Actor and B are evaluated when executing this send statement Analogously the agent term B occurring in the channel goal declaration must re appear as the actual argument given for the Actor parameter of the receiving entity Bob and the agent term A must re appear as the actual argument given for one other parameter named A in the above example of the receiving entity In this entity there must be a receive statement that contains the given goal label The values of the two parameters Actor and A are evaluated when the executing this receive statement The payload terms labeled with the goal name on both the sender and receiver sides indicate the value to the protected during transmission These terms may look different
121. e compression e If the transition enters a compressed section then only the right hand side is changed state_X MSGs IID facts conditions gt state X MSGs IID facts e If the transition is within the compressed section i e neither entering nor exiting it both sides are changed state X MSGs IID facts conditions gt state X MSGs IID facts e If the transition is exiting the compression section only the left hand side is changed state X MSGs IID facts conditions gt state _X MSGs IID facts Compressing the three step example above gives thus the following rules state_responder Actor IID 1 dummy_agent dummy_message iknows A gt state responder Actor IID 2 A dummy_message state responder Actor IID 2 A dummy_message exists N gt state responder Actor IID 3 A N state responder Actor IID 3 A N gt state_responder Actor IID 4 A N iknows N According to the macro step semantics introduced in A 3 5 a macro transition would not stop at the intermediate states that contain a state fact but continues with any applicable rule until reaching a state without a state fact and cannot apply any rule that does not change the state fact which guarantees that progress is made only in one process instance Note that in the above simple sequence of atomic actions as well as in many similar cases there is an equivalent compressed rule
122. e entity in place of its parameters a new fact state_BidM bm iid s1_0 bp dummy_message will be added to the state From now on this fact can be used to identify this particular entity via its instance ID iid the value of its variables M initially set to dummy_message to indicate that it is uninitialized and parameters Actor and BP here replaced by the terms bm and bp and its execution progress step label s1_0 O FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 124 190 As the above example shows this state fact stores all necessary information regarding the execution state of a particular instance of an entity in the system namely its instance ID its step label and the value of all its variables including also parameters Yet nested entities inherit these values from their ancestors meaning that variables of an instance are visible unless overridden to all its descendants Thus when an entity E refers to a variable of its ancestor A then it is A s state fact rather than E s that needs be used To this end in the following we will speak of the owner of a variable indicating the instance whose state fact contains the value of that variable While identifying which entity a variable belongs to can be done in the translation phase identifying the exact runtime instance depends on the execution of the system and can be done only by binding each instance to
123. e measures to copy it either before or on the fly as mentioned in 2 3 2 2 3 4 IsSubset and IsEqual IsSubset If we want to check whether one set is a subset of another set we can subtract the other set from that set and check whether the result is the empty set How to subtract one set from another we have just described in 2 3 3 How to test a set for emptiness is detailed above in 2 3 1 However we should take care to preserve the original sets carefully as nobody will expect a query operation like this to modify the sets in question Including optimizations like making a backup while checking for the subset property this might look as follows nonpublic isSubset fact locally declared auxiliary fact MySetBackup 1 provide a fresh location isSubset initially assume the subset property MySeti gt isSubsetOf MySet2 while MySet1 gt contains 7E amp isSubset if MySet2 gt contains E retract isSubset if isSubset MySetBackup gt add E MySet1 gt remove E move back the elements from NatSetiBackup to NatSet1 while MySetBackup gt contains E MySet1 gt add E MySetBackup gt remove E After this if the fact isSubset still holds we have checked that MySet1 is a subset of MySet2 By restoring all elements from MySetBackup to the original location in MySet1 we have preserved the original set and thus the validity of the tested set property As said already this wor
124. e of course you may not do You may not re assign a different location to the local parameter This for instance Bob would do by stating SetGlobalB e1 e2 Just imagine what would happen if in a C function you get passed a parameter containing a pointer and then plainly ignore the pointer by assigning a new pointer to the variable In the previous example however assigning a new set location to a global variable does not cause a problem as the changes are visible to all partners 2 5 2 References We can communicate sets among agents in ASLan by passing references to the sets This method should however be used with caution because of aliasing For instance if a reference to a set S which is stored locally at A is passed to B then B can directly read and manipulate S from the moment he receives the reference In particular if A adds elements to S after sending the reference to S to B the added elements will be visible to B Similarly B can directly add or remove elements to S even though S is locally stored at A The modeler can think of the set passed by reference as if it resides at a global level hence being accessible to both A and B Obviously if the receiver B is dishonest the content of the shared set S will be readily available to the attacker We remark that A can always make a local copy of S and pass the reference to the copy to B so that B would not be able to directly manipulate or read the content of S A simple ex
125. e such transitions as PF NF states C SV gt R stateg where PF and NF are sets of facts and negated facts respectively states represents a state of an entity instance C is a conjunction of possibly negated atomic conditions R is the set of facts introduced by the transition the entity is taking states is the next state of the entity while V is a finite set of existential variables See A 3 2 for ASLan transition rules A transition rule is considered empty if PF 0 NF C V and R Informally this means that the transition does not change the state except for moving one entity from a step label to another Empty transitions can be written as states gt states Empty transitions are introduced by the translation procedure whenever a branch is exited An empty transition states gt states can be eliminated when it is the only transition that takes the entity from states to states and one of the following holds e there exists one or more other transitions that take the entity into state states so that we can write PF NF stateg C SV R states states gt stategn FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 164 190 e there exists one or more other transitions that take the entity out of state states so that we can write states gt states PF NF statesn C V R stategm In this case the existing chains of two transitions of the
126. eFact stmt rest sl return_sl An independent receive statement R i e a receive operation that has not been specified as a guard in an on part of a select statement is translated at first as if it appeared in select on R see 4 7 11 for details A send statement is translated at first like a fact introduction see 4 7 7 for details As described in detail in Deliverable D3 3 2 we have formalized different models of com munication and definitions of channels as assumptions or goals respectively In particular for channels as assumptions The Cryptographic Channel Model CCM here channels are realized by passing mes sages via the intruder where security is achieved by certain ways of encrypting and signing the messages e The Ideal Channel Model ICM here we have abstract fact symbols and special tran sition rules that model the intruder s limited ability to send and receive on those channels For instance he can see everything that is transmitted on an authentic channel but he can only send under any identity that he controls e The Abstract Channel Model ACM is at a similar abstraction level as ICM but here the notion of a channel is per session between two parties It uses named channels and explicit send and receive events that are constrained by LTL formulas over the traces We have shown in 2 18 that CCM and ICM are equivalent under certain realistic assump tions and we are working to obtai
127. ecification and tutorial 97 190 We have shown in 2 18 that CCM and ICM are equivalent under certain realistic as sumptions while the ACM operates at a different abstraction level than CCM and ICM We are working at establishing a formal comparison between the ACM and the CCM ICM establishing such equivalence results is fundamental as they allow us to use each model inter changeably according to what fits best with certain analysis methods A detailed comparison of the strengths of the different models is given in 2 4 while here we just summarize the main differences There are slight differences in the way ACM and CCM ICM are used to formulate the interesting channel properties and in terms of expressiveness and scope of the models In ACM the modeler can conveniently refer to channels via their names This allows for instance to disambiguate several channels between the same participants and to specify in a very convenient way that for several message transmissions the very same channel is used In CCM ICM if needed this can be simulated by the modeler by attaching channel names to the transmitted messages ACM has more freedom to specify assumed security properties via LTL constraints allows in particular for the definition of resilient channels which cannot be expressed in CCM ICM 35 An important feature of CCM ICM are the availability of compositionality results be tween channels as assumptions and channels as goals 18 2 w
128. ecification are available already within the enveloping entity we must use security goal templates For this we first declare a security goal template within the outer entity and then fill in the template within the inner One may wonder why Bob is given A as parameter by Session and then plainly ignores its value The reason for this is as follows The translator compiler from ASLan to ASLan needs to know with which agent variables inside the Bob entity the security goals given in the Session entity are connected Therefore we need not only declare the Agent parameter of Bob but also the A parameter standing for Alice although the value passed during instantiation of Bob is overwritten later on receiving the first message SEvery agent automatically is assigned a default public and private key pair Definitions are part of the ASLan standard prelude For details see 3 13 FP7 ICT 2007 1 Project No 216471 A AN T SSAR E SOO ANDOOKR WN FH D2 3 update ASLan specification and tutorial 20 190 entities after the missing parameters have been declared and the security goal is required to be met by the inner entity Let us look at our NSPK example Alice and Bob both want to require the two nonce secrecy goals and the two authentication goals to be met Thus we specify the security goals in the enveloping entity which is Session However Session cannot access the nonces that Alice and Bob will use as they declare them
129. ed by horn clauses between each transition Whatever the strategy used there are always systems of horn clauses that won t terminate and thus the modeler should make sure that the horn clauses in his specification terminate w r t the strategy used by the tool used for the analysis Bounding Execution A second very important point to be aware of is the option nb which controls the bound on the number of sessions used during the analysis Except for e g OFMC in non classical mode this bound is a need to ensure termination anyway The definition of sessions is controlled by the 1v1 option but whatever the definition of FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 185 190 114 session used the nb option defines the maximum number of times each transition can be run in a trace The default value is 1 and thus it is up to the modeler to correctly adjust this value depending on his specification For example if the specification does not use loops then the default 1 value should be fine if the specification uses loops but the maximum number of iteration is known in advance e g loops used to avoid writing the same transitions many times then a value sufficiently large must be provided to ensure that the specification can be run completely and if the specification uses loops in an unpredictable or infinite way then the problem is fundamentally
130. ed by including a unique identifier into the messages In addition to their use as assumptions slightly abusing the notion and notation of channels we also allow for channels as goals This is inspired by a compositionality re sult 18 The idea is that complementing security assumptions on which a system can rely when using channels one can also ask what properties a system ensures when aiming to realize a certain kind of secured channel In fact as shown in that paper when considering a fixed set of application messages being exchanged in the system modeled we can identify the goals for authentic and confidential channels as the classical authentication and secrecy goals 37 3 8 3 Channel syntax To express security properties of potentially pseudonymous channels we use and partially extend the notation we introduced in Deliverables D2 2 4 and D3 3 2 and recalled above While 16 uses the bullet notation to reason about the existence of channels we use it to specify message transmission in services in two ways e First as described in this subsection the modeler may use channel properties as as sumptions i e when a service relies on channels with particular properties for the transmission of some of its messages e Second the service may have the goal of establishing a particular kind of channel Details on how to specify channel goals are given in 3 9 3 37In fact this identification has shown a problem
131. ed into a bilateral one which is checked by the goal secure_transmission _ C gt x S for the payload For the sake of completeness we also check that the client s password is only shared with the server shared_secret _ C S The idea of the construction using a login over a secure pseudonymous channel where the client is not a priori authenticated is that the result is a secure channel i e we can run an application protocol such as a webmail application over this channel as if it was a standard bilaterally authenticated secure channel Such a compositionality result is shown in 18 provided that certain conditions between channel and application protocol are fulfilled so that they do not interfere with each other If the focus is the verification of an application protocol and not of a login mechanism it is recommended to directly model secure channels without pseudonyms and passwords transmission as done below in 2 9 6 Note that here we employ one symbolic session between any client C and any server S either of which may be the intruder We just forbid that the client and the server are the same agent in which case the client would talk to itself which would not make much sense The ACM variant given next follows the design of the CCM variant with the main difference being that for modeling the assumed weak client authentica tion instead of using a pseudonym we use the more abstract channel relation unilatera
132. edefined step label s1_0 standing for the default initial step label and the following functions which are total injective and have disjoint range e succ sl returning the successor for sl and e branch sl n returning the nth branch for s1 These two symbols are used only for presentation purposes For a realistic ASLan model the number of applications of these predicates would be too high and would unneces sarily increase the complexity of the generated ASLan translation Thus based on the two predicates numeric step numbers are generated and used in the translation See 4 13 for a description on how this is done 4 7 Translation of Statements We define here in pseudo code a procedure ParseCode that recursively parses a list of statements and generates equivalent rewrite rules as output Its arguments are the list of statements Stmts to parse the current step label s1 and a return step label for returning from a branch For ease of understanding the procedure will call different sub procedures according to the kind of the statement examined each of which is treated in a subparagraph ParseCode Stmts sl return_sl if Stmts stmt rest Stmts not empty stmt first statement rest remaining statements case stmt assign Assign stmt rest sl return_sl freshGen FreshGen stmt rest sl return_sl entityGen EntityGen stmt rest sl return_sl FP7 ICT 2007 1 L Project No 216471 A ANTS
133. een found during a model check Why Very often no attack is reported by a model checker because in the model not all statements can be executed Non executability of a model in this context means that not even under optimal conditions i e all participants are behaving as they should and no intruder is messing up things the protocol can be executed until the intended end if any of the system run The most frequent reason for non executability of a model is that a message sent by some party does not match with the message pattern expected by the intended receiver Then the intended receiver who is waiting for a different message blocks execution and the rest of the protocol may never be executed Incompatibility may result because of missing sub messages Also wrongly set parenthe ses such as M1 M2 M2 vs M1 M2 M2 which is implicitly parenthesized as M1 M2 M2 etc can easily cause non executability and are easily overlooked by human readers Even more subtle mistakes are type mismatches e g because the sender sends an agent name and the receiver expects a public key instead To help detecting such problems the ASLan output format OF provides an UNUSED section which shows any ASLan rules that were never used by the model checker during its analysis So far only CL AtSe supports this SATMC offers the e option for executability checking showing which rules can be executed and which not OFMC will soon offer a similar functional
134. either verify the certificate s validity range i e the time interval for which the certificate is valid nor its revocation state nor its intended purpose The complete ASLan Model The following listing contains the complete ASLan model for the adapted NSPK ex ample 14_ gt cert A PK is an example of a macro defined for better readability in the macros section of an entity The definition of that macro you can find below in the listing of the complete model For further details about macros please refer to 3 6 15The model checkers as we have said already can be fine tuned by various options either as command line options or as directives in the ASLan code of the model Here with clatse hc blr we give FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 34 190 NSPK with Public Key Certificates Horn Clause Use Case clatse hc blr satmc NO ofmc NO specification NSPK_Cert_Unsafe channel_model CCM entity Environment symbols Declare global symbols root_ca ca agent certificate authorities c agent agent used as fake CA trusted_agent agent fact trusted_pk agent fact issued message fact macros Macros improving readability A gt signed M M _inv pk A M Agent A signed M A sign inv pk A M M C gt cert A PK C gt signed C A PK Abstract certificate without details like validity period cert
135. el NONE NOPS LUMP Sets a certain optimization level Can be one of LUMP this is the highest level of optimization which means that the generated ASLan transitions are lumped together as much as possible NOPS this is an intermediate level of optimization which means that empty transitions and transitions that can never be taken are eliminated or NONE this disables any optimization The default value is LUMP orch orchestration client CLIENT_ENTITY_NAME Render the specified entity as an orchestration client The name of the specified entity is changed to OrchestrationClient and some extra symbols and transitions are added to the resulting ASLan specification pp pretty print Pretty print the ASLan specification Comments are lost during pretty printing This option is meant mainly for syntax checking specifications and for getting a compact view of large specifications so strip output If this flag is enabled then no comments and no line information will be generated in the ASLan specification This is intended for debugging purposes FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 181 190 v version Display version information In order for imports to work you must define an environment variable named ASLANPATH It should contain all directories where the translator should search for files to import It works similarly with the CLASSPAT
136. ent symbols client server agent ch_c2s ch_s2c channel entity Session C S agent Ch_C2S Ch_S2C channel entity Client Actor S agent Ch_C2S Ch_S2C channel symbols FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 69 190 Nc Ns text body Nc fresh Actor C_C25 gt S Actor Nc S C_82C gt Actor Ns assert finished false entity Server Actor agent Ch_C2S Ch_S2C channel symbols C agent Nc Ns text body Ch_C2S gt Actor C Nc Server learns C here Ns fresh Actor Ch_S2C gt C Ns body of Session new Client C S Ch_C2S Ch_S2C new Server S Ch_C2S Ch_S2C body of Environment ch_c2s gt confidential_to server ch_s2c gt authentic_on server new Session client server ch_c2s ch_s2c Two channels are defined ch_c2s and ch_s2c In the body of the entity Environment the channel ch_c2s is declared confidential to the server while the channel ch_s2c is specified as authentic on the server side Note that the channel identifiers like ch_c2s are now passed as parameters like Ch_C2S to the two sub entities and used there within the send and receive statements FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 70 190 2 9 Modeling TLS Like in the examples given so far unle
137. ential to b and weakly authentic and and ch_b2a is weakly confidential and authentic authentic for b with the additional requirement referred to as the link requirement that the principal sending messages on ch_a2b is the same principal that receives messages from ch_b2a This can be used to model a run of SSL TLS in which principal b has a valid certificate but principal a does not Table 5 Properties channel facts and their informal meaning If we want to define the channel ch_c2s as resilient we may simply add the following line to the body of the entity session line 41 resilient ch_c2s It could also be important to constrain the behaviour of different channels as done in the relation between channels defined in Table 4 By leveraging the elementary properties defined above it is possible to define more complex properties and channel relations approximating real world transport level commu nications such as SSL TLS better than possible using CCM see 2 9 5 and 2 9 6 like the ones given in Table 5 With reference to the previous example if we want to model a TLS transmission with out client authentication we may simply replace lines 43 and 44 with the following one unilateral_conf_auth ch_c2s ch_s2c server Another feature of the ACM is the possibility to use either the same or different channel identifiers for different sessions For instance with reference to the previous example a modeler can
138. entity to which the state fact is associated For the root entity instance its value is root e The second parameter will be of type nat and will represent the instance ID with implicit name IID For the root entity instance its value is 0 e The third parameter will be of type nat and will represent the step label Its initial value is s1_0 which is later replaced by 1 as defined in 4 13 Consequently if the ASLan root entity has the name Environment it the state predicate given in the initial ASLan state will be state Environment root 0 1 Any other parameters and local variables of the entity will be listed as parameters of the state fact after these special three parameters If the entity has an Actor parameter it will be assimilated with the first of the three special parameters just listed Example 1 Consider the following entity declaration for the Bid Manager in the Public Bidding model entity BidM Actor BP agent symbols M message a variable then the following state predicate is created state_BidM agent nat nat agent message gt fact in section signature in the translation The arguments of the predicate are an agent name for parameter Actor a unique instance ID of type nat created at instantiation a step label of type nat an agent name for parameter BP and finally a message for variable M At instantiation of the entity new BidM bm bp where terms are passed to th
139. eprocessing phase renamed all homonymous elements so to have globally unique names declarations of new types both basic and compound are immediately reflected in the ASLan file in section typeSymbols modulo minor syntactic adjustments FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 125 190 Symbols must be partitioned into variables constants and functions and then be tran scribed to section types the first two and to section signature the latter in the ASLan specification Their types are also immediately reflected except in the case of para metric types i e tuple and set where a more involved translation is required fully detailed in 4 9 Symbols can be declared using the modifiers nonpublic and noninvertible e If a symbol which may be a constant f T Tn T where all 7 7 7 are subtypes of message or of some set type is not declared as nonpublic it is considered public The semantics of being public can be defined by the following clause hc f_public M1 Mn iknows f M1 Mn iknows M1 iknows Mn where the M are variables of type 7 respectively e Similarly if a function f 71 Tn T is not declared to be non invertible it is considered invertible in those arguments where both 7 and 7 are subtypes of message or of some set type The semantics of being invertible in the i th argument for i 1 n can be define
140. er if there are several non collaborating intruders FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 98 190 e Ae B denotes an authentic channel from A to B This means that B can rely that any message M he receives via this channel indeed comes from A One may thus say the channel protects the identity of the sender and use the bullet to indicate this Note that authentication is tied to the integrity of the transmitted message B can be sure that A has sent exactly that message M Furthermore in all channel models for channels that are at least authentic B can be sure that the message was meant for him This additional property known as directedness has been motivated in 2 4 1 4 The authentic channel does not however protect message transmission against eaves dropping the intruder can still see the message disruption the message does not arrive at the intended receiver replay the message may arrive several times even much later or re ordering messages may not arrive at the recipient in the order they were sent The behavior of an authentic channel is thus like a digital signature on the message by the sender including the intended recipient as part of the signed text e A eB denotes a confidential channel from A to B This means that A can be sure that any message M sent over this channel can only be read by B hence the bullet on the receiver side Any intru
141. es Default is btd Backward strategy with depth first recursivity Backward strategy with breadth first recursivity Backward TopDown plus heuristical choice of the fact to descend into first Extend tests for negtive constraints w r t Horn Clauses Debugging options max n y tab par heavy debug int Forced activation of lvl 0 if this number of steps is reached default 80 Print even more output and term informations debug Write the correspondence table debug Write the parser output debug Extend the search for unforgeable atoms Write debuging informations for Read ml debug a SEVENTH FRAMEWORK PROGRAMME FP7 ICT 2007 1 Project No 216471 A AN T SSAR D2 3 update ASLan specification and tutorial 188 190 split Use the split option on hlps12if for hlpsl input file states Shows all internal system states of the analysis trace Use trace Short trace to follow one particular trace reverse Inverse the order of protocol steps in the read module Miscellaneous options version Print the version number licence Print the Cl AtSe s disclaimer licence help Display this list of options help Display this list of options FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 189 190 References 1 10 11 12 AVANTSSAR Deliverable 2 1 Requirements for modelling and ASLa
142. es aba coec oec eea POA OES ES 175 Age Typing esas o ee a oS ee Ae A BM ee Ow 176 A 3 5 Micro and Macro PS av wie bw ae a Oe SE Ho 177 B Connector and Model Checker Options 179 B 1 ASLan Connector oaoa ee eee 179 B 2 SATMC das 6 oe OR ew Ge we a a a a wS 181 B3 OFMO gt ga oh kek ce ek me pa a ROW Ao Oe oe ee E 182 B 4 Cl AtSe ope 6 oO eb ke ee EA ea ea A 184 References 189 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 5 190 List of Figures oono AUNE E How the Model Checker simulates the Attacker 11 The Sequence Chart for the NSPK Protocol 11 The annotated Sequence Chart for the NSPK Protocol 12 The Security Goals for the NSPK Protocol 15 Nested Entities Environment its Sessions and their Actors 17 Two parallel sessions Multiple Interference Facilities 2 18 An AVANTSSAR Model Checker found a Vulnerability in the NSPK Protocol 28 The Lowe Attack on the NSPK Protocol 0008 29 Lowe s Fix for the Vulnerability in the NSPK Protocol 2 30 The CA Hierarchy Setup sad CIA Be ee Ge ee OR 31 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 6 190 List of Tables 1 Channel notations in ASLan for CCM and ICM 101 2 Channel notations in ASLan for ACM
143. es are partially supported in ASLan depending on the channel model as described in the subsequent sections FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 99 190 e Resilient channels the intruder cannot disrupt the communication indefinitely and messages will thus eventually arrive at the intended recipient With reference to the formalism presented in D3 3 2 4 2 this amounts to requiring that every message sent over the channel may be delayed by the intruder for an arbitrary but finite amount of time but will be eventually delivered to the intended recipient e Pseudonymous channels one endpoint is not authenticated but uses a unique pseudonym relative to which the channel is secured e Channels that are protected against replay This is also known as freshness of a channel each sent message can be received only once In ASLan we directly support this notion as a communication goal In ACM this is implied by the confidentiality and weak confidentiality channel assumptions while in CCM ICM it can be implemented by using sequence numbers or challenge response e Channels that are order protecting We do not have this as an ASLan primitive so far but it can be achieved by including sequence numbers into the messages e Linked channels where we distinguish different channels between two end points This is directly supported by ACM while for CCM ICM it can be achiev
144. essage non associative concatenation FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 118 190 subtypes of message and related symbols types text lt message agent lt message symmetric_key lt message private_key lt message public_key lt agent symbols noninvertible hash message message noninvertible scrypt symmetric_key message message noninvertible crypt public_key message message noninvertible sign private_key message message noninvertible defaultPseudonym agent nat public_key private inv public_key private_key noninvertible pk agent public_key generic public key symbols used for implementing CCM noninvertible ak agent public_key authentication noninvertible ck agent public_key confidentiality atag slabel authentication tag ctag slabel confidentiality tag stag slabel security A C tag symbols used for implementing ICM athCh agent agent message fact msg on authentic channel cnfCh agent message fact msg on confidential channel secCh agent agent message fact msg on secure channel symbols used for implementing ACM sent agent agent agent message channel fact rcvd agent agent message channel fact confidential_to channel agent fact weakly_confidential channel fact authentic_on channel agent fact weakly_authentic channel fact resilient c
145. etGlobal gt contains ei1 SetGlobal gt remove el Actor gt B sync2 entity Bob A Actor agent body FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 56 190 SetGlobal e1 e2 Possible assignment method SetGlobal gt add e1 Alternative assignment method SetGlobal gt add e2 Alternative assignment method Actor gt A syncl A gt Actor sync2 assert no_alarm SetGlobal gt contains e1 body SetGlobal Initialize global set new Alice a b new Bob a b Initially el belongs to SetGlobal Bob asks Alice by sending the synchronization message sync1 to apply her changes to the set Alice assigns the empty set to SetGlobal Then Alice notifies Bob by sending message sync2 that he can now access the shared set Indeed at this moment SetGlobal does not contain el anymore Hence the assertion no_alarm is never violated and therefore no attack has to be reported You do not need any special options for the model checkers Please note that when translating this model there will be warnings regarding the use of global variables You may ignore them at this point Currently only CL AtSe and SATMC support global sets OFMC cannot be used for verifying specifications which use global sets The synchronization mechanism as it is always the case with accessing shared objects is crucial for the correct working of the e
146. evel of a session entity and pertains to those message transmissions in sub entities that contain goal labels using the same goal name See also the example below When goals are specified using the channel notation they refer to individual message transfer even when the ACM is chosen for channel assumptions In other words the arrow symbols are interpreted as for channels as assumptions in the ICM CCM independently of the channel model chosen which only affects channel assumptions This implies the intuitive meaning for each type of arrow as given in Table 7 More details can be found in 2 4 1 4 and 18 19 As an example consider the following specification excerpt entity Session A B agent entity Alice Actor B agent symbols Payload message body Actor gt B secure_Alice_Payload_Bob Payload send Payload to B somehow fully secured entity Bob A Actor agent symbols Payload message FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 108 190 body A gt Actor secure_Alice_Payload_Bob Payload receive Payload from A somehow fully secured body new Alice A B new Bob A B goals secure_Alice_Payload_Bob _ A gt B A channel goal is given as follows The goal is stated using an arbitrary goal name in an entity enclosing both the sending and receiving entity In th
147. f ASLan on the channel model question but instead allow the modeler to plug in different kinds of channels and models for them which allows us to later define more and or different models Such extensions are currently in progress and can be integrated into the AVANTSSAR Platform in future 3 9 Goals Validation goals have a name and in one way or the other give rise to an LTL formula or equivalently an attack state that is checked by the validation back ends at appropriate times An LTL formula may contain predicates of type fact which may refer to the values of variables in the scope of the current entity typically at the current state of execution the usual first order logic operators namely propositional connectives and quantifiers and future and past temporal operators The LTL operators for ASLan are listed in Table 6 See A 3 and 4 12 for formal definitions of the operators Note that most LTL formulas that state a liveness property e g lt gt P would not hold for any ASLan or ASLan model because the semantics of specifications are Kripke structures in which the transitions relations are reflexive see A 3 In order to verify liveness properties therefore fairness assumptions must be added to the Kripke structure which can be done via LTL constraints In ASLan there are different kinds of goals which we describe below 39Due to stuttering at the ASLan level and merging of transitions d
148. f instructions In the case of the root entity it is also necessary to add its state fact with step label s1_0 in section inits in the translation in order for the execution to start For all other entities all rules that have on their left side the state fact with step label s1_0 need to contain FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 153 190 the extra precondition not dishonest Actor to avoid executing superfluous transitions which would be needlessly inefficient and could lead to spurious attacks Note that as a final step of the translation the step label terms built up from the s1_0 succ and branch symbols are replaced with numbers 4 13 describes how this is done 4 11 Translation of the Constraints Section The translation of constraints in the constraints section is immediate consisting in minor syntactical adjustments 4 12 Translation of the Goals Section 4 12 1 Invariants In the case of invariants given as LT L goals in a similar way as for guards we need to translate the LTL operators to ASLan LTL syntax given in A 3 according to Table 12 After doing so the terms contained in the goal formulae must be converted by means of a slight variant of the procedure introduced in 4 9 which we omit Operator ASLan connective ASLan predicate a If not f fi f2 equal f_1 f_2 f1 lef 2 not equal f_1 _2 A fi amp f
149. fidential_to server ch_server gt authentic_on server Apart from these declarations the resulting ASLan model is basically the same as before Oclatse nb 2 specification TLS_SessionsOrder_ACM channel_model ACM entity Environment symbols succ nat nat workaround declaration should not be needed server agent ch_server channel public initiation channel of server noninvertible ch_c2s text channel from client to server noninvertible ch_s2c text channel from server to client symbols ServerSessions agent text nat set global for Server entity Session C S agent ChS channel entity Client Actor S agent ChS channel symbols SessID text Counter nat PayloadC PayloadS text body 4 SessID fresh secrecy_goal secret_SessID Actor S SessID bilateral_conf_auth ch_c2s SessID ch_s2c SessID Actor S Counter 0 start session Actor ChS gt 8 Actor SessID Counter Counter succ Counter 1 PayloadC fresh Actor ch_c2s SessID gt S Counter PayloadC channel_goal Client_TLS_Server Actor gt gt S Counter PayloadC S ch_s2c SessID gt Actor Counter PayloadS channel_goal Server_TLS_Client FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 86 190 S gt gt Actor Counter PayloadS Counter succ Counter 2 PayloadC fresh
150. fore we use a function renewPositiveFactsIn that renews the positive explicit facts in the clause Implicit facts are not reintroduced on the right hand side of the corresponding rewrite rule because implicit facts stored in the set PolicyPredicates see 4 4 must not appear on the RHS of rewrite rules The function renewPositiveFactsIn is used in 4 7 5 4 7 9 4 7 10 etc 4 7 1 Grouping Grouping stmt rest sl return_sl stmt InnerStmts ParseCode InnerStmts rest sl return_sl FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 129 190 In the case of a series of statements grouped by brackets the internal statements are prepended to the remaining statements and the parsing is resumed on this new list of instructions 4 7 2 Variable assignment Assign stmt rest sl return_sl 4 stmt Var Term LHS state fact for this entity with step label sl state fact for the owner of Var RHS state fact for this entity with step label succ sl state fact for the owner of Var with Var set to Term add LHS gt RHS to section rules in the translation ParseCode rest succ sl return_sl In case of assignment to a variable Var we create a rewrite rule as given above with one exception Since Var may belong to an ancestor of the entity we need to change its state fact rather than the current entity s for which we will update the
151. g the checking for equality of received values to already known values and the decryption of encrypted values We have seen that Alice and Bob by message passing need to learn the values of nonces and names and need to check them for equality In ASLan this is done implicitly by pattern matching For instance let s look at the specification of entity Bob entity Bob A Actor agent 4 symbols duced and retracted as global meta information and message anything that can be sent over a network It also specifies that text and agent are subtypes of message and introduces a number of pre defined constants For more details on the standard prelude see 3 13 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 19 190 Na Nb text body gt Actor Na A _pk Actor secret_Nb Nb fresh Actor gt A Alice_authenticates_Bob Na Nb _pk A A gt Actor Bob_authenticates_Alice Nb _pk Actor secret_Na Na Na In line 7 Bob receives a message from some party which at this point is still unknown to him This is denoted by the on the left hand side of the message passing definition He learns the name A the sender claims to have and memorizes it Learning a value for A is indicated by the preceding A By Na Bob also learns the value Na which implicitly is decrypted using his private key corresponding
152. g an experimental feature You can safely ignore this warning and check the model with CL AtSe For a further example you may refer to 2 7 where we provide a simple RBAC model utilizing Horn Clauses 2 2 Modeling hints When specifying a protocol system in ASLan you may wonder whether your model is correct Of course there may be conceptual mistakes You for instance may have misunder stood the protocol system properties and the resulting model therefore would not adequately represent reality However here in this chapter we do not want to address conceptual cor rectness of individual models Rather we now discuss programming errors and inefficiencies These can render any conceptually flawless model useless We point out a few basic strategies of how to avoid the most common mistakes 2 2 1 Debugging wrt executability problems The following advice should be every model checker s intrinsic mantra Prior to checking your model for attacks FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 37 190 ALWAYS ensure executability of your model first If a model checker responds with NO_ATTACK_FOUND this does not necessarily mean that the protocol system described is secure Before you may put trust in such a result you must ensure as far as possible that there are no problems in the model or in the tools Until then indeed you must be very suspicious if no attack has b
153. ges 147 166 Springer Verlag 1996 G Lowe A hierarchy of authentication specifications In Proceedings of the 10th IEEE Computer Security Foundations Workshop CSFW 97 pages 31 43 IEEE Computer Society Press 1997 G Lowe Casper a Compiler for the Analysis of Security Protocols Journal of Com puter Security 6 1 53 84 1998 http web comlab ox ac uk oucl work gavin lowe Security Casper FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 190 190 116 17 18 19 20 21 22 U M Maurer and P E Schmid A calculus for security bootstrapping in distributed systems Journal of Computer Security 4 1 55 80 1996 S M dersheim Models and Methods for the Automated Analysis of Security Protocols PhD Thesis ETH Zurich 2007 ETH Dissertation No 17013 S Mo dersheim and L Vigan Secure Pseudonymous Channels In Proceedings of Esorics 09 LNCS 5789 pages 337 354 Springer Verlag 2009 S M dersheim and L Vigan The Open source Fixed point Model Checker for Sym bolic Analysis of Security Protocols In Fosad 2007 2008 2009 LNCS 5705 pages 166 194 Springer Verlag 2009 S Modersheim and L Vigan Channels as Assumptions Channels as Goals 2010 Submitted journal paper R Needham and M Schroeder Using encryption for authentication in large networks of computers Communications of the ACM 21 12 december
154. h forall RS forall A forall B forall M G implies resilient Ch G implies sent RS A B M Ch F rcvd B A M Ch The fact that the principal sending messages on Ch1 is the same principal that receives messages from Ch2 is captured by the 1ink Ch1 Ch2 property which is translated as the LTL constraint forall Chi forall Ch2 forall RS forall A forall B forall M forall R forall B forall M G implies link Ch1 Ch2 G implies and F sent RS A B M Ch1 F rcvd R B M Ch2 equal RS R The relation between two channels Chi and Ch2 capturing a bilateral confi dential and authentic communication between A and B is expressed by the fact bilateral_conf_auth Ch1 Ch2 A B This is implementend as shorthand that the trans lator expands on introduction to the facts confidential_to Ch1 B authentic_on Ch1 A confidential_to Ch2 A authentic_on Ch2 B Similarly the relation between two channels Chi and Ch2 capturing a unilateral confidential and authentic communication between A and B expressed by the fact unilateral_conf_auth Ch1 Ch2 B is expanded to the facts confidential_to Ch1 B weakly_authentic Ch1 weakly_confidential Ch2 authentic_on Ch2 B link Chi Ch2 4 7 7 Fact introduction When translating a fact introduction statement as defined next a check is done whether the fact symbol is contained in the set PolicyPredicates cf 3 5 and 4 4 In this case with the exception of i
155. h the original set copying all elements in both the copy and the backup location Finally we restore the elements from the backup location to the original location For improved efficiency we of course can combine performing actions on the elements and making the necessary backup for set preservation This is left to the reader as simple exercise To make this work with SATMC you need to set no special options For OFMC as usual please use the options classic untyped When using CL AtSe you must state the option nb lt n gt Select lt n gt large enough to cover the maximal number of iterations of while loops in the model For instance lt n gt resolves to at least 5 if you plan to use an example set with 5 elements This allows CL AtSe to execute the verb while loop 5 times FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 44 190 2 3 3 Union and Intersection Union If we want to compute the union of two sets not preserving the original sets and ending up with the union of both sets we may simply move the contents to one set into the other set MySetUnionResult MySetl Result points to MySet1 MySetUnionResult MySeti MySet2 while MySet2 gt contains E MySetUnionResult gt add E MySet2 gt remove E After this MySetUnionResult points to the same location as MySet1 where also the elements of MySet2 have been added MySet2 is now empty If we
156. hannel fact link channel channel fact bilateral_conf_auth channel channel agent agent fact unilateral_conf_auth channel channel agent fact macros M _K scrypt K M M _K crypt K M M _inv K sign inv K M FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 119 190 parameterized tuple type and related symbols types A B lt message symbols Cos J A B tuple constructor paramerized type of sets and related symbols types A set symbols Misas PUE A set set literal contains A set A fact add and remove are implemented by introducing and retracting contains facts clauses true_holds true dishonest_intruder dishonest i analysis_crypt K M iknows M iknows crypt K M amp iknows inv K analysis_scrypt K M iknows M iknows scrypt K M amp iknows K analysis_sign K M iknows M iknows sign inv K M amp iknows K end entity Prelude The modifiers private and noninvertible are explained more formally in 4 3 intuitively they are used to override the default behavior of function symbols that terms can be arbitrar ily composed that is functions are public and decomposed that is functions are invertible by the intruder Note that cryptographic operators are usually public and non invertible there are special intruder dedu
157. he above mistakes are found For instance SATMC which can report multiple goal violations at once prints DETAILS ATTACK_FOUND GOAL no_uninitialized_msg dummy_message no_uninitialized_mem set_1 fnat iid_1 0 0 dummy_message no_uninitialized_set dummy_set_message i This technique could be extended further to check e g for uninitialized sender and receiver variables in transmission statements 2 2 3 Improving efficiency Models may take quite a long time to get checked by a model checker Sometimes the size and complexity of a model may even prevent receiving an answer within reasonable time If the protocol and system to be modeled is so very complex and cannot be simplified sometimes this is unavoidable Maybe it can in some cases be solved by using a better computer Or it would require improving the translator and or the model checkers Or according to current facilities it cannot be fixed at all However modelers may follow some guidelines to improve the efficiency of their models making it easier for the translator to generate more efficient ASLan code and for the model checkers to perform faster checks This will allow for more for better lumping of ASLan transitions that is more efficient ASLan code generation resulting in reduced search space FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 41 190 e Try to ma
158. he can react accordingly The input of Web Sequence Diagrams corresponding to Figure 9 is A gt B Na A Kb B gt A Na Nb B Ka A gt B Nb _Kb We can now transfer the simple correction to our ASLan model of the NSPK protocol Within the definition of Bob we add as additional parameter Bob s name to the message he sends to Alice and on Alice s side we receive and check this name against the expected partner Bob entity Alice Actor B agent body B gt Actor Alice_authenticates_Bob Na secret_Nb Nb B _pk Actor entity Bob A Actor agent body FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 31 190 trusts Root CA LL la trusts certifies Figure 10 The CA Hierarchy Setup Actor gt A Alice_authenticates_Bob Na Nb Actor _pk A If we now re translate and re check the corrected model no more attack is found 2 1 7 Clauses Deductions and Recursion A concept required frequently is that of computation including recursion Although in ASLan there are no function calls there are clauses that may be used for such and many other purposes This section introduces some basic use of clauses We specify a simple Public Key Infrastructure PKI extension of our NSPK example and show how to use Horn Clauses to do deductions including recursion of additional facts from given facts On Public Key Inf
159. he mutex relations to be used during the SAT reduction i e 0 mutex off absRef on and 1 mutex on absRef off Basically if MUTEX is set to 0 then the abstraction refinement strategy provided by SATMC is enabled otherwise the abstraction refinement strategy is disabled and the static mutexes are generated the default value is 0 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 182 190 o OUTPUT_FILE the output is printed in the file OUTPUTA_FILE instead of the stan dard output output_ dir ODIR ODIR is the directory in which SATMC will store temporary files and put the detailed results of the analyzes in case the AVANTSSAR output is enabled by default these files will be put in the same directory in which FILE is contained of OF OF is a string indicating the output format selected aslan standard output format from the AVANTSSAR project default value or if standard output format from the AVISPA project sc SC SC is a boolean parameter for enabling or disabling the step compression op timization by default it is set to true Note in case the Abstract Channel Model ACM is used it must be set to false e exec to enable or disable the check on executability of actions rules without any intruder It is very useful to debug the input specification by default it is set to false Reserved keywords While using the tool conside
160. here the ICM serves as the abstract reference model Since ICM and CCM are equivalent at the ASLan level CCM channels and ICM channels are expressed in the same way the differences of these two channel models manifest in their translation to ASLan 3 8 2 Channel security notions Since the term channel has been used in many different ways both in academia and in the ICT industry in order to avoid any confusion let us first clarify our notions for channels and their properties depending on the particular channel model used For all channel models the default communication medium is a channel without any protection an insecure channel Here the communication medium is fully controlled by an intruder who according to the Dolev Yao model 11 can read and intercept all messages as well as send arbitrary messages he can craft to any agent as long as he has the appropriate keys i e he does not break cryptography One may imagine this situation as the intruder being the network Inspired by the bullet notation of 16 for CCM and ICM we introduce several kinds of channels that offer various forms of protection e A B like it is commonly written in the analysis of simple security protocols denotes the default insecure channel from A to B 35Qn the other hand potentially there may be properties that can be described more adequately in CCM by means of cryptographic primitives 36The situation is more complex howev
161. hird argument of sent identifies the intended receiver R The first argument of rcvd is the real name of the receiver R whereas the second argument is the official sender The remaining two arguments are the message M transmitted and the name of the channel Ch respectively Note that this rule entails directedness the only honest receiver of a message is the intended one The abilities of the intruder are augmented by the following rules step fake 0S R M Ch iknows M iknows 0S iknows R gt iknows M iknows 0S iknows R sent i 0S R M Ch step intercept A R M Ch sent A A R M Ch gt rcvd i A M Ch iknows M step overhear A R M Ch sent A A R M Ch gt sent A A R M Ch rcvd i A M Ch iknows M For instance the first rule models the intruder that exploits its knowledge to impersonate an agent OS in sending a message M to an agent R on a communication channel Ch FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 140 190 The facts used at the ASLan level cf Table 3 Table 4 and Table 5 to state assumed channel properties are kept at the ASLan level such that the backends can use them as triggers for LTL constraints described next The condition that a channel Ch is confidential to a principal p can be formalized by the following LTL formula confidential_to Ch p forall A forall B forall M G implies rcvd B A M Ch equal B p
162. ight hand side are fulfilled These conditions are typically positive occurrences of facts but we have some support by the experimental CL AtSe option not_hc also for equalities as well as negative facts and inequalities Both the head on the LHS and the body on the RHS may refer to local or inherited variables of the entity where the clause is defined making it applicable only when the entity instances owning these variables are present All other variables in the clause i e free in the scope of the owner entity are treated as universally quantified Free variables not appearing on the RHS and only these must be explicitly universally quantified using the keyword forall Any other free variables and only these must be listed as formal parameters right after the name of the clause which is useful for documenting derivations that involve the clause For instance assume Z is a variable defined in an entity Then the following Horn clause may be declared in the entity hc_name X forall Y fact2 X Y factia X amp factib Z When it comes to retracting facts from a state there is a difference between facts implic itly produced by the clauses and those explicitly introduced in the state For instance in the example above if factita 1 and fact1b 2 hold retracting fact2 1 3 would not be ef fective because fact2 1 3 is spontaneously introduced according to the clause hc_name In order to help the modeler to make
163. in C You can imagine they point to a location where the elements in the set are stored For instance if you copy with TextSetCopy TextSet then both pointers point to the same location and thus they are aliases of the same set of elements You do NOT get a cloned set of elements that way Naturally you also cannot concatenate sets simply with a like Set3 Set1 Set2 Just imagine what it would mean to concatenate two pointers in C FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 42 190 2 3 1 Basic Commands For querying and manipulating sets in ASLan we can use the following basic facts and statements commands For all these operations the type of variable E must be the type of the elements of MySet Contains contains MySet E or equivalently MySet gt contains E This fact states that the element E belongs to MySet If you use a like a wildcard with the element name then MySet gt contains E returns the value of a single random element if there is at least one element in the set If you use composite elements then you also may partially qualify the query like in ServerSessions gt contains C SessID N where client C and SessID are known and N may have any value If multiple elements would qualify this query also returns only a single random element IsEmpty if MySet gt contains it is empty There is no dedicated is
164. in many classical authentication definitions that had not been observed before the details are found in 18 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 100 190 Note that the properties for channels as goals refer to individual transfer of messages only which also holds for CCM and ICM channel assumptions whereas ACM channel assumptions may stretch over multiple message transmissions In an ASLan specification the channel model is globally specified right at the begin ning after the specification name using the keyword channel_model For ICM and CCM but also for channels goals in all channel models including ACM we adopt the intuitive notation from 16 briefly introduced above where a secure end point of a channel is marked with a bullet Just note that while so far we have used abstract bullet symbols we now switch to the concrete ASLan syntax and write e g A gt B M instead of Ae gt B M e A gt B Mrepresents an authentic transmission of M e A gt x B M represents a confidential transmission of M e A gt B M represents a secure transmission of M There is also a further variant of the channel notation using a double headed arrow like gt gt representing a fresh channel This notation may be used for channel goals that include at least authenticity e g A gt gt B M represents the goal that a channel is both secure and fresh
165. in the first phase converting ASLan terms into ASLan ones and e replacement of step label terms with numbers as described in 4 13 Finally 4 10 describes the translation of the encapsulating body section In order to decrease the number of transition rules that are generated by the translation procedure the set of transition rules can be optionally optimized 4 15 describes the two levels of optimization that can be employed 4 1 Preprocessing As a first step we consider a group of preliminary operations on the input specification which do not generate ASLan specifications but rather modify the input specification to ease the translation procedure These operations are Import of external modules In the import section a modeler can specify any number of external entities called modules to be included into the current entity specifica tion Importing a module corresponds to merging the sections of the module with the analogous sections of the current entity specification This step results in a single en tity without any remaining import section Note that imported modules may contain imports themselves treated recursively FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 122 190 Global disambiguation of elements Since entities may have nested sub entities local declarations of elements e g symbols sub entities types goals hide any homony mous ele
166. in the translation ParseCode rest succ sl return_sl A symbolic entity instantiation consists in a partially specified instantiation of an entity Its purpose is modelling a whole class of instances i e for all possible instantiations of the bound variables A_1 A_m with constants taken from the domain Usually these variables and constants are of type agent but it is only required that each of their type is a subtype of message The instruction is translated to a rule that introduces the new entity instance on the RHS The variables A_1 A_m will be bound to ground constants by the predicates iknows A_1 iknows A_m appearing in the LHS of the rule and also renewed in the RHS The binding allows to explore all possible instantiation of the variables A_1 A_m with concrete values To this end m new constants are declared of the types determined from from the respective parameters of the entity In addition to this the rule will also enforce that the chosen values for A_1 A_m satisfy Guard whose treatment using the auxiliary function positiveGuards we will introduce in FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 134 190 detail in 4 7 9 4 7 6 Send receive and channel models Transmission stmt rest sl return_sl if stmt receive params then Select select on stmt rest sl return_sl else stmt send params Introduc
167. ing in p_j gt RHS renewPositiveFactsIn p_j rules in the translation ParseCode LeftStmt branch sl i succ sl ParseCode rest succ sl return_sl The select construct allows one to nondeterministically pick one code block provided its guard is satisfied If no guard is satisfied it blocks until one is Theon guards in a select statement which typically contain receive conditions are translated with the adaptGuard function as described in 4 8 This translates in a way similar to an if construct differing in the following two aspects e the number of branches varies according to the number of different code blocks con tained and e there is no branching for failed evaluation of guards since the construct blocks until one is satisfied Example 9 The methods a SEVENTH FRAMEWORK PROGRAMME FP7 ICT 2007 1 Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 149 190 select on p_1 q_1 on p_n q_n will be translated to the following rules state _BidM Actor IID s1 BP M p 1 gt state BidM Actor IID branch sl 1 BP M p_1 state BidM Actor IID branch sl 1 BP M gt state_BidM Actor IID succ branch s1 1 BP M q_1 state BidM Actor IID succ branch s1 1 BP M gt state _BidM Actor IID succ sl BP M state _BidM Actor IID s1 BP M pn gt state BidM Actor IID branch sl n BP M p_n state _BidM Actor IID branch sl n
168. is a constant c In this case we leave c as is e T V i e Tis a variable V The case is similar to the above one for constants except that the variable name must be bound to its value Therefore we add the state fact of the owner of V to both LHS and RHS of R e T T_1 ie T is a pseudonym term T_1 which must be of type agent or of a subtype of it Then T will be replaced by defaultPseudonym T_1 IID if T_1 is Actor T_1 otherwise where T_1 is the recursive translation of T_1 and IID is the instance ID of the current entity FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 152 190 e T T_1 _ T_2 i e T represents an explicitly given pseudonym T_2 for the agent represented by term T_1 In this case the result is simply the recursive translation of T_2 that is T_1 is ignored e T T_1 T_2 T_n ie T is the concatenation of terms T_1 T_2 T_n In this case we apply the binary predicate pair to T_1 and the recursive application of pair to T_2 T_n and finally apply the terms translation procedure recursively on each of PA a a e T T_1 T_2 T_n i e Tis a tuple containing the terms T_1 T_2 T_n This case is translated exactly as the one for concatenation also as right associative pairing e T T 1 T_2 T_n ie Tisaset literal of type T set containing the elements T_1 T_2 T_nall of type 7 We create a fresh function symbol sf
169. is used The value for the protocol_id parameter is derived from the name of the channel goal depending on the kind of the channel Table 13 summarizes the events that are used for each kind of channel together with the rule for deriving the value for protocol_id Other fact symbols could be considered for the specification of other channel goals such as the facts whisper and hear that are considered for a different notion of secrecy for the compositionality results given in 18 44For the fact symbol secret the parameter of type protocol_id is not actually needed FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 155 190 Channel kind Events used Rule for deriving protocol_id Authentic witness request auth_ channel goal name Fresh request fresh_ channel goal name Confidential secret secr_ channel goal name Table 13 Events used in the translation of channel goals and rules used for deriving the protocol ID from the name of channel goals Declarations For ease of description consider the example similar to the one given in 3 9 3 where in some entity E there is the following channel goal declaration secure_Alice_Payload_Bob _ tA gt tB According to the syntactic restrictions given in 3 9 3 in each sub entity in which the goal label re appears there will be exactly one parameter that corresponds to the
170. its ancestors Assuming the restriction that entities can instantiate only direct sub entities we imple ment this binding as follows e We use a binary predicate descendant A D stating that the entity instance D has been instantiated directly or indirectly by A i e it is a sub entity of A in the tree of dynamically created entity instances e descendant predicate is completed by taking its transitive closure which is implemented via the clause descendant A D descendant A E amp descendant E D That is descendant facts are implicit facts see 3 5 In order to respect the distinc tion between implicit and explicit facts discussed in 3 5 the binary predicate child is consider with the following clause descendant A D child A D e At instantiation of an entity let iid and pid be the IDs of the new instance and its parent respectively We add to the state the persistent fact child pid iid e When we check for the state fact of the owner of a variable we actually write in the LHS of the generated rule both its state fact with ID OID and the predicate descendant OID iid where iid is the ID of the entity instance being executed at this step thus enforcing the binding See example 3 for more details 4 3 Translation of Types and Symbols ASLan has several built in types constants and functions as defined in 3 13 These are immediately reflected at the ASLan level After having in the pr
171. ity after a correction of its exec option Independently of such a special support by the model checkers a very helpful technique to spot and debug executability problems consists of manually adding checkpoints into the model like for instance assert reached_breakpoint4711 false for exec testing at various places in particular at the intended end of a protocol session Then with the help of the model checkers and typically for a single session of your protocol system you can observe if the artificial attack provoked by the false formula actually is found If so the breakpoint can be commented out and other reachability properties or actual security goals can be checked This technique also helps you to detect for instance overused statement lines caused by CL AtSe not being supplied with a large enough nb lt n gt value The nb option instructs CL AtSe how often it should execute code multiple times for instance in while 16Please note that individual unreachable statements not necessarily are a reason to worry about For instance with parameterized models if you instantiate your session with one parameter value sections of your model only applicable to other parameter values of course may not be executed Further if you use an if branch without any else branch in ASLan in ASLan there will implicitly be added an empty else branch which may show up as a single non executable statement pointing to the if branch of
172. ity as it would appear in a certificate but with respect to self chosen unauthenticated identifier called pseudonym This is indicated by square bracket the notation as in Actor gt using the sender s default pseudonym and a sender side signature One may also explicitly specify a pseudonym as in 20The digital signature implicitly deployed in CCM to implement gt serves as a proof of possession of FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 73 190 Actor _ MyNym gt When receiving a message on a pseudonymous secure channels with receiver side encryption we write gt Actor The server uses the term CP to represent the client s pseudonym Here is the ICM CCM specification of this request response pair entity Session C S agent symbols used for client_link LTL goal client_sent agent nat message fact client_rcvd agent nat message fact entity Client Actor S agent 1 PayloadC lt gt Nc fresh C generates nonce Actor gt S S can NOT verify C s identity Actor Nc PayloadC client_sent Actor IID Nc used for client_link goal S gt Actor Nc PayloadS checks nonce client_rcvd Actor IID Nc used for client_link goal entity Server C Actor agent 1 while true select on CP gt Actor S learns C here 7C Nc PayloadC PayloadS lt gt Actor
173. ke the code in the bodies of entities as linear as possible In particular try to avoid if and while constructs as far as possible If in a conditional statement you only need a positive branch like if condition statements then this can be coded more efficiently as select on condition statements e Use types as narrow as possible For example prefer type text over message whenever there is no need for the modeling to decompose into sub messages and use compound types indicating the internal structure of messages as far as possible This will reduce search time in particular for SATMC e Avoid complex recursive Horn clauses complex LTL goals etc For instance in many cases the lt gt once LTL operator can be avoided by using stable predicates i e facts that are never retracted 2 3 Set operations In ASLan we can use sets of elements of a certain type These types may be basic like text or nat They also may be composite like we will see in 2 9 on TLS where we use sets to model a session database Elements of sets must be of a uniform type and may not be of type fact Please note that sets are not multi sets thus elements may not be present in duplicates within a set The following examples define sets NatResultSet nat set TextSet text set ServerSessions agent text nat set Set variables like NatResultSet TextSet and ServerSessions are all references like pointers
174. known as modules with their filename being the entity name with the extension aslan appended to it which in turn contain a hierarchy of entity declarations There is a virtual module available called Prelude defined in 3 13 that is implicitly part of all specifications The top level i e outermost entity usually called Environment is not imported by any other entity but serves as the global root of the system being specified similarly to the main routine of a program Entities and variables have names starting with an upper case letter while types con stants and function names start with lower case letters The remaining characters in a name may be alphanumeric characters or underscores _ or primes Comments in ASLan as well as in the EBNF grammar in 3 12 start with a symbol and extend until the end of the line 3 3 Entities and agents The major ASLan building blocks are entities which are similar to classes in Java or roles in HLPSL 8 Entities are a collection of declarations and behavior descriptions which are usually known as roles in the context of security and communication protocols Entities may have parameters and contain via import or textual inclusion sub entities with nested scoping Variables and other items declared in outer entities are inher ited to the current one where inner declarations hide any outer declarations of elements 25Since the OFMC backend
175. knows an error message is produced by the translator because implicit facts are not allowed here FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 142 190 IntroduceFact stmt rest sl return_sl stmt funcapp LHS state fact for this entity with step label sl RHS state fact for this entity with step label succ sl funcapp add LHS gt RHS to section rules in the translation ParseCode rest succ sl return_sl An element addition statement of the form add Set X is handled as an introduction of contains Set X 4 7 8 Fact retraction When translating a fact retraction statement as defined next a check is done whether the fact symbol is contained in the set PolicyPredicates cf 3 5 and 4 4 In this case an error message is produced by the translator because implicit facts are not allowed here RetractFact stmt rest sl return_sl stmt retract funcapp LHS state fact for this entity with step label sl funcapp RHS state fact for this entity with step label succ s1 add LHS gt RHS to section rules in the translation ParseCode rest succ sl return_sl If the fact to be retracted is not present execution is blocked as long as the fact is not introduced An element removal statement of the form remove Set X is handled as a retraction contains Set X FP7 ICT 2007 1 L Project No 216471 A ANTSSAR
176. ks However it is pretty inefficient and does in no way utilize the full capabilities of the model checkers How could we proceed more efficiently By properly challenging the model checkers and letting them do the hard work they have been desigend to do We can query for the sub set property more efficiently utilizing the fact that the model checkers will evaluate any possible combination on their own anyway when properly challenged For this we state the following FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 46 190 nonpublic nonSubset fact A initially this fact is not set MySeti gt isSubsetOf MySet2 if MySet1 gt contains E amp MySet2 gt contains E nonsubset assert subset_test nonSubset This also works And it is much less work for us and less work for the model checker as well You will notice that this evaluates much faster Black magic No How does it work If you challenge a model checker by stating a security goal the model checker will look for ways to violate that goal This is similar to what it does here We say activate the nonSubset fact if and only if there is some E that indicates that the subset property does not hold The model checker will now try to find a way to violate the subset property by trying all possible values of elements from the two sets It will take each element from MySet1 and look at all elements from MySet2 t
177. l_conf_auth Ch_C2S Ch_S2 C S already used in the previous example specification TLS_client_auth_ACM channel_model ACM entity Environment symbols login ok text nonpublic noninvertible password agent agent text entity Session C S agent 4 symbols Ch_C2S Ch_S2C channel entity Client Actor S agent Ch_C2S Ch_S2C channel symbols Payload text body Actor Ch_C25 gt S login Actor 21Note that after successful client authentication we could have directly used secure channels instead of pseudonymous channels replacing e g Actor gt S by Actor gt S and CP gt Actor by C gt Actor making use of the compositionality theorem for CCM ICM Yet we did not perform this transformation in order to avoid confusion between the assumed properties of the channels namely unilateral TLS and the additional property namely client side authentication obtained by explicit authentication via the client s password FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 79 190 shared_secret password Actor S S Ch_S2C gt Actor ok Payload fresh Actor Ch_C25 gt S secure_transmission Payload entity Server C Actor agent Ch_C2S Ch_S2C channel symbols Payload text body 4 T Ch_C2S gt Actor login C Server learns C here shared_secret password C Actor checks password proceeds only if fine Acto
178. lain user account remove the comment in line 43 Then on retracting the admin role from Alice she still retains that user account and therefore can still read and disclose Datum to Eve This is also confirmed by Cl AtSe 2 8 Communication in different channel models We currently support three different channel models Cryptographic Channel Model CCM communication is realized by passing individ ual messages via the intruder security is achieved via applying cryptography to the messages Ideal Channel Model ICM This is similar to CCM with the difference being that message protection is achieved by more abstract means Abstract Channel Model ACM named channels are realized using explicit send and receive events that may be constrained by LTL formulas over the traces Thanks to the encoding of channels by cryptographic means that all current backends support CCM can be used with all existing backends ICM is currently more of theoretical interest While in CCM and ICM the focus is on individual message transfers in ACM there is a built in notion of channel identities ACM is currently supported only by SATMC It has a slightly different syntax and semantics of channels which allows for transmitting messages with respect to a channel name and for specifying channel properties more flexibly via LTL formulas For more details about the syntax and semantics of channels please refer to 3 8 and 4 7 6 FP7 ICT 2007 1 L P
179. le classic run only in classic mode o lt outputfile gt saves the result of the analysis in a file exec e checks the executability of each rule do not search for attacks help h display this help version display the version Options for classic mode theory lt TheoryFile gt use a custom algebraic theory sessco performs an executability check and session compilation untyped u ignores all type declarations depth lt DEPTH gt n lt DEPTH gt specify maximum search depth depth first search trace lt PATH gt t lt PATH gt PATH is white space separated list of ints specify a path in the search tree to visit by the indices of the successors to follow By default OFMC makes use of both classic and fixedpoint modules see 6 for more information on OFMC components and how they work and takes into account type declaration while considering the specification But since the fixedpoint module can only check models without composed types in many cases an error occurs if no options have been set As the error message says the more common way to circumvent the problem is to use the classic module only without the fixedpoint module by using the option classic A good practice while using OFMC is to use also untyped option because if there are composed types in the specification it is possible to obtain false NO_ATTACK_FOUND results see 6 for more details For what concerns depth and trace opti
180. lect on BMessage BE box Rest BNatSet gt add BE BMessage Rest assert finished false body of Environment new Alice a b new Bob b a Alice forms a concatenation of all elements of NatSet into NatSetMessage We use a box bracket to aid Bob in precise un marshalling We preserve a backup of NatSet in NatSetBackup In the end NatSetMessage consists of a concatenation of all the elements in NatSet which might look like 3 box 2 box 4 box 1 box nil which reminds us that contains non deterministically returns any element We restore the original NatSet from NatSetBackup Now Alice ships NatSetMessage to Bob Bob has to revert the procedure to retrieve the set from the message containing the concatenation of the set s elements In Bob s specification BMessage denotes the message received by Bob It contains a box ed concatenation of elements of type nat This message Bob processes iteratively we retrieve its elements BE one by one and add them to BNatSet Every added element BE is split off BMessage The box bracket aids Bob in precise un marshalling Why is this needed Let s suppose we would not used the box operator and instead transmit the message FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 62 190 SetMessage M1 M2 Mn directly where each Mi is an element of type message from MySet which is a set of type message The
181. lects a large number of situations like an honest agent who has been compromised and whose long term keys have been learned by the intruder or when there are several dishonest agents who collaborate This worst case of a collaboration of all dishonest agents may be simply modeled by one intruder who acts under different identities 28For instance to ensure that the intruder can generate for himself new pseudonyms y at any time and can send and receive messages with these new pseudonyms we use the predicate dishonest in the rule Y iknows w iknows inv w dishonest q This includes inv w which we need for the CCM where pseudonyms are simply public keys as e g in PBK Creating a new pseudonym thus means generating a key pair 4 inv w FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 92 190 As long as the actual value of the Actor parameter of an entity is an honest agent the agent faithfully plays the role defined by the entity If the Actor parameter value is dishonest already on instantiation of the entity which is typically the case for some of the possibilities included in symbolic sessions the body of the entity is ignored because the intruder behavior subsumes all honest and dishonest behavior We also allow that an entity instance gets compromised later that is the hitherto honest agent denoted by the Actor of the entit
182. levant in the interleaving of the entities hence they can be safely lumped together The effect of lumping is similar to atomic blocks i e nothing else can happen before the atomic section is finished 4 14 2 Step granularity and breakpoints The step granularity of a model is controlled by the set of breakpoint actions By default the only breakpoint is the action receive The modeler may optionally specify for each entity additional breakpoints with the declaration breakpoints bp_1 bp_n This set of breakpoints is inherited to sub entities unless they declare their own set of breakpoints If needed a modeler can specify further individual breakpoints in the model by placing a breaking instruction e g receive at the desired points of the code This will artificially force the translation to stop compressing and start a new transition The meaning is that all transitions within the entity are compressed up to but not including any breakpoint action This corresponds to declaring that everything from a breakpoint action up to the next one is considered as an internal computation This in particular allows for compressions up to an event in a loop without unrolling this loop for the specification of the compression We believe that this is a useful compromise between the goal of a declarative intuitive easy to use specification language of services and the needs of the validation tools that have to work on these specifications 4
183. lied to all statements using guards 4 7 10 Loop Loop stmt rest sl return_sl stmt while Guard Body positiveGuards Guard negativeGuards Guard p_1 p_n n 1 p m apply adaptGuard to p_1 p_n and n 1 n_m positive branches i e Guard satisfied for i from 1 ton LHS state fact for this entity with step label sl state facts for the owners of variables appearing in p_i RHS state fact for this entity with step label branch sl 0 state facts for the owners of variables appearing in p_i add LHS p_i gt RHS renewPositiveFactsIn p_i to section rules in the translation FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 147 190 negative branches i e Guard not satisfied for i from 1 tom LHS state fact for this entity with step label sl state facts for the owners of variables appearing in n_i RHS state fact for this entity with step label succ sl state facts for the owners of variables appearing in n_i add LHS n_i gt RHS renewPositiveFactsIn n_i to section rules in the translation ParseCode Body branch sl 0 s1 ParseCode rest succ sl return_sl A while construct translates in a very similar way to the if construct two sets of rules are created one set of which leading to the body of the loop if the guard is satisfied and the other leading outside the loop if the guard is not satisfied Then the body is parse
184. listing trusted_agent root_ca issued root_ca gt cert ca pk ca issued ca gt cert A pk A issued ca gt cert A pk B issued ca gt cert i pk i issued c gt cert i pk i The CA signing the certificates of Alice and Bob in our example is an intermediate CA authorized by a superordinate trusted root CA A and B both trust the root CA as depicted in Figure 10 We declare the root CA as trusted by stating trusted_agent root_ca line 1 as fact Then we state as fact that the root CA has issued a certificate for the intermediate CA by saying issued root_ca gt cert ca pk ca line 2 Then we also declare lines 4 5 7 that the intermediate CA has issued certificates for A B and also the intruder i Then we let some non trusted party c also issue a certificate for i line 8 which however neither A nor B would accept entity Alice Actor B agent body if trusted_pk B Alice as sketched in above listing in line 4 and Bob accept a signed message only if the signer has a trustworthy certificate otherwise they refuse communication A trustworthy certificate has been directly or indirectly signed by a trusted CA To discover the chain of trust requires recursive verification of certificates until reaching the signature of a trusted CA or coming to the conclusion that no such CA can be found This is done via deduction by evaluating above clauses against the known facts For simplicity we n
185. locally so we specify the security goals as templates within Session and fill in these templates within Alice and Bob when they refer to the respective goals After the specification of Session s body we still within the definition of the entity Session specify our security goal templates as follows entity Session A B agent 4 body 1 goals secret_Na _ A B secret_Nb _ A B Alice_authenticates_Bob _ B gt gt A Bob_authenticates_Alice _ A gt gt B In lines 6 and 7 of the above listing of the Session s goal section the secrecy goals by the names of secret_Na and secret_Nb are specified as templates They require some still undeclared item to be kept secret between A and B A and B must fill in the placeholder for that item _ with Na and Nb respectively when they are actually requiring the security goal to be met The equivalent applies to the authentication goals by the names of Alice_authenticates_Bob and Bob_authenticates Alice in lines 8 and 9 of above listing These goals require that some hitherto undeclared item is transmitted in an authenticated and fresh manner gt gt from one party to the other thus allowing the receiving party to authenticate the sending party and offering replay protection at the same time In lines 8 9 10 and 11 of the listing of Bob s body in the previous paragraph these four security templates are referenced and filled in In line 8 the secrecy goal se
186. lowed for direct sub entities such that static and dynamic scoping coincide Symbolic entity generations introduced by any are a convenient shorthand for loosely instantiating an entity in the following sense the bound parameters of the entity as indi cated by the given list of variables allows to explore all possible values from the domain of their type which may be any subtype of message An optional guard which may refer to the variables listed constrains the selection This mechanism is typically used to produce so called symbolic sessions where the bound variables range over type agent such that unless further constraints exist their values include i the name of the intruder 3 11 Guards Formulas used as conditions in if while select and symbolic entity generation statements are called guards They may refer to the current state of the system via variables and facts for example peer A B amp dishonest 7A The symbol indicates implicit logical quantification and may yield to implicit variable assignment Within guards variable names may be preceded by to specify that during pattern matching each variable obtains a suitable value such that the overall condition is satisfied For each variable name occurring in a guard either all occurrences must be preceded by or appear without a At pattern positions where the value to be matched is irrelevant one may write a single ton
187. ly and differently from CCM they do not need to be defined via concrete implementations Translation of channel goals is discussed in 4 12 2 Here we focus on the translation of channels when used as an assumption which depends on the choice of the channel model as we discussed in detail in D3 3 2 In this case we take into account the send and receive predicates generated after the preprocessing phase described in 4 1 In order to make explicit that both the translation and the interpretation of such predicates can be different according to the channel model chosen let us illustrate the translation s at hand of a concrete example we proceed analogously for the other cases Each model introduces a number of symbols facts and rules necessary to express the different channels as defined in D3 3 Note that freshness is not supported for CCM ICM channels as assumptions while for ACM it is implied by confidentiality and weak confiden tiality Assume that the translation process has proceeded up to the point of producing a transi tion rule that includes an agent receiving a message M1 on a confidential channel from A and sending a message M2 to B on an authentic channel For CCM ICM let us further assume that the agent sends M2 under pseudonym P A gt Actor M1 Actor _ P gt B M2 while for ACM let us further assume that the reception is on channel chi and transmission is on channel ch2 chi gt confidential_to
188. make use of the authenticity assumption specified for all message transmissions by the on left hand side of the arrow in any statement of the form A gt B where A is the real sender name known to the receiver clatse nb 2 specification TLS_SessionsOrder_CCM channel_model CCM entity Environment symbols succ nat nat 4 workaround declaration should not be needed server agent symbols ServerSessions agent text nat set global for Server entity Session C S agent entity Client Actor S agent FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 81 190 symbols SessID text Counter nat PayloadC PayloadS text body SessID fresh secrecy_goal secret_SessID Actor Counter 0 start session Actor gt x S Counter succ Counter 1 PayloadC fresh Actor gt S SessID Counter channel_goal Client_TLS_Server Actor gt gt S S gt SessID Counter channel_goal Server_TLS_Client S gt gt x Actor Actor Counter succ Counter 2 PayloadC fresh Actor gt S SessID Counter channel_goal Client_TLS_Server Actor gt gt S S gt Actor SessID Counter channel_goal Server_TLS_Client S gt gt Actor false h for If the model checker does not here assert finished hh can be commented out to check body 1 of Session
189. mal methods for protocol analysis Our approach is to let an au tomated model checker do the hard work How do we proceed from above informal protocol sketch We now outline the procedure followed in the rest of this section Approach First we formalize the protocol in cooperation with the protocol expert who is familiar with the protocol and its typical deployment scenarios A useful modeling and discussion base are annotated sequence diagrams An automated model checker must be told explicitly what are the security goals of the protocol Therefore together with the protocol expert we specify the security goals of the problem Valuable discussion partners also are those parties that are to deploy the protocol Their security goals should be covered by the protocol Next we model the problem and the goals in ASLan Then we translate compile the problem into ASLan which is the language understood by the model checkers The compiled model we feed to the automated model checkers and interpret their feedback If a model checker detects an attack trace we correct the model and re check it Once no more vulnerabilities are found we fix the original protocol This approach is followed within this introductory example The Attacker Model In the common ASLan attacker model the attacker is The Network as sketched in Figure 1 The attacker is handed every message sent by the sender and forwards it to the recipient or not The attacker m
190. ments may be labeled with a goal name e g my_name My_term which is used as goal labels for channel goals and secrecy goals as described in 3 9 3 and 3 9 4 We denote the concatenation of messages M1 and M2 as M1 M2 Therefore it also associates to the right so M1 M2 M3 M1 M2 M3 Except when explicit equations are given for them Function calls and constructors like concatenation of messages are not really evaluated but are kept as kind of tags around their argument list To enhance readability for instance for functions that one would like to write as infix operators like e g the binary predicate weaker_than any function application of the form f X Y Z may alternatively be written in object oriented style as X gt f Y Z Variables of set type hold globally scoped references to the set they represent These set references may be copied and even passed as arguments of send and receive instructions If a reference gets known to the intruder he may modify the set by adding or removing the respective contains facts 33 Formally terms are interpreted in the quotient algebra 7 5 where E are the specified algebraic equations By default when no algebraic equations are specified all functions are uninterpreted i e in the free algebra 34 At the moment this is only implemented by CL AtSe FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and t
191. ments of the same kind that are defined in outer entities Moreover sub entities of a given entity may declare independent elements that happen to have the same name but which should not conflict or in other ways interfere with each other Because ASLan only supports a flat name space each hidden or potentially conflicting element must be renamed for instance by prepending the name of the entity in which it is defined in order to make them unique within the global scope of ASLan Hence the element is known under the new disambiguated name for all further translation steps and at the ASLan level Expansion of macros The specification is parsed and any term matching the LHS of a macro defined in the macros section is replaced by the corresponding RHS After this step the macros section can be removed Expansion of shorthands All function applications in object oriented style nota tion namely of the form t_1 gt func t_2 t_n are converted to the form func t_1 t_2 t_n For the special cases of send and receive operations where just two arguments are given i e the optional argument Actor has been omitted Actor is inserted in this step as an additional first argument In a similar way all bullet style transmission i e annotated channel facts are converted into the appropriate predicates as specified in Table 1 4 2 Translation of Entities For every entity at any level of nesting in the specification we declare in the tr
192. model ACM entity Environment symbols client server agent ch_c2s ch_s2c channel entity Session C S agent Ch_C2S Ch_S2C channel entity Client Actor S agent Ch_C28 Ch_S2C channel symbols Nc Ns text body Actor C_C25 gt S Nc S C_82C gt Actor Ns entity Server Actor agent Ch_C2S Ch_S2C channel symbols C agent Nc Ns text body C Ch_C2S gt Actor Nc Actor Ch_S2C gt C Ns body new Client C S Ch_C2S Ch_S2C new Server S Ch_C2S Ch_S2C body ch_c2s gt confidential_to server ch_s2c gt authentic_on server new Session client server ch_c2s ch_s2c FP7 ICT 2007 1 Project No 216471 A AN T SSAR 47 48 D2 3 update ASLan specification and tutorial 104 190 Property Fact Meaning Linked link ch_a2b ch_b2a This relation requires that the entity send ing messages over the channel ch_a2b is the same entity that receives messages from ch_b2a Table 4 Linked channel fact and its informal meaning Property Fact Meaning Bilateral bilateral_conf_auth The relation of the pair of channels ch_a2b and confidential ch_a2b ch_b2a a b ch_b2a for instance modeling a run of SSL TLS and in which entity a and b have a valid certificate authentic with each other Unilateral unilateral_conf_auth A pair of channels ch_a2b and ch_b2a where confidential ch_a2b ch_b2a b ch_a2b is confid
193. n Constraints can be defined as LTL formu lae We assume that the variables occurring in the constraints and in the LTL formulas in the goal section are disjoint Section Goals GoalsSection Security goals can be defined as attack states or by means of LTL formulas Section Intruder IntruderSection The rules and clauses in this section describe the abilities of the intruder namely composition and decomposition of known messages As these abilities are again independent of the service they are included in the prelude A 2 3 Constraints on identifiers All used identifiers must be different from the ASLan keywords step section intruder equal leq not state The identifiers for types used in declarations can only be those identifiers that have been introduced as type identifiers in the prelude Identifiers for opera tors are only those that have been declared in the signature section of the prelude as having range type message Similarly fact symbols are only the ones declared in the signature section of the prelude or the ASLan file as having range type fact The identifiers that name initial states rules or goals must be unique and distinct from all constants and variables and declared identifiers A 2 4 Constraints on variables For a rule declaration the variables in the variable list must contain exactly those variables that occur in the LHS and in the exists clause of the rule The variables appearing in the exists clause
194. n on the receiving side a variable M of type message can match Mi but also Mi Mj The receiver cannot determine where to split We can translate and check the above example with the given four element set for instance using Cl AtSe supplying the nb 4 option java jar aslanpp connector jar sets_concatenation aslan t o sets_concatenation aslan gas cl atse nb 4 f sets_concatenation aslan gt sets_concatenation atk java jar aslanpp connector jar sets_concatenation aslan ar sets _concatenation atk 2 6 Time out In this section we give an example of specifying a simple timeout mechanism in ASLan A common use of timeout is to enable an alternative action for an entity For instance Alice sends a message to Bob and expects to receive an acknowledgement from Bob saying that he has received the message If the acknowledgement message does not arrive in time Alice may timeout and do something else for instance raise an alarm We abstract away the actual amount of time the entity Alice would wait for the acknowledgement in this case and model the timeout simply as a non deterministic event After sending her message to Bob Alice starts an imaginary timer which we do not model explicitly The timer may go off at any moment after it has been initiated on which Alice introduces the fact timeout Meanwhile Alice may receive the acknowledgement message from Bob or she may timeout if the timer goes off before such an
195. n a child entity of the entity declaring the secrecy goal After binding an auxiliary local variable like IID nat to the instance ID of the parent entity which can be achieved by select on child IID IID we can dynamically add c to the set by introducing the fact secreti_set IID gt add c or remove B from the set by stating secreti_set IID gt remove B where the secret1 part is the name of the secrecy goal 3 10 Statements Statements may be the usual assignments branches and loops but also nondeterministic selections assertions the generation of fresh values and of new entity instances the trans FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 112 190 mission of messages i e send and receive operations and the generation or retraction of facts The select statement is typically used within the main loop of a server which handles a variety of potential incoming requests or other events such as timeouts It checks the guards given blocking as long as no guard is fulfilled then nondeterministically chooses any one of the fulfilled guards and executes the corresponding statement block The evaluation of the guard chosen may assign variables as described in 3 11 Assertions induce goals to be checked at the current position in the control flow Entity generation introduced by the keyword new or any instantiates sub entities This is only al
196. n a similar result between ICM and ACM Establishing such equivalence results is fundamental as they allow us to use each model interchangeably according to what fits best with certain analysis methods In this regard each of these models has its strengths e The CCM allows one to model channels within tools that do not have support for channels because it requires only the standard cryptographic primitives and the in truder deduction machinery that is integrated in all the back ends of the AVISPA Tool that are providing a basis for the AVANTSSAR platform Also it allows for using FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 135 190 the optimization that an insecure network and the intruder can be identified i e we have a compressed transition where the intruder sends a message that is received and answered to by the receiver and the intruder immediately intercepts this answer e The ICM is more helpful in a different class of tools where the number of transitions is less problematic but the complexity of terms is an issue Also it is the abstract reference model for our compositionality results between channels as assumptions and channels as goals e The ACM finally allows for arbitrary LTL constraints on the sending and receiving e g resilient channels i e every message is eventually received Thus the assumed security properties of the channels are expressed abstract
197. n and tutorial 131 190 M fresh then we create a new variable M_1 in the translation and express the fresh generation via the rule state _BidM Actor IID s1 BP M exists M_1 gt state _BidM Actor IID succ sl BP M 1 As for the variable assignment case if the generated value is assigned to a variable belonging to an ancestor the state fact of the latter must be changed instead O 4 7 4 Entity instantiation EntityGen stmt rest sl return_sl 4 stmt new entity EL t 1 a t n wyu IID fresh variable declare IID of type nat in section types in the translation LHS state fact for the current entity with step label sl state facts for the owners of variables appearing in t_1 t_n RHS state fact for the current entity with step label succ sl state facts for the owners of variables appearing in lo ton state fact for new entity instance such that its step label is sl_0 its instance ID is IID all parameters p_1 p_n set to t_1 t_n all variables v_1 v_m set to dummy of the right type add LHS exists IID gt RHS to section rules in the translation ParseCode rest succ sl return_sl Conceptually instantiating an entity corresponds to creating a new state fact for the instance running from this point on in parallel to all other entity instances in the system FP7 ICT 2007 1 Project No 216471 A AN T SSAR SEVENTH FRAMEWORK PROGRAMME
198. n nested sub entities which inherit the items of their outer entities The top level i e outermost entity usually is called Environment It serves as the global root of the system being specified similarly to the main routine of a conventional program Inside the environment normally we define an entity called Session A session contains communicating entities Such an entity is called Actor In our NSPK example a session is conducted between 2 actors called Alice and Bob Alice will initiate the NSPK protocol with Bob therefore she must be told which Bob to contact The environment can be instantiated as a process Inside it one or several sessions may be instantiated The sessions instantiate their associated actors which communicate with each other following the specified protocol In our example as sketched in Figure 5 the 5A channel model characterizes the basic communication model of the specification CCM cryptographic channel model stands for communication security implemented via encrypted and signed messages For more detail and other channel models see 3 8 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 17 190 NSPK aslan specification NSPK channel model CCM entity Environment entity Session A B agent entity Alice Actor B agent entity Bob A Actor agent body new Alice A BJ new Bob A B a body
199. n v 1 Available at www avantssar eu 2008 AVANTSSAR Deliverable 3 3 Attacker models Available at www avantssar eu 2008 AVANTSSAR Deliverable 5 1 Problem cases and their trust and security requirements Available at www avantssar eu 2008 AVANTSSAR Deliverable 2 2 ASLan v 2 with static service and policy composition Available at www avantssar eu 2009 AVANTSSAR Deliverable 2 3 ASLan final version with dynamic service and policy composition Available at www avantssar eu 2010 AVANTSSAR Deliverable 4 2 AVANTSSAR Validation Platform v 2 Available at www avantssar eu 2010 AVANTSSAR Deliverable 5 3 AVANTSSAR Library of validated problem cases Avail able at www avantssar eu 2010 AVISPA Deliverable 2 1 The High Level Protocol Specification Language www avispa project org 2003 AVISPA Deliverable 2 3 The Intermediate Format www avispa project org 2003 C Dilloway and G Lowe On the specification of secure channels In Proceedings of WITS 07 2007 D Dolev and A Yao On the Security of Public Key Protocols IEEE Transactions on Information Theory 2 29 1983 J Heather G Lowe and S Schneider How to prevent type flaw attacks on secu rity protocols In Proceedings of The 13th Computer Security Foundations Workshop CSF W 00 IEEE Computer Society Press 2000 G Lowe Breaking and fixing the needham schroeder public key protocol using fdr In Proceedings of TACAS 96 LNCS pa
200. n20 Nb n22 IID request Req 1 Wit 1 fresh_Bob_authenticates_Alice n20 Nb n22 IID request Wit 1 i auth_Alice_authenticates_Bob n7 Na n6 IID request Wit 1 i fresh_Alice_authenticates_Bob n7 Na n6 IID state_Bob i n6 IID 1 Wit 1 dummy_text dummy_text state_Environment root 0 1 witness Req 1 Wit 1 auth_Alice_authenticates_Bob n7 Na witness Wit 1 i auth_Bob_authenticates_Alice n20 Nb MESSAGES Wit 1 gt lt i gt n7 Na Wit 1 _pk i lt gt gt Req 1 n7 Na Wit 1 _pk Req 1 Req 1 gt lt Wit 1 gt n7 Na n20 Nb _pk Wit 1 lt i gt gt Wit 1 n7 Na n20 Nb _pk Wit 1 Wit 1 gt lt i gt n20 Nb _pk i lt Wit 1 gt gt Req 1 n20 Nb _pk Req 1 As you can see CL AtSe was able to find an attack path to violate some security goal This it indicates at the very beginning under SUMMARY ATTACK_FOUND After some statistics about itself and the present model check the model checker lists a protocol of the steps it performed while checking our model The description of each step consists of a triple of STATES CLAUSES and STATEMENTS The STATES section lists all then existing entity instances and their current parameter values The CLAUSES section would provide information about Horn Clauses which however in our NSPK example we did not use So for the present this section is empty The STATEMENTS section lists the statements that were exe
201. nce in the clause clauses certAuthorityTrust A forall B K trusts Actor A isPK B K isCA A the variables B and K are interpreted universally That is the rule stipulates that if A is a certificate authority then he is trusted on stating that K is a public key of B for any K and B We create a set PolicyPredicates which stores all implicit facts i e iknows and all other predicate symbols appearing in the head of the clauses This set serves in later phases of the translation to ensure that no implicit fact except for iknows is introduced explicitly and no implicit fact is retracted explicitly cf A 2 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 127 190 4 5 Translation of Equations The syntax for equations in ASLan closely resembles the syntax for the equalities in ASLan and their semantics are identical therefore their translation will consist in minor syntactic adjustments applying a procedure for conversion of terms that we will present in 4 9 and transcription in the section equations of the file 4 6 Representing the Control Flow As anticipated in 4 2 we represent the control flow of the entity via a step label stored in its state fact We introduce here an abstract encoding for step labels which we will refer to in the next phases of the translation procedure Note that step labels are symbolic and do not need to be numbers We assume a pr
202. nclude in their bodies side conditions like in equalities and may be recur sive though this might lead to non termination of some model checking tools 3 6 Declarations Within an entity declarations of elements like types variables constants functions macros clauses and equations may be freely mixed Types and equations always have global scope i e visibility and effect Types may be declared in any entity but must not be re defined in sub entities All other declarations have lexical scope i e the declared elements are visible and effective only in the declaring entity and in sub entities unless the element is hidden there by a new declaration of a homonymous element of the same kind Types may have subtypes e g the built in subtype relation agent lt message means that any value of type agent may be used in a context where a value of type message is expected The type message includes all those values that may be sent over the network in particular concatenation and tuples of sub messages For atomic values in messages it may be more efficient for model checking with SATMC to use the subtype text Sets are not a subtype of message such that they cannot be directly sent as messages but see 2 5 for possibilities how to deal with this The only types that have implicit type parameters are tuples e g agent message and sets e g nat set There are also are compound types which are a shorthand for specifying stru
203. nd tutorial 174 190 Let C be a conjunction of possibly negated atomic and ground conditions We say that C holds if and only if 1 C is of the form equal t t2 and t amp ta 2 C is of the form leq t t2 where the ground terms t and tz evaluate as expected to n and ng N and n lt na 3 C is of the form not cy and cy does not hold and 4 C is of the form c cz and both c and cz hold Let H be the set of clauses defined in the section ClausesSection For a state S the closure of S with respect to a set of clauses H denoted is the smallest set containing S and satisfying the following property V A Ai An H Yo LU Aio C S Ao S P 1 lt i lt n where is any substitution function mapping the set of variables in var A UU lt i lt n var Ai to the set of ground terms The transition relation is defined as follows e for all S S S which models stuttering and e for all S S S with S as follows if and only if there exists a rule PF NF amp PCKNC 4V R in the section RulesSection where PF and NF are sets of positive facts and negated facts respectively PC is a conjunction of positive atomic conditions and NC is a conjunction of negative atomic conditions and a substitution o v1 Un gt Ts where v U are the variables that occur in PF or in PC such that PFo C S PCo holds NFoo N S 0 for all substitutions o such
204. new Client C S entity Server Actor agent Sessions SessID Counter SessID Counter SessID Counter SessID Counter Once this pseudo attack has been shown gt S SessID Actor SessID Counter PayloadC PayloadC Payloads Payloads PayloadC PayloadC Payloads Payloads excutability testing find an attack at least the model has an executability problem the assertion for the other goals agent text nat set FP7 ICT 2007 1 Project No 216471 SEVENTH FRAMEWORK PROGRAMME A ANTSSAR D2 3 update ASLan specification and tutorial 82 190 symbols C agent SessID text entity Thread Actor C agent SessID text Sessions agent text nat set symbols N nat PayloadC PayloadS text body 4 while true select on C gt Actor SessID N PayloadC amp Sessions gt contains C SessID 7N channel_goal Client_TLS_Server C gt gt Actor SessID N PayloadC PayloadS fresh Actor gt C SessID N Payloads channel_goal Server_TLS_Client Actor gt gt C SessID N PayloadS Sessions gt remove C SessID Sessions gt add C SessID succ N body 1 of the Server while true select 4 on C gt Actor C SessID 0O Q Server learns C here Sessions gt contains 7C SessID secrecy_goal secret_SessID Actor C SessID Sessions gt add C SessID succ 0
205. noninvertible password agent agent text entity Session C S agent 4 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 77 190 entity Client Actor S agent symbols Payload text body Actor gt S login Actor shared_secret password Actor S S gt Actor ok Payload fresh Actor gt S secure_transmission Payload entity Server C Actor agent symbols Payload text CP public_key pseudonym of C body CP gt Actor login C Server learns C here shared_secret password C Actor checks password proceeds only if fine Actor gt CP ok CP gt Actor secure_transmission Payload body of Session iknows password i S intruder knows its own password iknows password C i dishonest server knows client password we assume unilaterally authenticated TLS from C to S new Client C S new Server C S goals shared_secret _ C S secure_transmission _ C gt S body of Environment any C S Session C S where C S After the client s identity been verified by the server assuming that the client did not share its password with anyone else the unilateral authentication has FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 78 190 been effectively transform
206. npp connector jar gas timeout aslan J J PP J 8 FP7 ICT 2007 1 Project No 216471 SEVENTH FRAMEWORK PROGRAMME A ANTSSAR D2 3 update ASLan specification and tutorial 64 190 o timeout aslan cl atse f timeout aslan gt timeout atk java jar aslanpp connector jar timeout aslan ar timeout atk The goal no_alarm does not hold for this model as confirmed by CL AtSe You may want to try the following two experiments First we are curious if really the acknowledgement from Bob can arrive before the timeout occurs For this we can check the model against the following goal no_ackrcvd no_ackrcvd ackrcvd To try this in above listing you comment out the goal no_alarm in line 47 and comment in the goal no_ackrcvd in line 46 Then you re check the model as described Indeed the acknowledgement message in this specification may be received by Alice before the timeout Therefore the goal no_ackrcvd too is unsatisfied CL AtSe confirms that no_ackrcvd can be violated and provides the corresponding attack trace Now we at last want to check what happens if Bob never sends any acknowledgement at all For this in above listing we prevent Bob from returning a receipt by commenting out his reply in line 36 Then the goal no_ackrcvd holds safe in the model If you re check this modified model now Cl AtSe confirms to you that it found no attack anymore 2 7 Policies In 2 1 7 we have already seen how we
207. nt IID n4 IID SL 3 A A 4 B Req 1 Session Actor dummy_agent IID n5 IID SL 3 A Wit 1 B i Alice Actor Wit 1 IID n6 IID SL 5 B i Na n7 Na Nb n20 Nb Bob Actor i IID n6 IID SL 1 A Wit 1 Na dummy_text Nb dummy_text Alice Actor A 4 IID n22 IID SL 1 B Req 1 Na dummy_text Nb dummy_text Bob Actor Req 1 IID n22 IID SL 6 A Wit 1 Na n7 Na Nb n20 Nb CLAUSES VIOLATED auth_Bob_authenticates_Alice IID n22 IID Msg n20 Nb Req Req 1 Wit Wit 1 on line 48 EXPLICIT child 0 n4 IID child 0 n5 IID child dummy_nat 0 child n4 IID n22 IID child n4 IID n22 IID child n5 IID n6 IID child n5 IID n6 IID dishonest i iknows ak iknows atag iknows ck iknows n7 Na n20 Nb _pk Wit 1 iknows n20 Nb _pk i iknows n7 Na Wit 1 _pk i iknows ctag iknows hash iknows i a SEVENTH FRAMEWORK FP7 ICT 2007 1 PROGRAMME Project No 216471 A AN T SSAR 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 D2 3 update ASLan specification and tutorial 27 190 a SEVENTH FRAMEWORK PROGRAMME iknows inv ak i iknows inv ck i iknows inv pk i iknows n20 Nb iknows n7 Na iknows pk iknows root iknows stag iknows A iknows B iknows A iknows B request Req 1 Wit 1 auth_Bob_authenticates_Alice
208. ntended only for debugging purposes ar analysis result ANALYSIS_ RESULT Translate back to ASLan the anal ysis result given by a backend on an ASLan specification that was generated by trans lation from ASLan A file must be provided that holds the analysis result given by the validation platform gas goals as attack states Render ASLan goals as ASLan attack states when ever possible When an ASLan goal cannot be rendered as an ASLan attack state for example if it uses LTL operators then it will be rendered as an ASLan goal and a warning will be issued gv graphviz DIR Output Graphviz dot files with the transition rules of each entity The files are written to the specified directory If the dot program is available in the PATH then also output png files with the transitions rules Otherwise you can convert the dot files into images manually See http www graphviz org for details h help Show help hc horn clauses level ALL NPI NONE Makes it possible to leave out from the generated ASLan output some or all of the Horn clauses Can be one of ALL all Horn clauses are included in the output NPI the Horn clauses related to public and invertible functions are left out of the translation or NONE all Horn clauses are left out of the translation The default value is ALL o output OUTPUT_FILE Send output to the specified file instead of stdout opt optimization lev
209. ntiality protected body new Alice A B 42 According to current translator restrictions only direct sub entities are supported for secrecy goals FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 111 190 new Bob A B goals secret_Nonce _ A B The terms given for the same secrecy goal in the entities involved may look different e g due to different variable names like in the above example Nonce vs N_A but their actual values should of course be equal Note that confidential transmission of a value between two parties can also be stated as a channel goal but the secrecy goal is more general it may be used to state the value is shared between more than two parties In case a more complex secrecy goal cannot be expressed given the above syntactic restrictions advanced users may directly use the formulation using secret facts as described in 4 12 3 So far the translator accepts as agent terms in secrecy goals only constants or variables In case a more complex term is needed one may write e g body B peer A new Alice A B new Bob A B goals secret_Nonce _ A gt x B currently cannot write peer A instead of B here It is even possible to dynamically change the set of agents that may know the value For example consider the secrecy goal secreti _ A B and suppose we want to manipulate the set of agents withi
210. ntities The AVANTSSAR Platform can indeed help the modelers and designers to debug their synchronization mechanism In the example given above for instance using authenticated channels gt to communicate synchronization messages is essential for the correctness of the specification In particular if any of sync1 or sync2 is sent over insecure channels the attacker can fake them hence subverting the goal no_alarn e If sync1 is sent over an insecure channel then the attacker can fake this message hence enabling Alice to use SetGlobal while it still holds the empty set that is to before Bob inserts e1 in this set Recall that actions of Alice and Bob are interleaved in the semantics of ASLan see A 3 Then Bob and Alice would synchronize on sync2 while SetGlobal meanwhile contains e1 Consequently the no_alarm assertion would be violated in the state of Bob You are encouraged to try this out The attack has been reproduced using CL AtSe e If sync2 is sent over an insecure channel then the attacker can fake this message hence causing Bob to check the content of SetGlobal before Alice assigns the empty FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 57 190 set to this set The fact that Bob and Alice would synchronize on sync1 obviously enables the no_alarm assertion to be violated in Bob s state You may want to try this The attack has been reproduced using CL AtSe
211. o find whether that element from MySet1 is in MySet2 as well Just as we wanted to Smart Yes IsEqual Two sets S1 and S2 are equal if and only if S1 is a subset of S2 and S2 is a subset of S1 Checking equality can therefore be reduced to computing in both directions the subset relation which can be done as described in the previous paragraph We first do it the efficient way nonpublic nonMutualSubset fact initially fact is not set MySeti gt isEqualTo MySet2 if MySet1 gt contains 7E MySet2 gt contains 7E MySet2 gt contains E amp MySet1 gt contains E nonMutualSubset assert equal_test nonMutualSubset Again the model checker being challenged to violate the property of the mutual subset property will search for ways to find elements in MySet1 or MySet2 to violate this property That was easy And sufficient If we want to do it the hard way querying for equality manually but nevertheless in cluding some optimzations we can do as follows isSubset isEqual fact MySetIntersection Provide a fresh location isSubset initially assume the subset property isEqual retract isEqual initially assume sets are not equal FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 47 190 MySeti gt isSubsetOf MySet2 while MySet1 gt contains 7E amp isSubset if MySet2 gt contains E retract isSubse
212. oadS checks nonce FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 72 190 entity Server C Actor agent while true select on gt Actor S learns C here 7C Client_HTTPS_Server Nc PayloadC PayloadS lt gt Actor gt C reflects nonce Server_HTTPS_Client Nc PayloadS goals Client_HTTPS_Server _ C gt x S Server_HTTPS_Client _ S x gt gt C The goals specified here reflect many aspects of what this model of the TLS channel provides The client request is confidential to the server the response is authentic and replay protected However the fact that different parallel session are distinguished thanks to the nonce is not captured by the goals Note that the server accepts any unauthenticated client learning the alleged client name C in the request message Therefore in the backwards direction confidentiality would not make sense 2 9 4 Weak Client Authentication The next aspect we model is a form of weak authentication that the response can only be received by the client who sent the request It is common that the client does not possess a certificate and thus cannot authenticate itself directly to the server However even not authenticated TLS ensures that nobody else can read the response In CCM ICM this is modeled using the concept of pseudonymous secure channels the client not authenticated by its real ident
213. oals A secrecy goal has the form FP7 ICT 2007 1 Project No 216471 A AN T SSAR a o SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 110 190 name _ A1 A2 where the goal name is augmented with a parameter placeholder _ to indicate that in sub entities the goal name will appear again in the form of a goal label with a term as its argument Its interpretation is that the values annotated with the goal labels must be known only to the agents referred to in the set literal A1 A2 All terms A1 A2 etc must re appear as actual arguments in the instantiations of all sub entities sharing the secret In each sub entity whenever a term labeled with the goal name is evaluated the set of the knowing agents is computed from the current values of those parameters that have been matched as just described The goal labels should be given in all sub entities that may know the secret value as early as possible for instance when the value is produced or learned by the respective entity instance for example entity Session A B agent entity Alice Actor B agent symbols Nonce message body secret_Nonce Nonce fresh Actor gt B Nonce send Nonce to B somehow confidentiality protected entity Bob A Actor agent symbols N_A message body A gt Actor secret_Nonce N_A receive Nonce from A somehow confide
214. ob notation 2 it reads as A gt B Na A _Kb A lt B Na Nb _Ka A gt B Nb _Kb FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 10 190 Here Na and Nb stand for nonces i e non guessable random values produced freshly by Alice and Bob respectively Line 1 says that Alice sends her nonce and her name to Bob readable for B only A invents Na and together with her name sends it via gt to B encrypted with his public key Kb The in Na A means concatenation of two message parts Lines 2 and 3 specify analogous message transmissions B invents Nb and sends it to A along with Na to prove to her his ability to decrypt with his private key inv Kb A confirms Nb to B to prove to him her ability to decrypt with inv Ka Line 2 implies that A checks the value Na she receives similarly line 3 implicitly requires that B checks the value Nb he receives At the end of the protocol A and B are supposed to know each other s identities and know both Na and Nb These nonces may not get known to attackers They must be kept secret between A and B 2 1 2 Automated Security Analysis Is the protocol described above secure Can it be attacked Experience shows that man ual analysis is cumbersome and may overlook more complex to exploit vulnerabilities this protocol is famous precisely for this reason and has become the standard example for the importance of the use of for
215. ody of Session issued ca gt cert A pk A Alice s cert signed by CA issued ca gt cert A pk B Bob s cert signed by CA new Alice A B new Bob A B goals secret_Na _ A B Okay secret_Nb _ A B Attack found hhh May comment out the above secrecy goals such that hhh the attack is printed on authentiation Alice_authenticates_Bob _ B gt gt A Okay Bob_authenticates_Alice _ A gt gt B Attack found end entity Session FP7 ICT 2007 1 Project No 216471 A AN T SSAR SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 36 190 body of Environment trusted_agent root_ca We accept root_ca as trusted issued root_ca gt cert ca pk ca Intermediate ca issued ca gt cert i pk i i s cert signed by CA issued c gt cert i pk i Fake intruder certificate Two sessions needed for Lowe s attack any A B Session A B where A B amp A l root_ca amp B root_ca amp Al ca amp B cas any A B Session A B where A B amp A l root_ca amp B root_ca amp Al ca amp B ca If A Band i are granted a trusted certificate the well known Lowe attack 13 succeeds If for instance the intruder i does not have a trusted certificate then A refuses to communicate with i and no attack can take place Please note that on translating above listing you will receive a warning on horn clauses bein
216. of type 7 set parameterized by the instance ID of the entity which owns the set literal Then we substitute T by sf IID and add to the RHS of R the facts contains sf IID T_1 contains sf IID T_n e T i e T pattern matches anything which is allowed only in guards i e on the LHS of R In this case we just create a fresh variable name V and replace T by V e T V ie T represents an assignment of V by pattern matching which is allowed only in guards i e on the LHS of R We add the state fact of the owner of V to both the LHS and RHS of R where we replace the variable name V in the left state fact by a fresh variable name V For example if p V then q V is translated to state_X V MV gt State _X V p V q V e T T_1 T_n i e Tis the application of a function f to the terms T_1 T_n In the general case f will be left as is and we need only apply the terms translation procedure recursively to T_1 T_n As to the case where f is a send or a receive its translation will change according to the channel model employed discussed in depth in 4 7 6 4 10 Translation of the Body Section Now that we have introduced the procedure ParseCode parsing the Body section is straight forward In particular we just need invoke ParseCode Stmts sl_0 null where Stmts is the body and s1_0 the initial step label while no return step label is provided being this the main block o
217. of type agent Actor is used to refer to herself while B is the name of the party she is supposed to connect to The Bob entity obtains the name of Alice via the first message received The variables Na and Nb of the general type message are used to store the nonces produced by Alice and Bob respectively There are secondary secrecy goals expressing that the values of both variables are secrets shared between the two parties The primary security goals are that Alice strongly authenticates Bob and vice versa agreeing on the nonces A statement like B gt Actor Na Nb _pk Actor reads as follows the current agent Actor which is Alice receives a message from B encrypted with the public key of Actor containing three values Alice learns the value of Nb at this point while she already knows Na and thus can check if she received the correct value which is used to identify her session with Bob Note that this specification contains details not expressible in the Alice Bob notation how and when values like nonces and agent names are computed and checked and which sessions are created Moreover it contains several secrecy and authenticity goals 3 2 Specifications An ASLan specification of a system and its security goals has a name which should agree with the file name it is contained in and contains the declaration of a hierarchy of entities described in detail below An entity may import other entities contained in separate files
218. ons as well as confidentiality in the opposite direction Since both the clients and the server threads increase the sequence number upon each reception and the sequence number is part of the channel goals this also checks for the preservation of the message order in both directions Of course apart from the replay protection aspect the channel goals are obviously fulfilled by construction of the channels themselves To implement the session database we use sets With the definition Sessions agent text nat set we specify that our session database will hold client session identifier and current sequence counter for each session With Sessions gt add C SessID N we can add an entry to the database with Sessions gt remove C SessID N we can remove an entry and with 22The way to achieve replay protection in CCM is not that straightforward in particular from the clients to the server threads Indeed an earlier version of this model had a bug which lead to a violation of the freshness property found by CL AtSe The problem occurred because multiple instances of our single server each had their own session database To fix this problem all server instances now share the same session database 3The distinction between the channels as assumptions and the corresponding communication goals would be more clear if in the model there was a distinction between the implementation of the TLS channels and their use at application level
219. ons please note that e depth sets a limit to the maximum search depth on the tree of reachable states This obviously implies a limitation on the obtained result that is obtain ing NO_ATTACK_FOUND by setting depth to n does not mean that no attack will occur while checking the specification with an higher depth i e n 1 e trace can be used to select a specific trace in the reachable states tree Note that the tree may not be balanced i e nodes probably have not a common degree This means that trace 0 3 2 1 may return a partial trace selecting the first branch starting from the root then the fourth one the third one and finally the second available but the partial trace trace 0 3 2 2 may not exist causing OFMC to return an error FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 184 190 Reserved keywords While using the tool consider also that specifications must not contain new definition of default functions nor misuse reserved keywords that are managed in a special way by the tool Keywords reserved for internal usage by OFMC or at which particular meaning has been already assigned and thus cannot be freely used by users are e The set of all terminal symbols of the ASLan and ASLan syntax For a complete list see 3 12 and A 2 e The set of all identifiers and symbols defined in the ASLan prelude For a complete list see 3 13 e apply pair give
220. ons that we have considered FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 167 190 A AStLan This appendix describes the syntax and semantics of ASLan the low level input language for the back ends of the AVANTSSAR Platform We proceed as follows In A 1 we motivate why and describe how ASLan extends and refines the specification language Intermediate Format IF of the AVISPA Tool 9 In A 2 we give the syntax of ASLan and we then describe the semantics of the language in A 3 Background on ASLan The first version of ASLan called ASLan v 1 was described in deliverable D2 1 1 and then it was extended and called ASLan v 1 1 in deliverable D2 2 4 In this deliverable we refine ASLan in particular with respect to the notion of dynamic policies We introduce implicit closure of states under policy rules which allows us to specify the revocation of policy facts in ASLan in a natural way ASLan is defined by extending and refining the Intermediate Format IF 9 a specification language that several of the partners of the AVANTSSAR consortium developed in the context of the FP5 project AVISPA IF is an expressive language for specifying security protocols and their properties based on set rewriting Moreover IF comes with mature tool support namely the AVISPA Tool and all of its back ends which provide the basis for the back ends of the AVANTSSAR Platform that we ha
221. ove as constraining all goals and attack states or if they are interpreted as constraining system execution i e the model itself The aim is actually to do the latter which allows for a more efficient implementation because traces not conforming to the constraints do not need to be produced and checked for violations of A 3 4 Typing Types in our specification language serve two main purposes First like in programming languages types can be very helpful to avoid mistakes in the specification Second typing can help the back ends to reduce the size of the transition system being analyzed by excluding the ill typed actions of the intruder While this in general means a restriction that can exclude attacks the correctness of a typed model implies the correctness of its untyped version 12 Moreover the user may also choose to deliberately neglect type flaw attacks A typed specification can be analyzed in an untyped model i e the specification contains the types to check that the specification is well formed but the validation is performed ignoring the types For these reasons we formally define the type system of an ASLan as follows e Ifa model contains a set of basic types 1 n such as agent and nonce we assume that there exists an infinite number of constants of each such type and write Cg for each such set e We assume that Cg N Ca for 6 4 b2 Note that Cg is only part of all values that have type this lat
222. ow this operation is done only when the option not _hc is provided in stead of just refusing horn clauses using such tests Note that no false feeling of security can appear here This option might be activated by default in a near future Usage C1 AtSe options f file files files Name of the IF ASLanvi files to process Note HLPSL files allowed if hlpsl2if is available Multiple files allowed Default is standard input f file Name of a specification file to process Same as files u V Do not take term types into account Write the attack to file atk Print more output informations same as of if Expert Long options nb n Maximum number of times that a transition can be run in a trace The fefault is 3 for IF and 1 for ASLan free Uses a free pairing symbol default for typed model assoc Uses an associative pairing symbol default for the untyped model typed Use term types as defined in the spec default untyped Do not take term types into account short Perform breath first search minimal attack a SEVENTH FRAMEWORK PROGRAMME FP7 ICT 2007 1 Project No 216471 A AN T SSAR D2 3 update ASLan specification and tutorial 187 190 of str ASLan if if if if brief out dir d ns opt noopt verbose noexec col n bench ASLan if lvl n store split he str btd blr btd not_h
223. p label A redundant guard is a guard which is either always true or always false Removing empty transitions and redundant guards alters the semantics of the ASLan model with respect to the neXt and Yesterday LTL operators As an example lets consider the following ASLan code body M fresh while true Actor gt B M Without optimizations the generated set of transition rules is state_Alice Actor IID 1 B M exists M_1 gt state_Alice Actor IID 2 B M_1 state_Alice Actor IID 2 B M true gt state_Alice Actor IID 3 B M true state_Alice Actor IID 3 B M FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 163 190 gt state Alice Actor IID 4 B M iknows M state Alice Actor IID 4 B M gt state Alice Actor IID 2 B M state Alice Actor IID 2 B M not true gt state_Alice Actor IID 5 B M After eliminating empty transitions and redundant guards the set of transition rules becomes state_Alice Actor IID 1 B M exists M_1 gt state_Alice Actor IID 2 B M_1 state_Alice Actor IID 2 B M gt state_Alice Actor IID 2 B M iknows M Empty transitions Most transition rules generated by the translation procedure contain in their LHS and RHS state facts that refer to the same entity This means that the transition expresses some progress in the state of an entity We can writ
224. r Ch_52C gt C ok C Ch_C2S gt Actor secure_transmission Payload body of Session iknows password i S intruder knows its own password iknows password C i dishonest server knows client password Ch_C2S fresh Ch_S2C fresh we assume unilaterally authenticated TLS from C to S unilateral_conf_auth Ch_C2S Ch_ 2C C S new Client C S Ch_C2S Ch_S2C new Server C S Ch_C2S Ch_S2C J goals shared_secret CJ Os SJ secure _transmission _ C gt S body 1 of Environment any C S Session C S where C S After the client s identity has been verified like in the CCM variant we again state and check the goal client_authentication If we did not want to implement the client authentication we could have started with the stronger channel assumption bilateral_conf_auth Ch_C2S Ch_S2C C S for ACM or non pseudonymous secure channels for CCM FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 80 190 2 9 6 Dynamic sessions and message order preservation If a dynamic session concept is required and if we need to ensure message order preservation as provided by TLS we may proceed as outlined here We model the TLS concept of a session by dynamically creating session identifiers and including these in all messages belonging to the session To additionally ensure message order preservation the
225. r also that specifications must not contain new definition of default functions nor misuse reserved keywords that are managed in a special way by the tool Keywords reserved for internal usage by SATMC or at which particular meaning has been already assigned and thus cannot be freely used by users are e The set of all terminal symbols of the ASLan and ASLan syntax step section intruder equal leq not state goal For a complete list see 3 12 and A 2 e The set of all identifiers and symbols defined in the ASLan and ASLan prelude e apply pair witness wrequest request PreludeK PreludeM PreludeM1 PreludeM2 PreludeM3 Xvar s s nat gt nat has has agent message gt fact B 3 OFMC This section sketches how to use the model checker OFMC and the various options avail able to fine tune the behavior of OFMC as well as the various specific characteristics and idiosyncrasies of this backend By launching OFMC with help the following text is displayed Options numSess lt INT gt specify the number of sessions for an AnB spec ot IF do not check but produce only AVISPA IF ot Isa generate a fixedpoint proof for Isabelle OFMC of if standard output format from the Avispa project FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 183 190 of aslan Standard output format from the Avantssar project fp run only in fixedpoint modu
226. r processes or the intruder may make progress This gives rise to the following issues e Race conditions may appear in case of shared knowledge e g all instances of a service running on the same server accessing its database If we do not want to explicitly specify mutual exclusion algorithms within the model to prevent race conditions we thus need to be able to specify that certain sequences of transitions are atomic This is of course an abstraction step that the specifier may choose to use at the risk of losing certain behaviors of the model e On the practical side even for relatively small processes this fine grained model pro duces a large set of interleavings even for a few processes Specifications can thus easily FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 160 190 get infeasible for the validation tools Note that in many cases these interleavings are irrelevant because they concern internal computations of a service and the relative ordering with other internal computations is not really relevant On the other hand it is almost impossible to determine which interleavings could give rise to new attacks on the tool side For this reason we introduce here the concept of step compression allowing modelers to consider different coarser granularities for their models The idea is that some actions instructions in the ASLan code can be considered internal and not re
227. r syntactic restrictions on variables but not on singleton s They apply after constructing the disjunctive normal form DNF of the guard which among others expands implications of the form P gt Q as P Q e variables must not occur as arguments of negated facts e In the condition of an if or while statement the sets of variables occurring as arguments of facts must be pairwise disjoint i e no variable may appear in more than one conjunct of the DNF This rules out the occurrence of variables like X in multiple facts e g if fact1 X fact2 X Y because their negation in the else branch would require a quantifier namely exists X fact1i X amp fact2 X Y If needed the condition can be re phrased using an auxiliary Horn clause e g aux_fact12 X Y facti2 X Y facti X amp fact2 X Y 3 12 Grammar in EBNF The more or less context free aspects of the ASLan grammar are defined using an Extended Backus Naur Form EBNF where X Y stands for one or more occurrences of X separated by Y e g Term can be expanded to Term Term Term Context dependent restrictions are stated to the right of the respective BNF rule as informal text that is preceded by the symbols MainSpec specification Name channel_ model CCM ICM ACM EntityDecl Module EntityDecl EntityDecl entity UpperName Params 4 Imports
228. ranslation a set of auxiliary events modeled as ASLan facts of the service execution as an interface between the concrete service and the general goals The use of such aux iliary events is common to several approaches including most notably AVISPA s IF and Casper 15 More specifically we consider the following kinds of fact symbols witness agent agent protocol _id message gt fact request agent agent protocol_id message nat gt fact secret message protocol_id agent set gt fact where the protocol_id type is used to hold an identifier for the particular goal These events provide an interface over which we define service properties in LTL formulae Each specification of a channel as a goal as described in 3 8 implies the creation of such events within the execution of a particular entity in particular the translation to ASLan decorates appropriate transition rules with these facts as described here Remember that channel goal labels can be used only in the context of a transmission statement The auxiliary events are used depending on the kind of the channel e If the channel is authentic there is a bullet at the left of the arrow then the witness and request events are used e If the channel is authentic and fresh the arrow is double headed then an additional rule involving request is used e If the channel is confidential there is a bullet at the right of the arrow then the secret event
229. rastructures We assume that A and B and i have been issued Public Key certificates by a Certificate Authority CA A public key certificate is an electronic document that binds a name to a public key in a trustworthy manner Public key certificates are signed by a trusted certificate authority CA after the CA has verified the data of the applicant e g by checking their passport When validating a public key certificate one must check 13These are extensions of classical Horn clauses the syntax of the rules resembles Prolog FP7 ICT 2007 1 L Project No 216471 A ANTSSAR CONDO KWH EH Be eee ee O 39M Raya Nooo D2 3 update ASLan specification and tutorial 32 190 Validity Range Normally the Valid From and Valid To fields in the certificate can be compared to a reference time Revocation State A certificate may be revoked before it expires e g because an employee leaves the company A check against a blacklist or directory should help here Chain of Trust The certificate must be signed by a trusted party Especially in large PKI structures trust may be indirect e g a root CA signs a subordinate CA which in turn signs end user certificates Directories may help to discover chains of trusts Purpose A certificate is issued for a certain certificate use e g email signing file encryp tion client authentication certificate signing etc The relying party must check the certificate s signed p
230. re channel and is controlled by a Dolev Yao intruder The other properties of the channels FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 102 190 Property Fact Meaning Confidential confidential _to ch B A channel ch provides confidential ity if its output is exclusively acces sible to the specified receiver B Weakly weakly_confidential ch This is the relaxed notion of confi confidential dential channel A channel ch pro vides weak confidentiality if its out put is exclusively accessible to a single yet unknown receiver Authentic authentic_on ch A A channel ch provides authenticity if its input is exclusively accessible to the specified sender A Weakly weakly_authentic ch This is the relaxed notion of au authentic thentic channel A channel ch pro vides weak authenticity if its input is exclusively accessible to a single yet unknown sender Resilient resilient ch The channel ch is normally opera tional but an attacker can succeed in delaying messages by an arbi trary but finite amount of time In other words a message inserted into a resilient channel will eventu ally be delivered Table 3 Properties channel facts and their informal meaning that are currently supported are given in this section In Table 3 for each channel property the corresponding fact and an informal description are reported The
231. re already familiar with programming languages e Modularity is supported by the use of entities Each entity is specified separately and can then be instantiated multiple times and composed with others This allows the specifier in particular to localize policies in each entity by clarifying for instance who is responsible to grant or deny authorization as well as the various trust relationships between entities e There is an intuitive notation for channels which may be used both as assumptions and as service goals and provides a simple but powerful way to specify communication and service compositionality FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 8 190 The AVANTSSAR Platform 6 supports ASLan via a connector that works in two directions it translates ASLan specifications to ASLan and translates attack traces from ASLan level to ASLan level Structure of the document This document is self contained in terms of ASLan and ASLan In order to facilitate its use for ASLan modelers we start by an ASLan tutorial in 2 illustrating to newcomers the common usage of ASLan and the related AVANTSSAR tools via examples that contain typical specification patterns Next comes a detailed intro duction to the ASLan concepts and syntax in 3 The formal semantics of ASLan is defined in 4 via a procedure for translating ASLan specifications into ASLan spec ifi
232. redDB Unsafe aslan cl atse SharedDB Unsafe aslan gt SharedDB Unsafe atk java jar aslanpp connector jar SharedDB_Unsafe aslan ar SharedDB_Unsafe atk the model checker reports the expected attack Please note that here the model checker uses A 1 to refer to the instance A of Alice and Actor 0 to refer to the instance B of Bob INPUT SharedDB_Unsafe aslan SUMMARY ATTACK_FOUND STATES Alice Actor A 1 IID n2 IID SL 5 B Actor 0 Nonce n3 Nonce SharedDB Actor 0 n7 Nonce 1 A 1 n3 Nonce 0 Bob Actor Actor 0 IID n2 IID SL 7 A A 1 Nonce n7 Nonce SharedDB Actor 0 n7 Nonce 1 A 1 n3 Nonce 0 CLAUSES STATEMENTS g set_i ni IID gt contains Actor 0 n7 Nonce 1 line 26 set_1 n1 IID gt contains Actor 0 n7 Nonce 1 line 27 f Alice n2 IID Nonce n5 Nonce fresh on line 29 set_1 n1 IID gt contains A 1 n5 Nonce 2 on line 30 s A 1 gt Actor 0 n5 Nonce on line 31 STATES Alice Actor A 1 IID n2 IID SL 10 B Actor 0 Nonce n5 Nonce SharedDB A 1 n3 Nonce 0 A C1 n5 Nonce 2 Bob Actor Actor 0 IID n2 IID SL 7 A A 1 Nonce n7 Nonce SharedDB 1A 1 n3 Nonce 0 A 1 n5 Nonce 2 CLAUSES VIOLATED test_sharedDB_B Actor Actor 0 IID n2 IID Nonce n7 Nonce SL 7 SharedDB A 1 n3 Nonce 0 A 1 n5 Nonce 2 on line 47 MESSAGES A 1 gt lt Actor 0 gt n3 Nonce FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 upd
233. redicate ASLan translation for ACM A gt send B M over Ch sent A A B M Ch A gt receive B M over Ch rcvd A B M Ch Table 10 Translation from ASLan to the ACM ACM Table 10 shows the translation of send and receive terms obtained by replacing the predicates with the corresponding encoding for the ACM FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 139 190 Similarly to CCM the subterms A B M and Ch stand for the translation of A B M and Ch respectively Note that pseudonyms are not used for ACM such that in all cases A is identical to Actor In the translation table the following auxiliary symbols are used where the type channel stands for an ACM channel sent agent agent agent message channel gt fact rcvd agent agent message channel gt fact Reception and sending of messages are captured as two separated actions This allows for a finer grained model where resilient channels can be captured In particular the following rule is added to section rules in the translation step deliver RS 0S R M Ch sent RS 0S R M Ch gt rcvd R 0S M Ch The first argument of sent is the real name of the sender RS whereas the second argument is the official sender OS which is relevant for the receiver and might be faked manipulated by the intruder as given in the rules below The t
234. refore we did not define it as part of the built in authentication translation If needed it may be user defined as forall A B P M IID request B A P M IID gt witness A B P M dishonest A gt iknows M The LTL semantics of the freshness goal which may be given in addition to an authen ticity goal is forall A B M IID IID request B A P M IID gt lt gt request B A P M IID IID IID dishonest A This says that the agent B executing an entity instance IID should not accept the same value M in a different session identified by IID from the same honest communication partner A at the same point of B s execution identified by A and P that is B has never previously accepted the same value M at that point 4 12 3 Secrecy Goals Each secrecy goal will generate at the ASLan level several transition rules Declarations For ease of description consider the following secrecy goal secrecyGoalName _ tA tB tC declared in some entity E According to the syntactic restrictions given in 3 9 4 in each sub entity in which the goal label re appears there will be parameters that correspond to the terms tA tB and tC Let us assume that these parameters have the names A B and C Labels in sub entities In any direct sub entity E each term that bears a matching goal label for example secrecyGoalName Token is translated recursively and then the following pro
235. rform are covered by the intruder s general ability expressed by the built in Dolev Yao behavior and we therefore spare the tools the explicit transition rules associated with executing honest steps of the entity description for a dishonest agent 4 7 5 Symbolic entity instantiation SymbEntityGen stmt rest sl return_sl stmt any A1 Am entity t_1 a t_n where Guard g_1 g_k positiveGuards Guard apply adaptGuard to g_1 g_k IID fresh variable declare 11D of type nat and a_1 am of suitable type in section types in the translation FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 133 190 for i from 1 to k 4 LHS state fact for the current entity with step label sl state facts for the owners of variables appearing in t 1 t n state facts for the owners of variables appearing in g_i RHS state fact for the current entity with step label succ sl state facts for the owners of variables appearing in tol bm state facts for the owners of variables appearing in g_i state fact for new entity instance such that its step label is sl_0 its instance ID is IID all parameters p_1 p_n set to t_l t_n all variables v_1 v_m set to dummy of the right type for j from 1 to m LHS LHS iknows V_j RHS RHS iknows V_j add LHS g_i exists IID gt RHS renewPositiveFactsIn g_i to section rules
236. roject No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 67 190 To highlight the differences between the CCM ICM notation and the ACM style we give a couple of ASLan specification examples in both variants We first consider a client C who sends a request confidentially to a server S and S sends a response authentically This is a typical situation where the server possesses a key certificate so the client can check that the response really comes from S but the client does not have a certificate In fact one can achieve stronger channels in such a case for instance additionally guar anteeing that the response of the S is only visible to the principal who sent the request Because this principle is not authenticated this is called a pseudonymous secure channel in CCM ICM or a unilaterally authenticated channel in ACM However we postpone this to the section on modelling TLS see 2 9 For the first example we consider a response channel where the message contents are not confidential but only authentic 2 8 1 CCM ICM For CCM ICM authentication of the sender is specified in ASLan by using gt in the send and receive instructions Similarly message transmission confidentiality is expressed by gt Thus if an unauthenticated client submits a confidential request to a server and requires an authenticated reply from that server this looks as follows specification CCM_example channel
237. rotection freshness Secrecy Goals Secrecy goals specify who may gain knowledge of a certain piece of information In our NSPK example only Alice and Bob A and B may know Na and Nb These nonces may not get known by the attacker s Thus we have two secrecy goals namely secret_Na Na A B and secret_Nb Nb A B These secrecy goals are noted down in the annotated message sequence chart in Figure 4 The model checkers can refer to the goal names secret_Na and secret_Nb if they find a way to violate any of them FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 14 190 To implement this secrecy Alice and Bob who are assumed to know each other s public keys can send confidential messages to each other Only the intended recipient can decrypt the message Furthermore Alice and Bob may not disclose these nonces to any other party for instance by sending them to others Communication Security Notions ASLan offers an intuitive arrow notation used for both communication security as sumptions and goals These properties only refer to individual communication events that is of a single payload at a certain point in the system execution Communication se curity properties are unidirectional That is transmission of a message from A to B can and will have different security properties than that from B to A e A gt B M indicates default communication without any
238. ructure of an ASLan File An ASLan specification and similarly a prelude file consists of a sequence of sections Section Type Symbols TypeSymbolsSection In this section all basic message types are declared for example nonce In the sections signature SignatureSection and types TypesSection the types of vari ables constants function symbols and fact symbols are declared See also Section A 3 4 for further discussions on types in ASLan Section Signature SignatureSection This section contains declarations of the used function and fact symbols and more specifically their types It also contains supertype declarations Section Types TypesSection In this section the types for all constants and variables can be specified This implies that throughout an ASLan file an identifier cannot be used with two different types while the scope of each variable is limited to the rule it appears in Notice that a declaration of the form M op t1 tn is equivalent to the declarations M t1 M tn where M with i 1 n are fresh variables i e that do not appear in the ASLan file and every occurrence of M in the ASLan file is replaced with the term op M M Section Equations EquationsSection The equations contained in this section define the algebraic properties of the function symbols The sections inits InitsSection rules RulesSection intruder section IntruderSection and clauses lausesSec
239. rver Authenticated HTTPS Next we model a simple stateless server authenticated HTTPS HTTP over TLS message exchange in ASLan based on the above HTTP request response pairing That is we want to ensure that each request sent by the client is confidential to the server and that the result received by the client is protected for authenticity integrity and freshness and is associated with the right request For now we do not address client authentication nor maintain session state or preserve message order In CCM we express message transmission confidentiality using gt Similarly authenti cation of the sender can be specified by using gt The only thing we need to implement ourselves is the session disambiguation and the one sided replay protection Due to the confidentiality and integrity assumptions that we now make it is sufficient to include a nonce like in the example given before The client now sends the nonce confidentially with its re quest and it is now reflected authentically by the server in its answer and checked by the client This approach securely associates every response to the correct request and ensures that the response was not a replay of the response to an older request entity Client Actor S agent 1 PayloadC lt gt Nc fresh C generates nonce Actor gt S S can NOT verify C s identity Actor Client_HTTPS_Server Nc PayloadC S gt Actor Server_HTTPS_Client Nc Payl
240. s declared dishonest select on child IID IID secrecyGoalName_set IID gt add i where the IID variable must be declared of type nat 3 5 Facts and Clauses Instead of the usual type bool for truth values ASLan uses the type fact Atomic propositions are represented by predicates of type fact and the question whether an atomic proposition holds or not is expressed by the non existence the respective predicate term in a global fact space 220f course the intruder does not necessarily stick to the prescribed steps of this entity as an honest agent would 3 The select statement binds it to the instance ID of the parent of the current entity FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 93 190 For truth values represented by facts only the type fact is allowed We do not allow variables of type fact Facts may be combined with the usual logical operators in LTL formulas to express goals and they are also used in conditions e g in if statements known as guards cf 3 11 By default a fact does not hold but it may be explicitly introduced simply by writing it as an ASLan statement and retracted The constant true is introduced automatically while the constant false is never introduced Facts may also be produced and used by so called clauses These are rules for spon taneously producing facts whenever the conditions on their r
241. s the set variable S gt add U adds an uninitialized msg variable Uninitialized variables after translation in the resulting ASLan model have pseudo values such as dummy_message and dummy_nat depending on the type of the variable When an attack trace is printed by the model checkers one may have a close look at it to spot such values in term positions where variables are used e g in a term that is sent or assigned to some other variable In the given example an attack trace would include STATEMENTS of Test n3 IID s dummy_agent gt i dummy_message dummy_set_message gt contains i a S set_1 n3 IID set_1 n3 IID gt contains dummy_message clearly showing the four dummy_ values resulting from using Actor U two times and S while not yet being initialized So far there is no direct tool support for finding such mistakes Yet one may extend an ASLan specification with a couple of auxiliary declarations and goals at the level of the outermost entity as in the listing given next FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 39 190 specification Uninitialized_Unsafe channel_model CCM entity Environment symbols uninitialized_msg message fact uninitialized_set message set fact symbols UA agent UM message UK symmetric_key UN nat UP public_key US private_key UT text SA agent set SM me
242. s with respect to a pseudonym An almost equivalent model can be written in ACM where we can take good advantage of unilaterally authenticated channels entity Session C S agent symbols Ch_C2S Ch_S2C channel entity Client Actor S agent Ch_C2S Ch_S2C channel PayloadC lt gt Actor Ch_C25 gt 8 S can NOT verify C s identity Actor PayloadC S Ch_52C gt Actor Payloads checks nonce entity Server C Actor agent Ch_C2S Ch_S2C channel while true select on Ch_C2S gt Actor S learns C here 7C PayloadC PayloadS lt gt Actor Ch_S2C gt C sends response to same C only Payloads FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 75 190 body of Session Ch_C2S fresh Ch_S2C fresh we assume unilaterally authenticated TLS from C to S unilateral_conf_auth Ch_C2S Ch_ 2C C S new Client C S Ch_C2S Ch_S2C new Server C S Ch_C2S Ch_S2C goals Note that for each session of a client and a server we create a fresh pair channels between the two which is essential in case more then one session is created This ACM variant follows the general pattern of the CCM variant but with interesting differences For modeling the assumed weak client authenti cation instead of using a pseudonym we use the more abstract channel re lation unilateral_conf_auth Ch_C2S Ch_
243. s_admin X introduction_user X is_user X add_user X introduction_admin X is_admin X add_admin X body 4 Datum fresh add_admin alice if can_read alice Datum can_write alice Datum Datum fresh if is_admin alice 4 add_user alice add_user bob if can_read bob Datum retract add_admin alice if can_write alice Datum Datum fresh if can_read alice Datum discloses_to eve Datum FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 66 190 goals readers_goal_eve discloses_to eve Datum As goal we check readers_goal_eve which states that Eve may never be told Datum First Datum is initialized and Alice is granted admin status If she can both read and write Datum she initializes Datum If she has admin status she grants Bob user status Potentially Alice could disclose Datum to Eve because administrators also are users Therefore Alice also has reading rights And Alice has declared Bob user So Bob has reading rights too and could tell Eve about Datum Now we verify that Bob indeed has reading rights on Datum Then we retract Alice s admin role After this she can neither write nor read Datum anymore Thus she can no longer disclose it to Eve Cl AtSe confirms this Assume however that Alice while still being an admin also creates herself a p
244. secure_ Alice Payload_Bob Payload The confidentiality part if any is basically translated as described in 4 12 3 adding the fact secret Payload secr_secure_Alice Payload_Bob secr_secure_ Alice Payload_Bob_set FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 156 190 in the ASLan transition rule representing the send event within 41 and the necessary contains facts in the ancestor entity E Labels in receive statements Given a transmission statement where the Actor appears on the right of the arrow such that it is a receive statement in a sub entity 2 with the same channel goal label A gt Actor secure_Alice_Payload_Bob Payload the translator will first translate the receive statement A gt Actor Payload where the goal label has been stripped off Then it generates suitable auxiliary events for instance request Actor A auth_secure_Alice Payload_Bob Payload IID and inserts them into the ASLan transition rule representing the receive event Note that in analogy to the above here A and A usually have the value of tA but this is not guaranteed When using a pseudonym Phi the receiver or sender name will simply be replaced by that in the event request Phi A auth_secure Alice Payload_Bob Payload IID If the channel goal includes confidentiality the fact contains i secr_secure_ Alice Payload_Bob_set IID is introduced
245. security requirements as long as she is played by an honest agent has two parameters of type agent Actor is used to refer to herself and B is the name of the party she is supposed to communicate with The Bob entity obtains the name of A via the first message it receives Please note that we have intentionally commented out the secrecy goal templates in the Session entity The reason for this will be explained below when analyzing the results of the model validation 2 1 6 Validating the Model Translating the ASLan Model to ASLan We have specified our NSPK model in the high level language ASLan Now we must translate it into the lower level language ASLan which the model checkers accept as input Translation is done automatically by a compiler also known as ASLan connector The translator and its usage are described in great detail in Deliverable 4 2 6 4 1 For a brief overview of its options you can also refer to Appendix B The translator is available in both an online and offline version For directions please refer to the AVANTSSAR home page at http www avantssar eu Menu Item Avantssar Platform Assume that above listed model is placed in a file named NSPK aslan Then we can translate compile our ASLan model by this command 10Bob is given A as parameter by Session and then plainly ignores its value This as remarked already is necessary because the translator from ASLan to ASLan needs to
246. sender term tA and one parameter that corresponds to the receiver term tB In a sending sub entity El the former parameter must be Actor and let us assume that the latter parameter has the name B In a receiving sub entity E2 the former parameter must be Actor and let us assume that the latter parameter has the name A Labels in send statements Given a transmission statement where the Actor appears on the left of the arrow such that it is a send statement located in a sub entity El with the same channel goal label Actor gt B secure_Alice_Payload_Bob Payload the translator will first translate the send statement Actor gt B Payload where the goal label has been stripped off Then it generates suitable auxiliary events for instance witness Actor B auth_secure_Alice Payload_Bob Payload and inserts them into the ASLan transition rule representing the send event Note that here B the parameter of 1 corresponding to the term tB usually still has the value of tB but in fact B might have changed due to an assignment to B that may have occurred in the meantime Moreover typically the term B that occurs in the send statement usually is identical to B These two agreements are typically intended but not enforced which gives the modeler more freedom but also more responsibility When using a pseudonym Phi the sender or receiver name will simply be replaced by that in the event witness Phi B auth_
247. ss further action is taken the security guarantees offered by assumed standard channel properties like confidentiality and authenticity only pertains to individual message transfer Most of today s online applications however do not communicate via unrelated messages Web applications and web services base themselves on at least HTTP or HTTPS request and response pairs frequently combined via some notion of a session forming multiple correlated message exchanges The channel identifiers of ACM are already a step forward towards relating multiple transmissions 2 9 1 Security Properties of TLS Transport Layer Security TLS 22 provides stronger guarantees than the channels we have modeled in the previous section Even if the client is not authenticated TLS guarantees that the server can ensure that its answer goes only to the party that initiated the connection This is the typical case where only the server has a public key certificate If the client also has a certificate then we have a full secure channel both sides authenticated all messages confidential Additional properties are that different parallel sessions between the same parties are distinguished and that the order is preserved in which messages are sent and that message replay is prevented One way to model TLS channels would be to directly include the TLS handshake into the specification but this would not only mean a lack of abstraction and clutter up the specification of
248. ssage set SK symmetric_key set SN nat set SP public_key set SS private_key set ST text set entity Test implicit Actor parameter not initialized symbols U message S message set body send i U sends an uninitialized msg variable S gt add i uses an uninitialized set variable S initializes the set variable S gt add U adds an uninitialized msg variable body uninitialized_msg UA uninitialized_msg UM uninitialized_msg UK uninitialized_msg UN uninitialized_msg UP uninitialized_msg US uninitialized_set SA uninitialized_set SM uninitialized_set SK uninitialized_set SN uninitialized_set SP uninitialized_set SS FP7 ICT 2007 1 Project No 216471 a SEVENTH FRAMEWORK PROGRAMME A ANTSSAR D2 3 update ASLan specification and tutorial 40 190 uninitialized_msg UT uninitialized_set ST new Test goals no_uninitialized_msg forall U IC iknows U amp uninitialized_msg U no_uninitialized_set forall U S S gt contains U amp uninitialized_set S no_uninitialized_mem forall U S S gt contains U amp uninitialized_msg U The goals no_uninitialized_msg no_uninitialized_mem and no_uninitialized_set will raise an attack when an uninitialized message is sent when an uninitialized set reference is used or when there is an uninitialized element in a set Indeed when running the example t
249. statements in FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 159 190 an entity the successive application of succ and branch creates very complex terms which would only place an unnecessary burden on the verifiers In order to simplify the generated ASLan output in this last phase of the translation after all transition rules are generated we assign numbers to the generated step label terms so that each step label term receives a unique number This is done by a procedure that starts at the initial step label s1_0 which is replaced by 1 and proceeds recursively on the succ and branch symbols the procedure is omitted Then in all generated transitions the step label terms are replaced by their assigned numbers 4 14 Step Compression 4 14 1 Motivation and example The translation we define in 4 7 produces for each entity transition rules expressing progress at statement level granularity For instance the three lines receive A N fresh send A N would get translated into three individual transitions state_responder Actor IID 1 dummy_agent dummy_message iknows A gt state_responder Actor IID 2 A dummy_message state_responder Actor IID 2 A dummy_message exists N gt state_responder Actor IID 3 A N state_responder Actor IID 3 A N gt state_responder Actor IID 4 A N iknows N After each such progress step othe
250. step label nonetheless Yet in case Var belongs to the current entity the two state facts in the LHS are collapsed into one and there is only one state fact on the RHS that combines the change to the step label with the assignment to the variable A similar strategy is always followed in order to avoid unintended duplication of state facts on the right hand side of a rule e g when multiple variables and possibly step numbers on the right hand side of a rule need to be updated Example 3 Let us extend further the BidM declaration above with a variable assignment as follows M crypt pk BP m The variable assignment can be expressed via a rule as the following one which replaces M with the term assigned to it state_BidM Actor IID s1l BP M gt state_BidM Actor IID succ s1l BP crypt pk BP m Note that this is the case for assignment to a variable M local to the entity BidM whereas if it was another variable E belonging to an ancestor of BidM e g Env the resulting rewrite rule would be FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 130 190 state BidM Actor IID sl BP M state_Env 0ID E descendant OID IID gt state BidM Actor IID succ sl BP M state Env 0ID crypt pk BP m O Note that descendant OID IID is not reintroduced in the RHS of the last rewrite rule because descendant facts are implicit cf 3 5 and 4 2 4 7
251. t J if isSubset MySetIntersection gt add E MySet1 gt remove E MySet2 gt remove E if isSubset MySet2 gt contains 4 MySet2 is Empty isEqual move back the elements from MySetIntersection to MySet1 and MySet2 while MySetIntersection gt contains 7 E MySet1 gt add E MySet2 gt add E MySetIntersection gt remove E At the end of executing this if the fact isEqual holds we have checked that MySet1 and MySet2 are equal MySet1 has been shown a subset of MySet2 and after removing every element contained in MySet1 from MySet2 MySet2 is empty This confirms that also MySet2 is a subset of MySet1 Which is what we needed to show By restoring all elements from MySetIntersection to the original locations in MySet1 and MySet2 we have preserved the original sets 2 3 5 Exercises For the advanced reader we propose the following exercises e Count how many elements there are in a set using the succ O operator Implement indexed sets using composite elements and the succ operator Have fun 2 4 Shared Data Sometimes it is useful to model that more than one entity has access to the same data As long as the data is constant this can be easily achieved by simply declaring the values as constants characterized by lower case symbols in an entity surrounding the others for instance in the root entity which as we know is usually called Environment Then the constant d
252. t is usually sufficient If the additional properties of replay protection order preservation and session distinction are needed then they can be constructed as described in 2 9 6 In Table 1 ActorP stands for Actor or any pseudonym of P it which is either the default pseudonym Actor or Actor _ P Similarly B stands for the intended communication partner of Actor or any pseudonym P of this partner which is denoted by B _ P where B is a term different from Actor with irrelevant value ACM In ACM channels are referred to by terms of type channel Their properties are usually declared by introducing certain pre defined facts introduced below which trigger pre defined LTL constraints One must of course be careful not to require non fulfillable e g contradictory channel properties which would lead to a non executable model As mentioned before Table 2 shows the general syntax that ASLan supports for ACM Differently from the CCM and ICM in ACM the arrow is labeled with the name of the channel The name may be used for identifying the channel to relate several send receive statements as well as for stating the assumed properties of the channel The named channel syntax can be used only for ACM channels as assumptions while even when ACM is chosen channel goals are always expressed and interpreted in the same way as in CCM ICM Like in CCM and ICM by default a channel does not guarantee any protection insecu
253. te rules branching the execution of the model in one direction if the Guard is satisfied or another if it is not Then for each of these branches the corresponding statements are parsed and the control in both cases goes back to the original thread of execution This holds though only for possibly negated literals while in the general case a Boolean expression can be used Since ASLan rewrite rules admit only conjunctions of conditions we use an auxiliary function positiveGuards for computing the DNF disjunctive normal form and returning the list of clauses in it Analogously negativeGuards computes the DNF of the negated guard and returns its clauses For computing the DNF we expand implications of the form P gt Qas P Q For each of these clauses a branching rule will be created and added to the translation leading to the apposite branch Furthermore evaluation of the guards should not remove facts from the state so we assume a further function renewPositiveFactsIn that renews the positive explicit facts in the clause Implicit facts are not reintroduced on the right hand side of the corresponding rewrite rule because implicit facts stored in the set PolicyPredicates see 4 4 must not appear on the RHS of rewrite rules Example 6 Let p q and q be predicates defined in BidM on agents and the following branch occurs at step sl if p Actor then q Actor else q Actor We will then create one rule leading to
254. ter set is defined below as g but rather the set of constants whose primary type is 8 but due to sub typing a constant may be part of other types as well The disjointness of the C ensures that each constant has a unique primary type For example the main message type msg is a basic type in the sense of this definition and the type agent is a subtype of it even though Cagent NCmsg e For every declaration c 8 that constant c has type 8 in a given ASLan specification we assume that c Cg e The only non basic types in our setting are sets and tuples We do not allow constants of non basic types such as msg set e We now inductively define the set of terms that have type 7 i e each is the least set that satisfies the following properties First for all basic types Cg C Lg FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 177 190 Then for a function f that has type 71 X Tn T and any terms t Ln tn Lan we have f ti tn Le If 7 lt 72 sub typing then La C La This is extending Ln If S C L and S is finite then S L set Finally Leica Ln X X Lm e Each variable of type 7 can be assigned to any term of the set and we rule out all other interpretations e We require that is closed under i e the algebraic properties do not imply the equality of terms of different types
255. the nb 2 option to cope with variable inheritance without executability problems Consequently this method of global shared variables may only be used if its side effects regarding the selection of a model checker are acceptable 2 4 2 Implementation via facts An alternative method to inherited variables takes advantage of facts being global Therefore facts may be ab used for indirect communication To this end we can globally declare a symbol FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 50 190 shared protocol_id message fact that may be used to hold the value of a shared variable of type message in this case Here we refer to the variable by some value of type protocol_id representing the identity of the variable for instance SharedVarld protocol_id Initializing this variable to some value x amounts to introducing the fact shared SharedVarld x The variable may be read by referring to the fact as in shared SharedVarld lt pattern gt which has the same effect as testing the variable for equality where the lt pattern gt may be e g X such that the local variable verb X is bound to the current value of the shared variable The effect of assigning to the variable is achieved by retracting the previous fact for this variable and then introducing a new one e g retract shared SharedVarld 7 shared SharedVarld
256. the intruder she does not think that the intruder is Bob nor does she of course know that the intruder is actually a dishonest party i can relay the data received from A to B and vice versa with some re encryption and thus convince B that he is communicating with A That is Bob is tricked into thinking that he is talking with Alice while in fact he is communicating with the intruder The input of Web Sequence Diagrams corresponding to the compact attack trace in Figure 8 is A gt i Na A Ki i gt B Na A Kb B gt i Na Nb Ka FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 29 190 Na Nb Ka Na Nb Ka Figure 8 The Lowe Attack on the NSPK Protocol i gt A Na Nb Ka A gt i Nb _Ki i gt B Nb _Kb This attack only succeeds if two NSPK sessions are conducted in parallel and interleaved as sketched in Figure 8 The intruder i re encrypts A s nonce and name received from A with the public key of B He then under the heading of lt gt in Figure 7 relays this re encrypted message to B B reads that A wants to communicate with him generates his fresh nonce Nb and sends the response encrypted with A s public key to the party he assumes to be A under the heading of lt Wit 1 gt in Figure 7 which however as we know actually is i Now i cannot read Bs response as B has encrypted his reply to A with A s public key However i can rela
257. the environment sessions are instantiated To find an attack on NSPK we need Alice to conduct at least two sessions in parallel body 1 need two sessions for Lowe s attack any A B Session A B where A B any A B Session A B where A B Therefore we instantiate two so called symbolic sessions between A and B where A may be an honest Alice instance or a dishonest attacker also known as the intruder i and B may be an honest Bob instance or an attacker For details on symbolic sessions cf 3 10 In this specification two sessions of the protocol are launched each involving one instance of A and B However we disallow entities talking to themselves So for instance a session of Alice talking to herself is not taken into account The model checker will evaluate the combinations sketched in Figure 6 For two parallel sessions the model checker taking into account symmetries will evaluate 6 different pairs of parallel sessions The model checker will try to interlace each of these session pairs in all different protocol compliant variants possible It makes sense to be careful about the numbers of sessions one instantiates in parallel as the workload for the model checker explodes with the number of parallel sessions This may preclude receiving an answer in reasonable time ASLan Implicit Operations In ASLan many operations are performed implicitly Among these are the learning of new values received by message passin
258. the first branch if p Actor is satisfied state _BidM Actor IID s1 BP M p Actor gt state _BidM Actor IID branch sl 0 BP M p Actor and another leading to the second branch if instead p Actor is not satisfied state _BidM Actor IID s1 BP M not p Actor gt state BidM Actor IID branch sl 1 BP M Parsing the two branches separately will give rise to the following rules state BidM Actor IID branch sl 0 BP M gt state _BidM Actor IID succ branch sl 0 BP M q Actor state BidM Actor IID succ branch sl 0 BP M gt state_BidM Actor IID succ s1l BP M state_BidM Actor IID branch sl 1 BP M FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 145 190 gt state _BidM Actor IID succ branch sl 1 BP M q Actor state BidM Actor IID succ branch sl 1 BP M gt state _BidM Actor IID succ sl BP M O Example 7 A guard can be a general Boolean expression which will always be reduced to a disjunctive normal form like Cy VW V En where the clauses c c are conjunctions of possibly negated predicates For each of these clauses we need a rewrite rule checking it on its LHS and leading to a common RHS except for the positive facts of the clause that are renewed Consider the following branch where p r and s are constant facts here if p not r not s then q Actor else q Actor Here the DNF obtained is p
259. this distinction we partition the facts into two sets called explicit and implicit facts Implicit facts are those which appear in the head of a clause the rest of the facts are explicit It is required that the facts appearing in the head of the clauses cannot be explicitly introduced nor retracted in the specifications Conversely facts explicitly introduced or retracted must not appear as the head of any clause We con sider the facts of the form iknows M used to model the intruder knowledge as the only exception to this restriction These facts may appear both in the head of clauses and may be freely introduced in specifications Therefore iknows facts are the only facts that are both explicit and implicit However iknows facts cannot be retracted since intruders never lose their knowledge Note that while the aforementioned requirement prevents the modeler from explicitly introducing e g fact2 1 3 to the state the modeler can instead introduce a new fact say fact2e 1 3 to the state and add the clause hc_extra X Y fact2 X Y fact2e X Y 31We use this name as a shorthand for definite Horn clauses with side conditions 32The requirement follows the distinction between policy and state predicates in A 2 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 94 190 to the specification to achieve essentially the same result as introducing fact2 1 3 Clauses may i
260. tion describe the service as a transition system the section constraints ConstraintsSection describes the constraints the transition system will always enjoy and the section goals GoalsSection describes the security goals or the attack states 48This is so far supported only by SATMC FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 172 190 Section Inits InitsSection In this section we specify one or more initial states of the service Section Rules RulesSection This section specifies the transition rules of the honest agents executing the service For the declaration of rules we also use the following syntactic sugar We assume that the iknows predicate iknows M means that the message or set M is known by the intruder is persistent in the sense that if an iknows fact holds in a state then it holds in the successor states i e once sent messages are always available to the intruder To simplify the rules however we do not repeat the iknows facts that appear in the left hand side of a rule in the left hand side of the rule Also a rule can be labeled with a list of existentially quantified variables Their purpose is to introduce new constants representing fresh data e g nonces Section Clauses ClausesSection A finite set of clauses is given in this section These describe for instance the authorization logic Section Constraints ConstraintsSectio
261. tion symbol macros MacroDecl Var gt LowerName Vars Term clauses ClauseDecl LowerName Vars name and parameters forall Var Term Condition amp Term Term Term Term Term Condition equations EquationDecl only allowed in the root entity Term Term LowerName Numeral Var Var h only allowed within guards on hh Only allowed within guards Term _ Term pseudonym FuncApp Term Term message concatenation Term Terms Terms 3 set literal Term _ Term Term _ Term Term _ inv Term Term tuple hh only allowed in variable assignment symmetric encryption asymmetric encryption digital signature a SEVENTH FRAMEWORK PROGRAMME FP7 ICT 2007 1 Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 115 190 Name Term goal label Terms Term FuncApp Term gt LowerName Terms 4 transmission not allowed here Body BreakDecl body Stmt BreakDecl breakpoints 4 LowerName Guard FuncApp Transmission sending transmission not allowed here Guard Term Term Term Term Guard amp gt Guard Guard GuardNoRcv Guard any Guard but no transmissions allowed here
262. to the verifier tools these transition rules are actually lumped into one rule wherever possible This process of lumping transitions is guided by the breakpoints defined in the ASLan model Intuitively each macro step should result in a single transition rule However this is not always possible for example if there are loops in the ASLan model Thus in certain situations the lumping of transitions cannot replace using the state fact As an example consider the following ASLan code 17The handling of the state facts has not yet been implemented for any of the back ends FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 165 190 body B gt Actor Req Actor gt B Resp some_fact Req Resp Without any optimizations the generated transition rules are state_Alice E_A_Actor E_A IID 1 B Req_1 Resp iknows Req gt state _Alice E_A Actor E_A IID 2 B Req state_Alice E_A Actor E_A_IID 2 B Req gt state_Alice E_A Actor E_A_IID 3 B Req state_Alice E_A Actor E_A IID 3 B Req gt state _Alice E_A Actor E_A IID 4 B Req Resp Resp Resp iknows Resp Resp Resp some_fact Req Resp Since no breakpoints are explicitly defined the default breakpoint is the receive predicate After merging transition rules where possible only one transition rule results state_Alice Actor IID 1 B Req_1 Resp iknows Req
263. tract from as explained in 4 14 To support this concept in ASLan we introduce a new fact state that is similar to the normal state fact but will be used for local states of honest agents within a compressed i e micro stepping section We require transition rules to have at most one state fact on either side and that the initial state does have a state fact The micro step transition relation is now the standard transition relation gt of ASLan as defined above We define the new macro step transition relation based on the micro steps as follows S1 gt Sn iff there exist S2 5 1 such that These concepts have not yet been implemented in the back ends FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 178 190 e y Oe gt pe Sn e S contains exactly one state fact for 1 lt i lt n e the state fact is not the same in two consecutive S so there is progress in the process represented by the state and e S and Sn do not contain a state fact All LTL goals are now interpreted with respect to the macro step transition relation i e the formulae are blind for the micro steps Note that our definition does not allow for partial macro steps suppose that by we can get into a state with a state fact where no transition rule allows further progress of this intermediate state i e a process is stuck within micro
264. uld be close to specification languages for security protocols and web services but also to procedural and object oriented programming languages so that it can be employed by users who are not experts of formal protocol service specification languages 3 1 Introductory example For those readers who have skipped the ASLan tutorial 2 here is a simple example of how an ASLan specification looks like the well known Needham Schroeder Public Key protocol 21 aiming at mutual authentication of two parties A and B which in Alice Bob notation reads as 1 A gt B Na A _Kb 2 A lt B Na Nb _Ka 3 A gt B Nb _Kb Here Na and Nb stand for nonces i e non guessable random values produced by Alice and Bob respectively The first line says that Alice sends her nonce and her name to Bob encrypted with his public key Kb while the second and third line specify similar message transmissions The second line implicitly requires that Alice checks the value Na she receives similarly the third line implicitly requires that Bob checks the value Nb he receives In ASLan this protocol reads as follows where the various language components will be introduced below specification NSPK channel_model CCM entity Environment entity Session A B agent entity Alice Actor B agent symbols Na Nb text body FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 89
265. uring translation these operators make little sense at the ASLan level 40Due to ASLan s stuttering semantics this only makes sense with fairness constraints FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 106 190 Operator ASLan connective Explanation If negation f1i f2 equality ET let 2 inequality A f1 amp f 2 conjunction V f1lf2 disjunction gt f1 gt 1f2 implication Vv forall V_1 V_n f universal quantification exists V_1 V_n f existential quantification neXt X f in the next state Yesterday Y in the previous state Finally lt gt f at some time in the future Once lt gt f at some time in the past Globally O always Historically at all times in the past Until U f 1 4 2 f holds until f holds and f will eventually hold Release R f_1 f_2 f2 holds until and including the point where f first becomes true if f never becomes true f2 must remain true forever Since S f_1 f_2 f2 was true at least once in the past and since then f holds Table 6 LTL operators for specifying goals 3 9 1 Invariants Goals that should hold during the whole life of an entity instance should be stated in the goals section of the entity declaration In particular goals expected to hold globally during the overall system execution should be given in the outermost entity For this type of go
266. urpose against the intended certificate use Validating Certificates To implement the validation of the chain of trust from a given certificate to a trusted root certificate authority we introduce the following clauses within the Environment entity symbols trusted_agent agent fact trusted_pk agent fact issued message fact clauses trusted_pk_direct C trusted_pk C trusted_agent C trusted_pk_cert_chain A B trusted_pk A trusted_pk B amp issued B gt cert A pk A amp BI A With the clause named trusted_pk_direct line 8 we express that we trust a public key of an entity C if C has been declared a trusted agent In our model we will do this for the trusted root certificate authority only This clause is a recursion termination point With the other clause named trusted_pk_cert_chain line 12 we introduce the recur sion step We say that we trust the public key of an entity A only if we trust the public key of another entity B and if B has issued a certificate for A accrediting A s public key and if it is not a self signed certificate Please note that A and B here are not Alice and Bob but just placeholders for any entity FP7 ICT 2007 1 L Project No 216471 A ANTSSAR CONnoPwnr CONnOoKRWN HE D2 3 update ASLan specification and tutorial 33 190 To simplify the presentation we do not model the issuing of certificates but just declare them as shown in the following
267. utorial 96 190 The basic operator on sets is the contains function where the presence of the fact contains Set X means that X is a member of Set There is syntactic sugar for the intro duction and retraction of Set gt contains X namely Set gt add X and Set gt remove X The precedence of operators in guards and other formulas is in descending order A A A Encryption of a message M with a symmetric key K can be written as scrypt K M or equivalently as M _K Asymmetric encryption with a public key PK can be written as crypt PK M or as M _PK The very same syntax is used also in receive operations where it means decryption A digital signature with the private key PK corresponding to the public key PK i e PK inv PK can be written as sign PK M or as M _inv PK The very same syntax is used also in receive operations where it means signature checking 3 8 Channels ASLan offers a concept of channels that allows specifications to abstract from the tech nical details of the realization of communication and their protection such as cryptographic mechanisms First we describe the meaning of channels as assumptions i e when for the transmission of some of its messages a protocol or service relies on channels with particular properties Second we also introduce the meaning of channels as goals i e when a protocol or service aims at establishing a particular kind of secured channel Moreover there is a
268. vantssar eu Menu Item Avantssar Platform The back ends are based on different technologies and thus provide complementary strengths for instance CL AtSe efficiently deals with Horn clauses and exhibits good per formance in general OFMC supports algebraic reasoning a proved correct pruning of the search space compositionality and an experimental combination with abstract based inter pretation and SATMC supports LTL goals all channels models and Horn theories We can upload the ASLan file to the model checker service of our choice and let the model checker execute the model remotely Alternatively we can use the offline binary of a model checker locally e g we use CL AtSe on our ASLan file by executing cl atse NSPK aslan The search behavior and the attack output of the model checkers may be tuned by certain options For instance OFMC usually needs both the classic and the untyped option CL AtSe requires the nb n option with n being least 2 in order to deal with loops and requires the not_hc option to deal with negations in clauses For detailed instructions on how to use and tune the various AVANTSSAR model checkers please see Appendix B and refer to Deliverable 4 2 6 The options to fine tune the model checkers can be given manually as command line option each time the model checker is executed Another method is to use directives at the very beginning of the ASLan model definition Here as a kind of comment each model
269. ve been developing As described in detail in 1 ASLan extends IF with a number of important features so as to express diverse security policies security goals communication and intruder models at a suitable abstraction level and thereby allow for the formal specification and analysis of complex services and service oriented architectures Most notably ASLan extends IF with Horn Clauses In ASLan invariants of the system can be defined by a set of definite Horn clauses Horn clauses allow us not only to capture the deduction abilities of the attacker in a natural way but also and most importantly they allow for the incorporation of authorization logics in specifications of services LTL In ASLan complex security properties can be specified in Linear Temporal Logic As shown for instance in 3 this allows us to express complex security goals that services are expected to meet as well as assumptions on the security offered by the communication channels ASLan is the actual input language to the validation tools that comprise the AVANTS SAR Platform A 1 Motivation We define ASLan by extending the Intermediate Format IF 9 a specification language that several of the partners of the AVANTSSAR consortium developed in the context of the AVISPA project it provides the user with an expressive language for specifying security protocols and their properties based on set rewriting Moreover IF comes with mature tool support namely
270. whose purpose is just to tag the state so to make references possible in the ASLan goals section and the other removing the predicate In fact the assertion itself i e the Guard whose satisfaction is required is checked via an extra goal checking that when this predicate appears the Guard holds The exists V_1 V_n Guard part in the above definition is further translated as given in 4 12 4 8 Translation of Guards In some of the previous sub procedures we made use of a function adaptGuard This is a minor and straightforward procedure that only replaces all applications of logical connectives with ASLan predicates as specified in Table 11 Note that the disjunction and gt implication operators are not included since there is no corresponding predicate in ASLan and coherently the function will be only applied to separate clauses of disjunctive normal forms The function adaptGuard recursively follows the term structure of the guard and does the substitutions defined in Table 11 Note that the translation of sub terms i e atoms from the logical point of view is specified in 4 9 FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 151 190 ASLan operator ASLan predicate IG not G G1 amp G2 ES Ti TI equal T_1 T_2 T1 T2 not equal T_1 T_2 Table 11 Substitutions done by the adaptGuard function 4 9 Translation of Terms In
271. y B s response to A who obligingly decrypts Nb for i Then i can re encrypt Bs nonce and under the heading of lt Wit 1 gt in Figure 7 forward it to B B now erroneously believes that he has successfully authenticated A Please note that only due to the intentional commenting out of the secrecy goal templates in the Session entity the attack was able to continue that far If you re activate the secrecy goals then of course the model checkers already find a violation of a security goal when A discloses Nb to i Then the secrecy goal secret_Nb is violated as only A and B may know of it You are encouraged to try this out Correcting the ASLan Model What went wrong When i relays B s response to A A has no possibility to discern that this response came from B originally She thinks that she is communicating with i and i FP7 ICT 2007 1 L Project No 216471 A ANTSSAR D2 3 update ASLan specification and tutorial 30 190 Figure 9 Lowe s Fix for the Vulnerability in the NSPK Protocol only Thus we have to extend the protocol with some indication for A that the response comes from B B puts into his response not only A s nonce and his own but also his name before encrypting it for A i e Na Nb B _Ka as shown in Figure 9 Now i again relays this message which he cannot decrypt to A However on checking the name in the message now A will notice that the nonce is from B and not from i as she thought Then s
272. y becomes dishonest From the above follows that one may declare any number of dishonest agents at any time to model for instance that an intruder has been able to compromise some machine at some point The modeler must take care to correctly represent this situation by introducing the fact dishonest a and by giving the intruder access to all knowledge of agent a needed to behave like a This may be achieved by introducing iknows facts for e the private keys of a in particular iknows inv pk Actor e the shared keys known to a e values of other parameters and local variables that are not already known to the in truder which may include values produced by a using the fresh operator and set literals e nonpublic symbols used by a All other data known to a can then automatically be inferred In this way it is ensured that for an entity that is played by a dishonest party with the sufficient knowledge of long term secrets e g private keys the intruder has enough information to perform every legal step of the entity so that the behavior of that entity can be subsumed by what the intruder can do 7 One must then however be careful in the handling of the information that the intruder obtains and how that may affect the goals For instance consider a secret between a set of agents If any of these agents is compromised the secrecy goal may lead to spurious attacks which can be avoided by stating just before the agent i
273. y the same effect as the previous example This variant is more involved than the previous one but has the advantage that all three model checkers SATMC OFMC and CL AtSe can deal with it without problems 2 4 3 Shared databases A very typical way to implement shared databases is via sets which by the semantics of ASLan are implemented using references to global facts This technique will be used lSRegarding semantics there is one caveat when changing the value of the shared variable there might be race conditions if between the retraction of the old value and the introduction of the new value there is interleaving with any other entity instances that use the same shared variable Yet due to default optimization options of the translator the retraction and the introduction are typically executed in a single atomic transition FP7 ICT 2007 1 Project No 216471 A AN T SSAR a SEVENTH FRAMEWORK PROGRAMME D2 3 update ASLan specification and tutorial 52 190 among others in 2 5 1 and 2 9 To implement a database we first have to declare it With the definition SharedDB agent text nat set we specify that each entry in our shared database will hold an agent a nonce and a counter To work with our database we need some basic commands With SharedDB gt add Actor Nonce 0 we can add an entry to the database With SharedDB gt remove B 1 we can remove an entry With SharedDB gt contains

ASLan++ specification and tutorial

Contents

Download Pdf Manuals

Related Search

Related Contents