Home

Documentation - LSV

1. ae Xf ZF E newX P p F newX P P X _nu newX P _ca X Xx p new Note that we do not add X to on the left hand side of H This is because X just got replaced by the term c X4 Xp The context p does not change either The first argument to __nu which is the process newX P itself is a constant As in the lean semantics the rules for inferring the values of expressions e aggravate any preexisting loss of information This is done so as to produce judgments that can be easily translated into the H class The main source of information loss is the fact that we forget about environments in judgments P F e t In other words we really ought to write judgments of the form P p F e t which would say that if we reach program point P under context p then the 15 value of e is t Instead we just say that this is so whenever P can be reached under any context 1 Main Xk i Agee yee forsome1 lt i lt k 1 ZF E gt P _ca ti tr P Eca Gu Xk Sia tpat S uke E Sk ZF E PK_celti tr Y PFX 2 e 1 Var 1 Xi Xk 1 4 Sh t1 in pairwise distinct EF E P _cs t1 te PE f Xa Xin fC as Pkrewrt Pre 2th PE f e1 n Rise In rule Flat we require f X f n but we may think this is implicit In rule f we require f X X f n and either some e is not a variable or all are variables
2. F E case e of f X1 Xn gt P else Q p case e of f Xj Xn gt P else Q F e1 g ti tm gE Ugh m g f F case e of f X1 Xn gt P else Q gt Qi p casef casef g As in the lean semantics there are as many instances of rule casef g as there are symbols g other than f This says that you may execute the else branch as soon as e may have a value that does not match the pattern f X1 Xn As promised in Section 3 1 we improve on the lean semantics for symmetric decryption Look at expression case e of X P else Q Instead of checking that e has some value t such that u is also a value of e2 we shall impose that e has a value of the form t 7 where o is some substitution of the free variables of es for terms Additionally the most interesting case is when e1 and deserves a special rule of its own Accordingly we have two rules replacing case When e is a variable X A TON ee lt k The free variables of ez are X Xi 1 lt t1 lt lt im lt k P case X of X e gt P else Q E gt P ll_ca ty t ee P _cz t1 So UE t eo Xi t oe Koiti bisa arte th AKE ia P e P _cx s t tis AE tr 1 1 Varcase Again we are using the premise duplication trick in order to approximate an equality here t grees X X e nota variable The free variables of ez are X Xi 1 lt t1 lt lt im lt k F E case e
3. which is a map from identifiers f to natural numbers the arity of f X contains the map crypt gt 2 acrypt gt 2 eq gt 1 pub gt 1 prv gt 1 0 gt 0 s gt 1 nu gt 2 U __c E process variable list e A constructor signature K is a subset of dom K contains the set 0 s U _ cs process variable list e A set of private functions Prv which is a subset of dom X Prv contains the set _eq nu e A process table Proc which is a finite map from identifiers to process abstractions A process abstraction is an expression X X P where X1 Xn are n distinct variables and P is a process Typically writing proc f X1 Xn P means adding a binding from f to Xj Xn P to Proc Proc contains at least the entries dy_synthesizer gt c_in c_out P and dy_analyzer gt c_in c_out P n These are meant to describe capabilities of a Dolev Yao intruder Pyn is a process that is the parallel composition of processes of the form in c_in M in c_in Mn out c_out f M1 M stop 1 3 for each f n in such that f Prv this expresses the fact that a Dolev Yao intruder can build new messages using the functions in X that are not private Pant is the parallel composition of in c_in M in c_in M2 case M of Mi out c_out M else stop 2 in c_in M in c_in M2 case M of Mi m out c_out M1 else stop 3 in c_in M case M of f M Mn gt out c_out M
4. but will forget that the values of X and Y are the same The purpose of the light semantics is to try and keep such relations as much as possible The new judgments of the light semantics are e Pt e t states that expression e may have value t when program point P is reached Additionally processes P will not be limited to be subprocesses of some initial process In general P will be obtained by replacing variables by terms in subprocesses E g newX P will involve instantiating X by terms of the form _nu newX P _ c t1 t in all contexts where X has value t4 Xp has value t e P p tou states that message u may have traveled on channel t and sent at program point P under context p A context is a finite mapping from variables to values That is it states which values the variables of P had when P sent u on t We choose to represent p as a term of the form _ca t t where is a list of exactly k variables X1 Xx this represents X1 gt t1 Xk gt tr e Pp t gt u Q p states that P under context p may have sent u on t and u was received by Q under context p e Z F E P p states that execution may reach P with context p and that the last program point before P was E This judgment will always obey the invariant that as a set is exactly the set of free variables of P Also if is X1 Xp then p is a term of the form __ca ti tk In the sequel we assume
5. of X e gt P else Q _ca ti tx Stipe im tim case X t case e of X gt P else Q P _cya t t tk 19 Then we have a rule saying that decryption may fail This may happen because the value of e1 is not a symmetric encryption F E case e of X gt P else Q p case e of f X Xn gt P else Q F e1 g ti tm g E X X g m g crypt F case e1 of X e gt P else Q gt Q p case 9 This may happen also because the value of e is a symmetric encryption with the wrong key ZF E case e of X e gt P else Q p case e1 of f X1 Xn gt P else QF e thu case e1 of f X1 Xn gt P else QF ez u case case e of X gt P else Q gt Q p l UP F E case e of X gt P else Q Kp case e of X gt P else QF e gt tly case e1 of X gt P else QF ezt u case l X case e of X gt P else Q P __cx t p EL E case e of X gt P else Q Kp case e of X gt P elseQFe xt casel 7 X t case e of X gt P else Q gt Q 4 The Full Language In the full language patterns are meant to denote expressions matching only certain terms For example the pattern X a variable matches every term The pattern cons2 X Y matches every term of the form cons2 u v if cons is declared as a constructor of arity 2 eine S 24 variables f pati pat application of constructor f
6. patite symmetric decryption pati ez asymmetric decryption D e equality check The encryption patterns pat and pat e use terms not patterns in key positions This is intended Matching a term u against pat e means checking that u is a symmetric encryption using key e2 of something matching pat Matching a term u against pat means checking that u is an asymmetric encryption using the inverse of key e2 of something matching pat Patterns are restricted to be linear and non ambiguous Linearity means that no pattern binds the same variable twice e g cons X X is forbidden as a pattern because X occurs twice in it Non ambiguity means that no variable free in any subexpression such as ez or e above is also 20 bound in the pattern For example X x is forbidden as a pattern Intuitively matching against it would mean decrypting with the current value of X getting the plaintext and binding it to the same variable X but this is hard to read The e pattern only matches the term e and is concrete semantics for __eq e This is useful for nonce verification for instance In the core language patterns are restricted to so called core patterns defined by the gram mar epat X variables f Xi Xn application of constructor f to n distinct variables i dhe symmetric decryption lh Kle asymmetric decryption e equality check References Abadi M and Gordon A D 1997 A calculus for cryptogr
7. that all bound variables are renamed apart so that no alpha renaming is ever needed 14 We may start running the whole system starting from main with no variable bound to any term Start ef e main _c We write e the empty sequence of variables Replication as expected creates a fresh process identifier and stores it into X ZF E gt IX P _c a ti tx teNn X ERYUX P gt P _exsl t hh ga r The judgment t N was defined in Section 3 1 Rule does not suffer from the same loss of precision problem than and Sec tion 3 1 The dependencies between the values of all variables are indeed kept Parallel composition does not modify any context Ebr E gt PQK I Eb E gt P Q o i pin py SUR I ee Br P Q gt Po BE PIQ gt Q p PIQ Ko Evaluating an expression of the form newX P involves substituting the term _nu newX P _c X1 X for X where X1 X are the variables in We assume that substitution P X e of X for e in P is defined in the usual capture avoiding way What we would like to write is let be X Xp and assume that E newX P p i e we can reach program point newX P with environment p then we can reach P in the environment p augmented with the binding from X to _nu newX P p To gain some precision we directly replace X by _nu newX P c X1 Xk knowing that p will give the correct values to Kaige sya
8. 1 stop out c_out Mn stop else stop 4 where in the last process f ranges over K Prv and X f n The parallel com position out c_out M1 stop out c_out Mn stop denotes stop if n 0 and out c_out M stop ifn 1 A typical encoding of the Dolev Yao intruder is then proc dolev_yao_intruder c init new id out c init stop out c id stop in c M out c M out c M stop new out c N stop dy_synthesizer c c dy_analyzer c c e A main process i e a process name describing the whole system to be analyzed The main process is always called main and must be in dom Proc This main process is meant to describe the whole system including all honest agents as well as all intruders For the purpose of verification we also add to the set of all I Spi processes seen as constants 1 e we add P gt 0 for every process P to XJ considering that no process is equal to any identifier in dom X The binary symbol __nu is used to represent fresh names see the semantic rules for the newX P construct 2 Approximating Equality In the various approximate semantics of the core calculus it will be necessary to deal with equality of values For example decrypting a message of the form t with some key v only works provided that u v Conversely if u v then attempting to decrypt t with v must fail We wish to encode both the equality relation and the disequality
9. OC eet ti tk Rule __cx in is the only one until now where we extend the context p cz t1 tk inside _ to cx z u ti t Another will be given by rules on case expressions below In this case we write the following analogue of in gt X X B Xi Xk forsomel lt i lt k 1 e _m Qi cs Xi ee E gt in e X Q _cel th te F Pp mu Qr cs ti te ou 0 1 1 Kp P e 8b u F Pp sou inle X Q p We again use the premise duplication trick here The two premises F E in e X Q __ca ti tx and F E in e X Q p may seem redundant we really mean that p __c t1 t However dispensing with the second one and replacing p by _ cs t1 in the conclusion would make this rule a non H clause Similarly with the two premises F P p _nu Q1 cz ti th gt u and F P p sou There is no need for a rule such as in which allowed one to conclude that u was a possible value for X after executing in e X in the lean semantics Indeed this is done here by applying rule c x profiting from the fact that all values of variables are recorded in the _ part of the conclusion of rule cx in Second the case where e is a variable X is the most common It is the case where Q expects data from a channel that was passed as a parameter to it or on yet another channel Note that the value of the chan
10. The I Spi Tool Jean Goubault Larrecq LSV UMR 8643 CNRS amp ENS Cachan INRIA Futurs projet SECSI 61 avenue du pr sident Wilson F 94235 Cachan Cedex goubault lsv ens cachan fr Phone 33 1 47 40 75 68 Fax 33 1 47 40 75 21 December 6 2005 Contents 1 Syntax of the Core Calculus 1 2 Approximating Equality 4 2 1 Finding an over approximation of equality 5 2 2 Finding an over approximation of disequality 7 3 The Semantics of the Core Calculus 12 3 1 The Lean S manticsem ee We es 12 3 2 The Ligh Semanticsemesri WERA es 16 4 The Full Language 22 The I Spi tool is meant to verify cryptographic protocols in a notation close to that of the spi calculus Abadi and Gordon 1997 In practice the syntax of I Spi processes is very close to that used in Blanchet s ProVerif tool Blanchet 2004 1 Syntax of the Core Calculus First expressions are meant to denote messages A X variables f ei1 n application of constructor f erhe symmetric encryption ere asymmetric encryption Variables are always capitalized as in Prolog Other identifiers always start uncapitalized Constructors may be any identifier The constructors _cz are reserved for each finite list 1 Xj X of process variables and are used to represent value environments E g the environment mapping M to t Na to ta and X to t3 is represented as __cya x t ta t3 The const
11. X2 __def_1 X1 _ def_1 X2 def_3 p l o 2 _ def_5 X1 __def_6 X2 __def_ crypt X1 a _ def_3 X1 __def_4 X2 __def_2 plus X1 X2 __def_8 X1 __def_9 X2 __def_6 b __def_9 crypt X1 X2 __def_6 X1 __def_4 X2 def 27 0 __def_8 crypt X1 X2 __def_5 X1 __def_4 X2 __def_5 a Here __def_1 ___ de f__9 are auxiliary states of the automaton Next complement this automaton You first need to add clauses so as to describe the signa ture Let s say for the purpose of illustration that we have a constant symbol zero and a unary symbol minus in our signature X in addition to crypt plus a b c already mentioned above Add the clauses sig zero sig minus X sig X Sig crypt WOD sig IPES Aa Sig plus TOPE sig XIF OCO sig a sig b sig c to eq1 nd p1 by writing cat sigl pl gt gt eql nd pl We assume the above clauses were written in a file sigl pl Note that pair is nota symbol in the signature By the way here is a graphical version of this automaton rendered using pl2gastex layout dot egql nd pl gt eql tex Then determinize the augmented automaton using pldet Using auto2p1 with the negate option on the output of p1det will produce the complemented automaton pldet egql nd pl auto2pl defs negate eq gt neql pl echo distinct X Y __not_eq pair X Y sig X sig Y gt gt neql pl The last line above serves t
12. a message uz on channel ui and in e X Q F e u Q actually expects some input on channel u1 then X in e X Q Q _cxs ue ti on the one hand you can reach Q with X bound to Uz and P p t gt tz in e X Q p on the other hand Q received its message from P However just writing in e X Q F e u as a premise incurs some loss of precision in that we require that the value of e be u1 disregarding the context __c t that we knew from the other premise F E in e X Q _ ca ti t In some cases i e when e is a variable as in rule Varz or when e is a term of the form _nu Qj cz Xi Xx with a suffix of E as in rule __cx or when e is a flat term f X X as in rule Flat we can actually relate the value of e to the context __cs t t while remaining inside the H class In fact we only have to deal with the cases where e is a variable X or a name _nu Q1 cs X X This is because only names can be used as communication chan nels as in the pi calculus or the spi calculus Let s deal with the case where e is of the form _nu Q c Xj X first This is the case where Q expects some data from a fresh channel created by new earlier in the same 17 process Xi Xk 2 Xi X forsome1 lt i lt k 1 ean E E F E ine X Q aie aa P o On ell bf gt U cx in Aya in e X Q gt
13. alue v of the model M is translated to a fresh predicate q For every f X X f n for every n tuple of values v1 Un in M write down the clause du F X yee Xn Qu X1 fase 1 qon Xn where v is the value of f applied to vj Un in M Let A be the resulting set of clauses If M is equal to N modulo EF then M and N will have the same value in M so for every value v both q M and q N will be consequences of the clauses in A Alternatively defining the predicate p by the set of clauses Xi xe X G X1 X2 5 when v ranges over the values in M describes p as an over approximation of equality modulo E Additionally the automaton A has the property that for every ground term t q t is derivable from A if and only if the value of t in M is v Since M satisfies all clauses sequal Si4 tm 4 1 lt j lt n there is no pair of ground instances s 4 0 tm 0 that are made equal in M It follows that there is no value v in M such that q 5m4j o and dy tm 4j are both derivable from A In other words no instance of 5 4 m tm4 is derivable from A and the clauses 5 we have found an over approximation of equality modulo E that correctly recognizes all negative examples 2 2 Finding an over approximation of disequality To over approximate disequality under approximate equality A trivial way is to enumerate finitely many ground instances of the equational theory and of the positive examples s g
14. aphic protocols The spi calculus In Proc 4th ACM Conference on Computer and Communications Security CCS pages 36 47 Blanchet B 2001 An efficient cryptographic protocol verifier based on Prolog rules In 74th IEEE Computer Security Foundations Workshop CSFW 14 pages 82 96 IEEE Computer Society Press Blanchet B 2004 Cryptographic Protocol Verifier User Manual Ecole Normale Sup rieure and Max Planck Institut fiir Informatik http www di ens fr blanchet Claessen K and S rensson N 2003 New techniques that improve MACE style fi nite model building http www uni koblenz de peter models03 final soerensson main ps Goubault Larrecq J 2001 Les syntaxes et la s mantique du langage de sp cification EVA Rapport num ro 3 du projet RNTL EVA 32 pages Goubault Larrecq J 2004 Une fois qu on n a pas trouv de preuve comment le faire com prendre a un assistant de preuve In Actes 15 mes journ es francophones sur les langages applicatifs JFLA 2004 Sainte Marie de R France Jan 2004 pages 1 40 INRIA collec tion didactique Goubault Larrecq J 2005 Deciding H by resolution Information Processing Letters 95 3 401 408 Nielson F Nielson H R and Seidl H 2002 Normalizable Horn clauses strongly recog nizable relations and Spi In 9th Static Analysis Symposium SAS Springer Verlag LNCS 2477 21
15. ay actually be no attack at all In the sequel we assume a signature J a constructor signature and a set of private functions K Prv C dom X a process table Proc and a main process main dom Proc to be given once and for all We give several such semantics from most approximate to most precise the Jean semantics Section 3 1 the light semantics Section 3 2 3 1 The Lean Semantics The coarsest semantics of I Spi is the lean semantics and is inspired from Nielson et al 2002 Le this is really close to the semantics in the cited paper except you may fail to recognize it It is given as a set of rules allowing one to derive one of the following forms of judgments e e t states that the I Spi expression e may evaluate to the value t values are represented as terms just like expressions but we keep the denominations expression e and term t distinct so as to emphasize the difference Note that contrarily to what the notation suggests is not meant to be particularly reflexive symmetric or transitive here e P t u states that message u may have traveled on channel t and sent at program point P i e P may have sent u on channel t Here t and u are terms that is values not I Spi expressions e P teu Q states that P may have sent message u on channel t and that u was then read by Q e F E P states that execution may reach the program point P and that the last program
16. but at least two are identical In other words f only applies if none of cx Var Flat apply Rule Varz applies only if there is no super expression on which c x or Flat applies To emit a message we do essentially as in the lean semantics adding contexts to processes We could content ourselves with writing analogous rules i e if E out e1 e2 Pp we can reach out e1 e2 P with context p if out e1 e2 P F e1 ti er s value may be t and if out e1 e2 P F e2 amp t e2 s value may be tf then first F out e1 e2 P gt P p we can reach P with an unmodified context p and second out e1 e2 P p t gt te out e1 2 P send tz on channel t However there are interesting special cases that deserve to be considered in a special way so as to lose as little information possible namely when e is a variable and the case where ex is a name __nu Q v We consider that as in the pi calculus or the spi calculus communication can only take place on channels and that only names can be values of channels This can only happen if e is a variable e g a formal parameter or something gotten from some other communication channel using in or if e is of the form _nu Q v i e when the current process wants to output on a channel it itself created earlier Let s look at the case where e4 is a name Flat f _nu Q1 e Xi te Xx cz t1 tk
17. ches are reachable although not both branches can be reached F E letX einP Fert H E letX einP Fert DO O U a 1et Me let X e in P gt P FAXA ay F E gt case e of f X Xn gt Pelse Q Fe f th tn casef X1 Xn F case e of f X1 Xn gt P else Q gt P F E gt case e of f X Xn gt Pelse Q Fe f t tn O _ case fr KX 2t l lt i lt n F E gt case e of f Xj Xn gt P else Q ome g t1 tm ged U g m g f F case e of f X1 Xn gt Pelse Q gt Q case g 12 There are as many instances of rule casef g as there are symbols g other than f This says that you may execute the else branch as soon as e may have a value that does not match the pattern f X1 Xn F E case e of X gt PelseQ Fer th Feru X case e of X e gt P else Q gt P ZF E gt case e of X gt PelseQ Fer th Feoru PASS ZF E case e of X gt PelseQ Fert F case e of X e gt P else Q gt Q case case case 4 The most notable feature of the rules above is that we estimate that decryption may always fail rule case indeed says that as soon as e has at least one value you can always follow the else branch We shall produce a more precise rule in the light semantics Section 3 2 Asymmetric decryption is very similar except that we now need an auxiliary judgment F e7 t to say when e denotes an asymmetr
18. do also hold modulo All these are implicitly universally quantified This can be checked when F is presented by a convergent set of rewrite rules modulo AC for example rewrite s and t to their normal form modulo AC 1 lt i lt m and check that the resulting normal forms are equal modulo AC form 1 lt 7 lt m n narrow s and t instead of rewriting them and check that no common term is obtained from s and t Narrowing will in general fail to terminate unless negative examples are ground in which case narrowing will coincide with rewriting and therefore will terminate Our approximations will be separated in finding an over approximation p of p Sec tion 2 1 and in finding an over approximation p of p Section 2 2 2 1 Finding an over approximation of equality Then let Sx be the set of clauses consisting of 1 all equations of i e all clauses equal s t where s t is an equation in F 2 all negative examples i e the clauses sequal 5 tm 1 lt j lt n equal is the equality predicate in TPTP notation the input format for h1 and for Paradox Find a finite model M of S plus the theory of equality using a finite model finder such as Paradox Claessen and S rensson 2003 E g consider the equational theory amp given as follows X 4 Z X4 Y 4 Z X Y Y X X4 0 X and take as negative example X Y z Ae X z Y Z 5 stating that symmetric encryption never commutes with sums The re
19. fle1 k f 11 The following rules state that you may always proceed to execute P from out e1 e2 P and that the event out e1 e2 P t gt t2 is derivable Eb E gt out ei e2 P Fe xt F e to F out e1 e2 P gt P ELE out e e2 P Fert Fet out outo E out ey e2 P tiD to To read a message executing in e X Q we evaluate e to a value t4 then look for some derivable event out e1 e2 P t gt te with the same value t for the channel on which tz was sent Then we bind X to the message f2 EEE in e X Q FP tpte Ferty in X t in e X Q Q EF E in e X Q H P tiot Ba o C FX to Et E in e X Q PIZ eE Fert na O i P tibt inle X Q This is the set of rules that most likely loses the most information Essentially they state that you can read some message t gt on channel as soon as some process P has sent or will send or would have sent tz on t if some other execution branch had been taken Will send the semantics above forces the process in c X out c e P to accept the value t of e sent by out c e as possible value of X received by in c X as soon as some arbitrary message has been sent on c Would have sent the process if e eg then in c X P else out c e Q will be dealt with as though P in the then branch is reachable with X bound to the value of e as given in the else branch as soon as both bran
20. fresh name creation out e1 2 P writing to a channel in e1 X P reading from a channel let X e in P local definition case e of f X1 Xn gt P else Q constructor pattern matching case ec of X e gt P else Q symmetric decryption case ec of X gt P else Q asymmetric decryption if e1 e2 then P else Q equality test fleir n process call Intuitively stop just stops X P launches an unbounded number of copies of process P each copy receiving a fresh natural number its pid in variable X P Q launches P and Q in parallel newX P creates a fresh name nonce key channel name binds it to X then executes P out e1 e2 P writes ez on channel e1 then executes P in e1 X P blocks reading on channel e1 binds any received value to variable X then executes P let X e in P binds X to the value of expression e before executing P case e of f X1 Xn gt P else Q evaluates e1 and if its value is of the form f t1 tn it binds each X to the corresponding t then executes P otherwise it executes Q case e1 of X P else Q decrypts e using key e gt and a symmetric decryption algorithm and on success binds X to the plaintext and executes P otherwise it executes Q case e of X P else Q does the same with asymmetric decryption where ex evaluates to the inverse of the key with which e was obtained f e1 en is meant to call the process named f passing it the n arguments 1 En A prog
21. ic key k and k is the inverse of key t EL E casee of X gt PelseQ fFex il Fer xu casel X b case e of X gt P else Q P ZF E gt case e of X gt PelseQ Fe xfi Fez xu casel EASi F E case e of X gt PelseQ Fert casel F case e1 of X gt P else Q gt Q The judgment e t is defined by the following rules e pub t e prv t i pub prv ieee prv t e pub t St E if e ethen P elseQ Fext Bri if F if ej e then P else Q P F E ife e then P elseQ Fert Fegru if F if ey e2 then P else Q P Note that e and ez are required to have the same value t in rule if In if we only check that e and e2 both have a value not necessarily distinct 13 ZF E fle 5en f dom Proce Proc f X1 Xn P Fe xt Fey 2 ty Xi Xn malt dR eee er ee P ELE f ei n f dom Proc Proc f X1 Xn P Fey ti F en tr PX pete Q lt i lt n Call Call 3 2 The Light Semantics The idea behind the light semantics which is more precise than the lean semantics is to keep more relations between the values of the variables in the given scope In the lean semantics if you have two runs of the same process that lead respectively to give X the value 0 or to give X the value 1 then you bind Y to_X the lean semantics will estimate that X can be 0 or 1 and that Y can be 0 or 1
22. nel is the term t which should be restricted to be a name 1 e a term of the form _nu s t But doing so would produce a clause outside of H We use the premise duplication trick again _Cxy in gt _ cx in b a Xij Xk e Xi 1 lt i lt k Eb B in e X Q cati te H P U tiru F E in e X Q K czlti ti 1 nu u v tiga t R a Varin X Eb in e X Q gt O __cralu ti tx Again the corresponding analogue of in gt uses the premise duplication trick Be a ag Ak X 1 lt i lt k Eb B in e X Q _ ce t te H P tiru ZF E gt inle X Q Ko F E in e X Q K ca t ti 1 nu u v tii tk Y PEF Varin gt F P o tiou inle X Q Co 18 Just as for new in expressions of the form let X e in P we have the choice between recording the value of the bound variable X inside the environment the part in the judgment Er E let X e in P p or to replace X by e in P The latter is more precise so we choose this way of expressing the semantics of let expressions EF E let X e in P p lett F let X e in P gt PIX el Kp Case expressions are then evaluated in the obvious way F E case e of f X1 Xn gt P else Q _ca uy Up Y case of f X1 Xn gt P else QF e f ti tn Oe ale case e of f X iet Xn P else Q PK eq Rae Xa a t n U1 eh Ur
23. o define those pairs X Y such that not only the pair pair X Y is recognized at __ not__eq but also X and Y are terms in the signature complementation produces lots of strange terms recognized by __not_eq We can then massage the output neql pl by filtering out all those predicates that do not serve to define the distinct predi cate using plpurge and by calling h1 to eliminate the __ not__eq predicate entirely plpurge final distinct negql pl pl2tptp hl no trim model no alternation plpurge final distinct hlout model pl gt distinctl pl Here this yields a 130 transition automaton for distinctness The distinct predicate is the desired over approximation p of g 3 The Semantics of the Core Calculus The core calculus of I Spi could be given a semantics looking like the one of the spi calculus Abadi and Gordon 1997 In practice it is more useful to consider approximate semantics i e semantics that are guaranteed to simulate at least all valid execution traces of I Spi programs but which may simulate a bit more In practice this means that it may be that a given cryptographic protocol has no actual attack but that one will exist in the approximate semantics This is done in the name of computability and in some cases even efficiency The point is that is no attack is found in any of the approximate semantics then the protocol is indeed definitely secure But if some purported attack is found there m
24. out e1 e2 PF e u 1 1 _cx out gt This is a bit tricky as the two premises F E gt out e1 e2 P __cs ti t and E F E out e1 2 P p may seem redundant we really mean that p __c t t However 16 dispensing with the second one and replacing p by _ ca t1 t in the conclusion would make this rule a non H clause Call this the premise duplication trick When e is a variable we check that its value is a name l RAR ey X 1 lt i lt k ZF E outer P Ca h te1 nu s t ti1 16 ZF E out e 2 P __ca ti t ZF E out ei e2 P o out e1 e2 PF e amp u Varout gt out e1 e2 P p tip u We again use the premise duplication trick here we make three copies of what should essentially be the same premise The above rules say what messages are sent on the relevant channel The following states that out e1 e2 P may proceed to execute P in the same cases nu Q ce X afars Xk F E out e1 e2 Pp out e1 e2 PF eg u _ cx out F out e1 e2 P gt P p ESN jose AT G Xi EE ESk EF E out e a P lt a t ti 1 nu s t tizi be ZF E out ej e2 P p out e1 e2 PF e2 u Vee FEF out ey e2 P gt P p Let s now read messages The idea is that if F E in e X Q __cs ti t we can reach in e X Q P p u1 gt uz some process P sent
25. point before P was E Sub processes of a given process are basically equivalent of program points in usual programming languages To be precise may either be a program point Q or the special symbol e no event yet the program has just started is a list of variables they are the variables bound in message read instructions in replications and formal parameters above P Additional auxiliary judgments will be introduced on a case by case basis They are t N meaning that is a natural number e t meaning that the value of e is the inverse of key t 10 The first rule states that we may start running the whole system starting from main ___ Start F e main The semantics of replication X P states that when you have reached X P you can im mediately proceed to evaluate P and X is any natural number EhE X P Sh E xX P ten ay tcN e NS ____ a X EEIX P gt P Re OEN s t E N The second rule states that X may be any natural number t Natural numbers are defined through the auxiliary judgment t N which can only be derived used the last two rules In other words the natural number n is the term S 0 There is some loss of precision in the rules above and in similar rules to follow rule states that we may reach P and rule states that X may be bound to t but these rules are independent These rules do not enforce that X should be bound to t only when we
26. ram is syntactically a sequence of declarations Each declaration can be e proc f X P and f X2 Py and and f X Py declaring k process names f fk parameterized by argument lists X 1 lt i lt k and defined as the respective processes P e private data f n declares the identifier f as a constructor of arity n initially I Spi starts as though we had written data 0 0 data s 1 data _cs k for every list of process variables of length k constructors can be used in constructor pattern matching The private keyword is optional If present it states that a Dolev Yao intruder cannot use f either to build messages f M M or to do pattern matching on f The only influence private has is in the definition of processes Peyn and Pan below e private fun f n declares the identifier f as a function of arity n it cannot be used in constructor pattern matching but can be used to build new messages The private keyword is optional If present it states that a Dolev Yao intruder cannot use f either to build messages f M Mn The only influence private has is in the definition of process Psyn below The intruder as well as any process cannot do case analysis on f if you want to do this use data instead of fun We assume that these declarations have been checked for consistency meaning that process names are only declared once that arities match etc and have been compiled to e A signature X
27. reach P To execute the parallel composition P Q you need to execute both P and Q F E P Q ZF E P Q The semantics of fresh name creation involves the auxiliary function symbol _nu In execut ing newX P we bind X to the term _nu newX P cz t1 tk where t t are the values of the variables X4 X in the list to the left of F This way of representing fresh names is a variant on one due to Blanchet 2001 F E gt newX P X i Xk F E gt newX P FX xt F Xk tk hnn A n Z FH newX P P X _nu newX P cr x t1 tk Note that in rule new we do not add X to the set in the conclusion of the rule There is some slight loss of information here too Normally executing newX P creates a fresh name each time and stores it into X The rules above may create twice the same name namely when we execute the same process newX P twice with the same values t1 t of the variables X Xk Given that we know the values of variables we may infer the value of more complex expres sions This is given by the following rule which is parameterized by the function symbol f of arity k fees X f sk Fert Kerk A flei ek X tba we abe The f rule does not lose any information by itself but propagates and aggravates any loss of information E g if there are two possible values t for e1 two possible values t for ep then there are 2 possible values for
28. relation as binary predicates in logic On the free term algebra encoding the equality relation is easy just write the clause X X However this escapes the H class Nielson et al 2002 a particularly nice decidable and broad fragment of Horn logic This is not in H1 technically because the head X X of this clause is not linear A linear head is one where every variable occurs at most once In fact any extension of H that encodes equality is undecidable Goubault Larrecq 2005 In particular it is also futile to try to replace the clause X X above by clauses encoding a recursive characterization of equality on ground terms such as FX iea Xn SIO et X Xn Yn for each f E f n n N However it is possible to define approximate relations possibly equal and possibly distinct Additionally we wish to take some fixed equational theory E into account That is we wish to approximate equality modulo and g disequality modulo E by two relations g possibly equal modulo and p possibly distinct modulo We assume E is presented through a finite set of equations which we write again E In the following subsections we describe an automated way to compute some sets of clauses that achieve this purpose Imagine we have some positive examples s f t Sm E tm of equations that do hold modulo FE and some negative examples Sm 1 FE tm 1 Smtn tm n Of disequations that
29. ructors crypt and acrypt are reserved too In fact e1 e is synonymous with crypt e1 2 and e is synonymous with acrypt e1 e2 The first denotes symmetric en cryption of e using key e2 The second denotes asymmetric encryption of e with eg This is a simplification of the EVA model Goubault Larrecq 2001 The idea is that whether you use a symmetric a public or a private key ez to decrypt e1 e you need to know ez not its inverse in case it has one and to decrypt e1 e you need to know the inverse of e gt and it needs to have one In other words there are two encryption algorithms in I Spi one symmetric one asymmetric You must use the same keys to encrypt and decrypt with the first one and you must use inverse keys with the second one In other models the shape of the key determines whether you should take the same key or an inverse this is hardly realistic The EVA model allows for arbitrary many encryption algorithms some symmetric some asymmetric this is simplified here by just having one of each The unary constructors pub and prv are also reserved to denote asymmetric keys The inverse of pub k is prv k and the inverse of prv k is pub k The ISpi language is comprised of a so called core language from which all other constructs of the language can be defined The core processes are described by the following grammar P Q R stop stop X P replication P Q parallel composition newX P
30. sulting set S of clauses is in TPTP notation input_clause assoc_plus axiom qual plus X plus Y Z plus plus X Y Z input_clause comm_plus axiom equal1 plus X Y plus Y X input_clause plus_zero axiom equal plus X zero X input_clause non_homo_1 conjecture equal crypt plus X Y Z plus crypt X Z crypt Y Z Say the above clauses are in some file named ex1 p Launch Paradox on Sx paradox model exl mod exl p and look at the resulting model here of size 2 in file ex1 mod crypt 1 1 72 crypt 2 1 72 plus 1 1 1 1 plus 1 2 2 plus 2 1 2 plus 2 2 1 zero 1 Of course such a model may fail to exist typically if the examples contradict or if there are only infinite models Since a finite model is just a complete deterministic automaton Goubault Larrecq 2004 it can be expressed as H clauses The example model above for instance gives rise to the following clauses in Prolog notation go crypt X Y m X a Y go crypt X Y X aY q plus X Y q X a V go plus X Y a X Y go plus X Y Q X aY q plus X Y X Y For all unspecified cases fix some value e g decide that crypt 1 2 1 and E RE 2 2 aml i qi crypt X Y a x Y qi crypt X Y X Y Formally this is done as follows Each v
31. t gt Sm E tm This provides a finite set of pairs Any finite set of terms is regular and the com plement of any regular set is regular The resulting complement is then an over approximation of disequality Let us give an example Imagine that in fact encryption is homomorphic s t g s u t for every terms s t u Imagine we have one positive example which is a particular ground instance of this say a b pun c e a puv c P pun c Write this pair of equal terms as a Prolog clause eq pair crypt plus a b pub c plus crypt a pub c crypt b pub c The h1 tool suite understands this syntax without modification Add all clauses that describe properties of equality and which are 7 clauses These are eq pair X Y lt eq pair Y X eq pair X Y lt eq pair X Z eq pair Z Y eq pair c c for every constant c X Put these clauses into some file eq p1 and run 7 pl2tptp eql pl mv hlout model h1 1 no trim mod pl eqli nd pl and you ll get the corresponding automaton as Prolog clauses in file eql nd pl __def 2 _ def_7 X eq pair X1 X2 _ def_2 X1 _ def_1 X2 eq pair X1 X2 _ def_2 X1 __def_2 X2 eq pair X1 X2 __def_6 X1 _ def_6 X2 eq pair X1 X2 __def_1 X1 __def_2 X2 eq pair X1 X2 __def_5 X1 __def_5 X2 eq pair X1 X2 __def_7 X1 __def_7 X2 eq pair X1

Documentation - LSV

Contents

Download Pdf Manuals

Related Search

Related Contents