A Computationally Sound Mechanized Prover for Security Protocols Bruno Blanchet

Bruno Blanchet

Description

Niveau: Supérieur, Doctorat, Bac+8
A Computationally Sound Mechanized Prover for Security Protocols Bruno Blanchet?† May 25, 2007 Abstract We present a new mechanized prover for secrecy properties of security protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these games are formalized in a probabilistic polynomial-time process calculus. Our tool provides a generic method for speci- fying security properties of the cryptographic primitives, which can handle shared-key and public-key encryption, signatures, message authentication codes, and hash functions. Our tool pro- duces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. We have implemented our tool and tested it on a number of exam- ples of protocols from the literature. 1 Introduction There exist two main approaches for analyzing security proto- cols. In the computational model, messages are bitstrings, and the adversary is a probabilistic polynomial-time Turing machine. This model is close to the real execution of protocols, but the proofs are usually manual and informal. In contrast, in the for- mal, Dolev-Yao model, cryptographic primitives are considered as perfect blackboxes, modeled by function symbols in an al- gebra of terms, possibly with equations. The adversary can compute using these blackboxes.

• let xm


• suchthat defined


• variable access


• single definition


• when i1


• sev- eral security


• security parameter


• can then


• mj then

Sujets

• Blanchet
• Security parameter

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 22
• Langue: English

Extrait

A Computationally Sound Mechanized Prover for Security Prot ocols Bruno Blanchet ∗† May 25, 2007 Abstract tool produces proofs valid for a number of sessions polynomi al in the security parameter, in the presence of an active adver sary. We present a new mechanized prover for secrecy properties of  These proofs are presented as sequences of games, as used by security protocols. In contrast to most previous provers, o ur tool  cryptographers [16,44,45]: the initial game represents th e proto- does not rely on the Dolev-Yao model, but on the computational  col to prove; the goal is to show that the probability of breaking model. It produces proofs presented as sequences of games;  a certain security property (secrecy in this paper) is negli gible in these games are formalized in a probabilistic polynomial-t ime  this game; intermediate games are obtained each from the pre - process calculus. Our tool provides a generic method for spe ci-  vious one by transformations such that the difference of pro b- fying security properties of the cryptographic primitives , which  ability between consecutive games is negligible; the nal game can handle shared-key and public-key encryption, signatures,  is such that the desired probability is obviously negligible from message authentication codes, and hash functions. Our tool pro-  the form of the game. The desired probability is then negligi ble duces proofs valid for a number of sessions polynomial in the  in the initial game. security parameter, in the presence of an active adversary. We  We re re lus. This calculus is in - haveimplementedourtoolandtesteditonanumberofexam- spiredby p th s e en p t i- g c a al m c e u s l i u n s a an p d ro b c y es t s h c e al c c a u lculiof[33,34,39]and ples of protocols from the literature.  of [32]. In this calculus, messages are bitstrings, and cryp- tographic primitives are functions from bitstrings to bits trings. 1 Introduction i T n h p e o c l a y l n c o ul m u i s al h t a i sa e. pr T o h b e ab m il a i i st n ic to s o e l m f a or nt s i p cs e , ci a f n y d in al g l s p e r c o u c r e it s y sesrun m prop- There exist two main approaches for analyzing security prot o-  erties is observational equivalence: Q is observationally equiv- cols.Inthecomputationalmodel,messagesarebitstrings,and a al b e il n i t t to f Q ′ d , is Q tin ≈ gu Q is ′ h , in w g he Q nt f h r e o a m dv Q e ′ r . sar W y it h h as re a sp n e e c g t li t g o ib p l r e e p v r i o o b u - s the adversary is a probabilistic polynomial-time Turing ma chine.  y o This model is close to the real execution of protocols, but the  calculi mentioned above, our calculus introduces an import ant proofsareusuallymanualandinformal.Incontrast,inthefor- no l vel t t h y e w v h al ic u h es is of k a e l y lv f a o r r i t a h b e le a s u d t u o r m in a g ti t c he pr e o x o e f c o u f ti s o e n c o u f rit a yproto- mal, Dolev-Yao model, cryptographic primitives are consid ered  co s: process asperfectblackboxes,modeledbyfunctionsymbolsinanal- a h re c s o t p o y re o d f i t n h a e rr p a r y o s c . es F s o t r h i a n t st d a e n  ce n , es x x [ i . ] i A s r t r h a e ys v r a e lu pl e a o c f el x is i t n s t o h f e te i n - gebraofterms,possiblywithequations.Theadversarycan t usedbycryptographersintheirmanualproofsofprotocols.For compute using these blackboxes. This abstract model makes itpossibletobuildautomaticvericationtools,butthesecurity t e i x c a at m io p n le c , o c d o e n ( si M de A r C th ). e I d n e fo  r n m it a i l o l n y, o t f hi s s ec d u e ri  t n y it o i f o a ns m a e y s s sa th g a ea h u e th a e d n - - proofs are in general not sound with respect to the computati onal  t t model. versary has a negligible probability of forging a MAC, that i s, SincetheseminalpaperbyAbadiandRogaway[3],therehas t o h ra at cl a e l . l S c o o , rr i e n ct cry M p A to C g s ra h p a h v i e c b p e r e o n of c s, o o m n p e ut d e e d  b n y es ca a ll l i is n t g c t o h n e tai M ni A n C g been much interest in relating both frameworks (see for exam -  the arguments of calls to the MAC oracle, and when ch ki ple [1, 9, 12, 23, 27, 28, 37, 38]), to show the soundness of the  ec ng a Dolev-Yaomodelwithrespecttothecomputationalmodel,and t M his A l C ist o , f w a i m h e a ss n a e g g e lig m ib , le on c e ha c n a g n e a i d n di p t r i o o b n a a b ll il y it c y. he I c n k o t u h r a c t al m cu i l s u i s n , thus obtain automatic proofs of protocols in the computational  t model. However, this approach has limitations: since the com-  the arguments of the MAC oracle are stored in arrays, and we putational and Dolev-Yao models do not correspond exactly, ad-  p m e . rfo A r r m y a s lo m o a k k u e p it in ea t s h i e e s r e to ar a ra ut y o s m in ate or p d r e o r o t f o ss  in n c d e t t h h e ey m a e r s e sa a g l- e ditional hypotheses are necessary in order to guarantee sou nd-  ra  in the calcul s: one does not need to add explicit ness. (For example, key cycles have to be excluded, or a specic  ways present u securitydenitionofencryptionisneeded[5].) i i n nst m ru a c n t u i a o l ns pr t o o o i f n s s . er T t h v e a r l e u f e o s re i , nt m h a e n m y , t in iv c ia o l n l t y ra s s o t u t n o d th b e ut lis d t i s f us cu e l d t Inthispaper,weproposeadifferentapproachforautomat- toautomatesyntactictransformation r sdisappear.Furthermore, ically proving protocols in the computational model: we have builtamechanizedproverthatworksdirectlyinthecomputa- r e e q lati li o t n ie s s b , e p t o w s e s e ib n ly el i e n m vo e l n v t i s n o g f c a o rr m a p ys ut c a a ti n o e n a s s o il n y a b rr e a e y x i p n r d e i s c s e e s d . by tional model, without considering the Dolev-Yao model. Our  ua ´ Our prover relies on a collection of game transformations, i n ∗ B.BlanchetiswithCNRS,EcoleNormaleSup ´ erieure,Paris,France E-mail: [e-mail] order to transform the initial protocol into a game on which † A short version of this paper appears at IEEE Symposium on Security and the desired security property is obvious. The most importan t Privacy, Oakland, California, May 2006. kind of transformations exploits the denition of security cryp- 1

tographic primitives in order to obtain a simpler game. As de - M N ::= terms scribed in Section 3.2, these transformations can be specied i replication index in a generic way: we represent the denition of security of each x [ M 1      M m ] variable access cryptographic primitive by an observational equivalence L ≈ R , f ( M 1      M m ) function application where the processes L and R encode functions: they input the arguments of the function and send its result back. Then, the Q ::= input process prover can automatically transform a process Q that calls the 0 nil functions of L (more precisely, contains as subterms terms that Q | Q ′ parallel composition perform the same computations as functions of L ) into a process ! n i e ≤ w n C Q hannel c ; Q r c e h p a li n c n a e t l io re n st n ri t c i ti m o e n s Q ′ that calls the functions of R instead. We have used this tech- e e nique to specify several variants of shared-key and public-key c [ M 1      M l ]( x 1 [ i ] : T 1      x k [ i ] : T k ); P encryption, signature, message authentication codes, and hash  input functions, simply by giving the appropriate equivalence L ≈ R to the prover. Other game transformations are syntactic tra ns- P ::= c [ M 1      M l ] h N 1  output process a ion of     N k i ; Q output f cr o y r p m t a o t g i r o a n p s, hi u c s p e r d im in iti o v r e d s e , r o t r o to b s e i a m b p l l e if t y o th p e p g l a y m th e e o d bt e a  in n e it dafter new x [ i 1      i m ] : T ; P random number l ions. let x [ i 1      i m ] : T = M in P assignment appyingthesede e nit if defined ( M 1      M l ) ∧ M then P else P ′ In order to prov protocols, these game transformations are  conditional organized using a proof strategy based on advice: when a tran s- e e formation fails, it suggests other transformations that sh ould be find ( L j m =1 u j 1 [ i ] ≤ n j 1      u jm j [ i ] ≤ n jm j applied before, in order to enable the desired transformati on. suchthat defined ( M j 1      M jl j ) ∧ M j then P j ) Thanks to this strategy, protocols can often be proved in a fully else P array lookup automatic way. For delicate cases, our prover has an interac - tive mode, in which the user can manually specify the trans-  Figure 1: Syntax of the process calculus formations to apply. It is usually sufcient to specify a few transformations i c n omi h n e g c fr o omthesecuritydenitionsofprimi- denotedby | S | . If S is a nite set, x ← R S chooses a random t t i h v e es c , o b nc y e i r n n d e i d ca s t ecr g et t keyif n a c n e y r ; ne th d e c p r r y o p v to er gr i a n p fe h r i s c t p h r e i i m n i t t e iv r e me a d n i d - elementuniformlyin S and assigns it to x . If A is a probabilis- ate syntactic transformations by the advice strategy. This mode  tic algorithm, x ← A ( x 1      x m ) denotes the experiment of ub choosing random coins r and assigning to x the result of running i e s ra h l el s p e f c u u l ri f t o y r d p e ro  v n i i n ti g o s n o s m o e f p prim li i c t - iv k e e s y c p a ro n to b c e ol a s p , p i l n ie w d, hi b c u h t s o e nl v y - A ( x 1      x m ) with coins r . Otherwise, x ← M is a simple as- one leads to a proof of the protocol. Importantly, our prover  signment statement. is always sound: whatever indications the user gives, when the d pr e o e v d e h r o s l h d o s w a s ss a u se m c i u n r g it t y he pr g o i p v e e r n ty h o y f p t o h t e he p s r e o s to o c n o t l, h t e h c e r p y r p o to pe g r ra ty ph in ic - 2 A Calculus for Games primitives. Our prover CryptoVerif has been implemented in Ocaml 2.1 Syntax and Informal Semantics i ( s 17 a 3 v 0 a 0 ila li b n le es a o t f h c t od t e p: f / or /w v w er w si . o d n i. 1. e 0 n 3 s o . f fr C / ry ˜ p b to l V a e n ri c f) he a t n / d The  syntax of our calculus is summarized in Figure 1. This crypt html . calculus was inspired by the pi calculus and by the calculi oc-eng. of [33, 34, 39] and of [32]. We denote by η the security pa- rameter, which determines in particular the length of keys. 1.1 Outline This calculus assumes a countable set of channel names, de- The next section presents our process calculus fo in  noted by c . There is a mapping maxlen η from channels to inte- games.Section3describesthegametransforma r ti re n p s re t s h e a n t t we g gers,suchthat maxlen η ( c ) is the maximum length of a message o sent  on channel c . Longer messages are truncated. For all c , use for proving protocols. Section 4 gives criteria for prov ing se- maxlen η ( c ) is polynomial in η . (This is key to guaranteeing crecy properties of protocols. Section 5 explains how the pr over  that all processes run in probabilistic polynomial time.) chooses which transformation to apply at each point. Section 6  Our calculus also uses parameters, denoted by n , which cor- presents our experimental results. Section 7 discusses rel ated  respond to integer values polynomial in the security parame ter. t w io o n rk al a f n or d m S a e l c d ti e o ta n ils 8 , c pr o o n o c f lu s d k e e s t . che T s h , e an a d pp d e et n a d i i l c s e o s n c t o h n e ta m i o n d a el d i d n i g - So,denotingby I η ( n ) the interpretation of n for a given value of some cryptographic primitives.  of the security parameter η , I η ( n ) is a polynomially bounded, efciently computable function of η . Our calculus also uses types, denoted by T . For each value 1.2 Notations of the security parameter η , each type corresponds to a subset I η ( T ) of Bitstring ∪ {⊥} where Bitstring is the set of all bit- We recall the following standard notations. We denote by strings and ⊥ is a special symbol. The set I η ( T ) must be recog- { M 1 x 1      M m x m } the substitution that replaces x j with nizable in polynomial time, that is, there exists an algorithm that M j for each j ≤ m . The cardinal of a set or multiset S is decides whether x ∈ I η ( T ) in time polynomial in the length of 2

e e x and the value of η . Let xed-length types be types T such that u j 1 [ i ] ≤ n j 1      u jm j [ i ] ≤ n jm j can be further abbreviated I η ( T ) is the set of all bitstrings of a certain length, this length u e j [ e i ] ≤ n f j . A simple example is the following: find u ≤ n being a function of η bounded by a polynomial. Let large types u be types T such that | I η 1 ( T ) | is negligible. ( f ( η ) is negligible s a u n c i h n t d h e a x t d u e s fi u n c e h d ( t x h [ at ]) x [ ∧ u ] x i [ s u ] de =  a ne t d he a n nd P x ′ [ e u l ] se = P a t , ri a e n s d to w  he n n d when for all polynomials q , there exists η o ∈ N such that for  such a u is found, it executes P ′ with that value of u ; other- all η > η 0 , f ( η ) ≤ q (1 η ) .) Particular types are predened: bool , wise,  it executes P . In other words, this find construct looks such that I η ( bool ) = { true  false } , where false is 0 and true is for the value a in the array x , and when a is found, it stores 1; bitstring , such that I η ( bitstring ) = Bitstring ; bitstring ⊥ in u an index such that x [ u ] = a . Therefore, the find con- such that I η ( bitstring ⊥ ) = Bitstring ∪ {⊥} ; [1  n ] where n struct allows us to access e arrays, which is k e ey for our purpos e. is a parameter, such that I η ([1  n ]) = [1  I η ( n )] . (We consider  More generally, find u 1 [ i ] ≤ n 1      u m [ i ] ≤ n m suchthat integers as bitstrings without leading zeroes.) defined ( M 1      M l ) ∧ M then P ′ else P tries to nd values of The calculus also uses function symbols f . Each function u 1      u m for which M 1      M l are dened and M is true. In symbol comes with a type declaration f : T 1 ×    × T m → c T a h s i e si o s f f s u u r c th ce er ss g , e it ne e r x a e li c z u e te d s to P ′ . m I b n ra ca n s c e he o s f : f fi ai n lu d r ( e, L it j m e = x 1 ec u j ut 1 e [ i e s ] P ≤ . T . For each value of η , each function symbol f corresponds to e a function I η ( f ) from I η ( T 1 ) ×    × I η ( T m ) to I η ( T ) , such n j 1      u jm j [ i ] ≤ n jm j suchthat defined ( M j 1      M jl j ) ∧ that I η ( f )( x 1      x m ) is computable in polynomial time in the M j then P j ) else P tries to nd a branch j in [1  m ] such that lengths of x 1      x m and the value of η . Particular functions  there are values of u j 1      u jm j for which M j 1      M jl j are are predened, and some of them use the inx notation: M = N dened and M j is true. In case of success, it executes P j . for the equality test, M 6 = N for the inequality test (both taking  In case of failure for all branches, it executes P . More for- two values of the same type T and returning a value of type  mally, it evaluates the conditions defined ( M j 1      M jl j ) ∧ M j e e bool ), M ∨ N for the boolean or, M ∧ N for the boolean and,  for each j and each value of u j 1 [ i ]      u jm j [ i ] in [1  n j 1 ] × ¬ M for the boolean negation (taking and returning values of    × [1  n jm j ] . If none of these conditions is true , it exe- type bool ). cutes P . Otherwise, it chooses randomly with uniform 1 prob- e e In this calculus, terms represent computations on bitstrin gs.  ability one j and one value of u j 1 [ i ]      u jm j [ i ] such that the The replication index i is an integer which serves in distin-  corresponding condition is true and executes P j . The condi- guishing different copies of a replicated process ! i ≤ n . (Repli-  tional if defined ( M 1      M l ) ∧ M then P else P ′ executes P cation indices are typically used as array indices.) The vari-  if M 1      M l are dened and M evaluates to true . Otherwise, able access x [ M 1      M m ] returns the content of the cell of  i fi t n e d xe s c u u c t h e t s h P at ′ . d T efi hi n s e c d o ( n M di 1 t  i  o  n  a  l i M s l d ) e ∧ n M ed t a h s e s n yn P ta e ctic su ′ gar T f h o e r indices M 1      M m of the m -dimensional array variable x . lse P . We use x y z u as variable names. The function application  conjunct defined ( M 1      M l ) can be omitted when l = 0 and f ( M 1      M m ) returns the result of applying function f to M can be omitted when it is true . M 1      M m . Finally, let us explain the output c [ M 1      M l ] h N 1      The calculus distinguishes two kinds of processes: input pro- N k i ; Q . A channel c [ M 1      M l ] consists of both a chan- cesses Q are ready to receive a message on a channel; output c nel all n o a w me u c s a t n o d d a e t  u n pl e e p o r f iv te at r e ms ch M an 1  n  el  s   to M l . wh C i h h an t n h e e ln a a d m ve e r s - processes P output a message on a channel after executing some  r h e access, by newChannel c . c (Thisisuse- internal computations. The input process 0 does nothing; Q | Q ′ s f a u r l y in ca t n he ne p v r e oofs a , v althoughallchannelsofprotocolsareof is the parallel composition of Q and Q ′ ; ! i ≤ n Q represents n - copies of Q in parallel, each with a different value of i ∈ [1  n ] ; ten public.) Terms M 1      M l are intuitively analogous to newChannel c ; Q creates a new private channel c and executes  IP addresses and ports which are numbers that the adversary e may guess. A semantic conguration al consists of a Q ; the semantics of the input c [ M 1      M l ]( x 1 [ i ] : T 1      ways e single output process (the process currently being execute d) x k [ i ] : T k ); P will be explained below together with the seman-  and everal input processes. When the output pr tics of the output.  s ocess exe- The output process new x [ i 1      i m ] : T ; P choosesanew c o u n te c s ha c n [ n M e 1 l  c  [  M  l ′  M  l  ] h  N M 1 l ′  ]  ,   w  h N er k e i ; M Q 1 ′ ,   o  n  e  l M o l o ′ k e s va f l o u r at a e n t i o np th u e t random number uniformly in I η ( T ) , stores it in x [ i 1      i m ] , same  bitstrings as M 1     M l , and with the same arity k , and executes P . (The type T must be a xed-length type,  in the available input proce  sses. If no such input process is because probabilistic polynomial-time Turing machines can  found, the process blocks. Otherwise, one such input pro cess choose random numbers uniformly only in such types.) Func- e e c [ M ′ 1      M l ′ ]( x 1 [ i ] : T 1      x k [ i ] : T k ); P is chosen ran- t n i u on b s e y r m s b m ol u s st r b e e pr c e h se os nt en d b et y er n m e i w ni x st [ i i c 1  f  u  n  c  t i io m n ] s : , T s . o D al e l te r r a m n i d n o is m - domlywithuniformprobability.Thecommunicationisthenex- m ecuted:  for each j ≤ k , the output message N j is evaluated, its t c i a c n fu d n u c p ti li o c n a s te m a ak t e er a m uto wi m th at o i u c t s c y h nt a a n c g ti i c ng m i a t n s ip v u al la u t e i . on T s h e e as p i r e o r: ce w s e s resultistruncatedtolength maxlen η ( c ) , the obtained bitstring ( le w t h x ic [ i h 1  m  u  s  t  b i e m i ] n : I T η ( T = ) ) M in i x n [ i P 1  s  t  o  r  e i s m th ] e an b d its e t x ri e n c g ut v e a s lu P e . o N f ex M t, 1 A probabilistic polynomial-time Turing machine can choose a random num- m e ≤ n j 1     j [ i e ] ≤ ber uniformly in a set of cardinal m only when m is a power of 2. When m is L j =  u jm obtain a random integer in [0  m − 1] , we can choose a random integer r uni- we explain the process find ( 1 u j 1 [ i ] not a power of 2, there exist approximate algorithms: for example, in order to n jm j su e chthat defined ( M j 1      M jl j ) ∧ M j then P j ) else P , formly among [0  2 k − 1] for a certain k large enough and return r mod m . where i denotes a tuple i 1      i m ′ . The order and array in- The distribution can be made as close as we wish to the uniform distribution by dices on tuples are taken component-wise, so for instance, choosing k large enough.

3

e is stored in x j [ i ] if it is in I η ( T j ) (otherwise the process blocks). (last item). Both invariants are checked by the prover for th e Finally, the output process P that follows the input is executed. initial game and preserved by all game transformations. The input process Q that follows the output is stored in the avail-  We say that a function f : T 1 ×    × T m → T is poly- able input processes for future execution. Note that the syntax injective when it is injective and its inverses can be computed in requires an output to be followed by an input process, as in [32].  polynomial time, that is, there exist functions f j − 1 : T → T j If one needs to output several messages consecutively, one can  ( 1 ≤ j ≤ m ) such that f j − 1 ( f ( x 1      x m )) = x j and f j − 1 can simply insert ctitious inputs between the outputs. The adver-  be computed in polynomial time in the length of f ( x 1      x m ) sary can then schedule the outputs by sending messages to these  and in the security parameter. When f is poly-injective, inputs. we  dene a pattern matching construct let f ( x 1      x m ) = Using different channels for each input and output allows the M in P else Q as an abbreviation for let y : T = M in adversary to control the network. For instance, we may write let x 1 : T 1 = f 1 − 1 ( y ) in    let x m : T m = f m − 1 ( y ) in ! i ≤ n c [ i ]( x [ i ] : T )    c ′ [ i ] h M i    The adversary can then decide if f ( x 1      x m ) = y then P else Q . We naturally generalize which copy of the replicated process receives its message, s im-  this construct to let N = M in P else Q where N is built from ply by sending it on c [ i ] for the appropriate value of i . poly-injective  functions and variables. An else branch of find or if may be omitted when it is P the set les that occur in P and else yield hi ; 0 . (Note that “ else 0 ” would not be syntactically  by f W c e ( P d ) en th ot e e s b et y o v f a f r r ( ee ) channels o o f f v P a . ri ( ab Weusesimilarnotations correct.) A trailing 0 after an output may be omitted.  for input processes.) Variables can be dened by assignments, inputs, restrictions, and array lookups. The current replication indices at a certain program point in a process are i 1      i m where the replications 2.2 Example above the considered program point are ! i 1 ≤ n 1    ! i m ≤ n m . We  Let us introduce two cryptographic primitives that we use be low. often abbreviate x [ i 1      i m ] by x when i 1      i m are the cur- rent replication indices, but it should be kept in mind that this is only an abbreviation. Variables dened under a replication must  i D nt e u  it n i i v t e i l o y n t 1 o L ra e n t d T o m m r , se T e m d k s, ,a k n e d ys, T m an s d be m t e y s p sa es ge th a a u t t c h o e r n r t e i s c p at o i n o d n be arrays: for example ! i 1 ≤ n 1    ! i m ≤ n m let x [ i 1      i m ] : T = M in    Moreformally,werequirethefollowinginvariant: t c h o e d n e t s i , ca r t e i s o p n e c ct o i d v e el [ y 1 ; 5 T ] m co r n i s s is a ts  o x f e t d h - r l e e e n f g u th nc t t y io p n e. sy A m m bo e l s s s : ageau- Invariant 1 (Single denition) The process Q 0 satises Invari- • mkgen : T mr → T mk where I η (mkgen) = mkgen η is ant 1 if and only if  the key generation algorithm taking as argument a random n and returni 1. in every denition of x [ i 1      i m ] in Q 0 ,theindices b d i o ts m tr i igngak s e i y.(Usually, m e k t g h e e n c i h s oi a ce ra o n f - i 1      i m of x arethecurrentreplicationindicesatthat rando z m ed n a u l m go b r e i r t s h f m r ; om he c re o , mp n u c ta e ti w on e , se m p k a g r e at n takes an addi- denition, and  tional argument representing the random coins.) 2. two different denitions of the same variable x in Q 0 are in • mac : bitstring × T mk → T ms where I η (mac) = mac different branches of a find (or if ). is  the MAC algorithm taking as argument a message an η d Invariant 1 guarantees that each variable is assigned at mos t once  a key, and returning the corresponding tag. (We assume for each value of its indices. (Indeed, item 2 shows that only one  here that mac is deterministic; we could easily encode a denition of each riable can be executed for given indices in  randomized mac by adding an additional argument as for va each trace.) mkgen .) • check : bitstring × T mk × T ms → bool where I η (check) = Invariant 2 (Dened variables) The process Q 0 satises In- check η is a checking algorithm such that check η ( m k t ) = x v [ ar M ia 1 n  t   2   if M an m d ] i o n nl Q y 0 i i f s e e v it e h r e y r occurrenceofavariableaccess true if and only if t is a valid MAC of message m under key k . (Since mac is deterministic, check η ( m k t ) is typically • syntactically under the denition of x [ M 1      M m ] (in mac η ( m k ) = t .) i w n h d i i c c h es c a a t se the M d 1  e    n  i  tio M n m of a x re ) infactthecurrentreplication Wehave ∀ m ∈ Bitstring  ∀ r ∈ I η ( T mr )  check η ( m ; mkgen η ( r )  mac η ( m mkgen η ( r ))) = true . A MAC is UF-CMA (satises unforgeability under chosen • or in a defined condition in a find process; message  attacks) if and only if for all polynomials q , ′′ e m e • o P n f r j i w s n u h c e M r h e j ′ th f o a o r t r P s d j o e i m fi n n e a e k d p ( r ≤ o M c l e j ′ j 1 s ,  s  x o  [ f  M t  h 1 e M  f j ′  o l j r  )  m ∧ M fin m M d ] j ′ i ( s t L h a e j s n = u 1 b P t u j e j ) r [ i m e ] ls o ≤ e f m A ax Pr " ( r m ← R t I ) η ( ← T m A r ) m ; a k c η ( ← k ) m  c k h g ec e k n η η (  (  r k )  ; ) : check η ( m k t ) # M ′ jk . isnegligible,wheretheadversary A is any probabilistic Turing Invariant 2 guarantees that variables can be accessed only when  machine, running in time q ( η ) , with oracle access to mac η (  k ) they have been initialized. It checks that the denition of the  and check η (  k  ) , and A has not called mac η (  k ) on message variable access is either in scope (rst item) or checked by a find m .

4

Denition 2 Let T r and T r ′ be xed-length types; let T k and MAC under x mk of the ciphertext, and sends the ciphertext and T e be types. A symmetric encryption scheme [13] consists of the MAC on c A [ i ] . The function k2b : T k → bitstring is the three function symbols kgen : T r → T k , enc : bitstring × natural injection I η (k2b)( x ) = x ; it is needed only for type T k × T r ′ → T e , and dec : T e × T k → bitstring ⊥ , with conversion. The context is then expected to forward this mes - I η (kgen) = kgen η , I η (enc) = enc η , I η (dec) = dec η , such sage on c B [ i ] . When Q B receives this message, it checks the that for all m ∈ Bitstring , r ∈ I η ( T r ) , and r ′ ∈ I η ( T r ′ ) , MAC, decrypts, and stores the obtained key in x ′ k ′ . (The func- dec η (enc η ( m kgen η ( r )  r ′ )  kgen η ( r )) = m . tion i ⊥ : bitstring → bitstring ⊥ is the natural injection; it is Let LR ( x y b ) = x if b = 0 and LR ( x y b ) = y if b = 1 , useful to check that decryption succeeded.) This key x ′ k ′ should dened only when x and y are bitstrings of the same length. be secret. A symmetric encryption scheme is IND-CPA (satises indistin- The context is responsible for forwarding messages from A to guishability under chosen plaintext attacks) if and only if for all B . It can send messages in unexpected ways in order to mount polynomials q , an attack. Although we use a trivial running example due to length con- m A ax 2 Pr " b b ′ R ← ← { 0 A  1 r ′ } ; ← R r I η ← R ( T I r ′ η ); ( e T nc r η ) ( ; L k R ( ←  k b ) g k e  n r ′ η ) ( r : ) b ; ′ = b # − 1 i s o s t f r ti a o c i u n p r t r s, p o r t t o o h v c i o s e l r e . s. x S a e m ct p i l o e n is 6 s p u r f e  se c n ie ts nt re t s o u i l l t l s us o t b r t a a t i e n t e h d e o m n ai m n o f r e e at r u e r a e l s - is negligible, where the adversary A is any probabilis- tic Turing machine, running in time q ( η ) , with oracle ac- 2.3 Type System cess to the left-right encryption algorithm which, given  We use a type system to check that bitstrings of the proper type two bitstrings a 0 and a 1 of the same length, returns r ′ ← R I η ( T r ′ ); enc η ( LR ( a 0  a 1  b )  k r ′ ) , that is, encrypts a 0 r a e re ctl p y a . ssedtoeachfunctionandthatarrayindicesareusedcor- when b = 0 and a 1 when b = 1 . To  be able to type variable accesses used not under their de- Example 1 Letusconsiderthefollowingtrivialprotocol: c ni h t e i c o k n i ( n s g uc a h lg a o c ri c t e h ss m es pr a o re ce g e u d a s rd i e n d t b w y o a p fi as n s d es c . on I s n tr t u h ct e ),  th rs e t ty p p as e s - , A → B : e mac( e x mk ) where e = enc( x ′ k  x k  x ′ r ′ ) t it o b ty ui p l e d s s [ a 1  ty n p 1 ] e × en  v  ir  o × nm [1 e  nt n m E , ] w → hic T h , m w a h p e s re v t a h ri e ab d l e e  n n a it m i es o x f and x ′ r ′  x ′ k are fresh random numbers x [ i 1      i m ] of type T occurs under replications ! i 1 ≤ n 1 , o . n .., A and B are assumed to share a key x k for a symmetric encryp- ! i m yi ≤ e n ld m t . h T e h s e a t m o e ol v c al h u e e ck o s f t E h ( at x ) a , ll s d o e t  ha n t iti E o i n s s p o r f o t p h e e rl s y a d m e e  v n a e ri d a . ble tion scheme and a key x mk for a message authentication code. x A creates a fresh key x ′ k and sends it encrypted under x k to B . vir I o n n t m h e e n s t ec E o b n y dp a a s s i s, m t p h l e et p y ro p c e e s s y s s i t s e t m y . pe T c h h i e s c t k y e p d e in sy t s h t e e t m yp is e d e e n - - A MAC is appended to the message, in order to guarantee in-  tailed in Appendix A. It denes the judgment E ⊢ Q , which tegrity. The goal of the protocol is that x ′ k should be a secret key  means that the process Q is well-typed in environment E . shared between A and B . This protocol can be modeled in our calculus by the following process Q 0 : Invariant 3 (Typing) The process Q 0 satises Invariant 3 if Q 0 = start (); new x r : T r ; let x k : T k = kgen( x r ) in and only if the type environment E for Q 0 is well-dened, and new x ′ r : T mr ; let x mk : T mk = mkgen( x ′ r ) in E ⊢ Q 0 . c hi ; ( Q A | Q B ) We require the adversary to be well-typed. This requirement Q A = ! i ≤ n c A [ i ](); new x ′ k : T k ; new x ′ r ′ : T r ′ ; d  o n e e s t n y o p t e r - e c s a t s ri t c f t u i n ts ct c io o n m s p f ut : in T g p → ow T e ′ r, to be b c y a p u a s s e s i t t h c e a t n y a p l e w s a y y s s te d m e . - let x m : bitstring = enc(k2b( x ′ k )  x k  x ′ r ′ ) in Similarly, the type system does not restrict the class of pro tocols c A [ i ] h x m  mac( x m  x mk ) i that we consider, since the protocol may contain type-cast func- Q B = ! i ′ ≤ n c B [ i ′ ]( x ′ m  x ma ); tions. The type system just makes explicit which set of bitstrings may appear at each point of the protocol. if check( x ′ m  x mk  x ma ) then let i ⊥ (k2b( x ′ k ′ )) = dec( x ′ m  x k ) in c B [ i ′ ] hi 2.4 Formal Semantics When Q 0 receives a message on channel start , it begins execu- The semantics is dened by a probabilistic reduction relation tion: it generates the keys x k and x mk by choosing random coins formally detailed in Appendix B. The notation E M ⇓ a means x r and x r ′ and applying the appropriate key generation algo- that the term M evaluates to the bitstring a in environment E . rithms. Then it yields control to the context (the adversary ), by We denote by Pr[ Q Ã η c h a i ] the probability that at least one of outputting on channel c . After this output, n copies of processes the outputs of Q on channel c sends the bitstring a . (When c is for A and B are ready to be executed, when the context outputs not free in Q , Pr[ Q Ã η c h a i ] = 0 .) on channels c A [ i ] or c B [ i ] respectively. In a session that runs Our semantics is such that, for each process Q , there exists as expected, the context rst sends a message on c A [ i ] . Then a probabilistic polynomial time Turing machine that simulates Q A creates a fresh key x ′ k ( T k is assumed to be a xed-length Q . (Processes run in polynomial time since the number of pro- type), encrypts it under x k with random coins x ′ r ′ , computes the cesses created by a replication and the length of messages sent

5