Verifying Secrecy by Abstract Interpretation(2)

Verifying Secrecy by Abstract Interpretation

Bozga,Lakhnech,P´e rin

all sessions where(resp.B)plays the role of(resp.)and the role(resp.)is played by

a participant not in,etc...

Identifying sessions means also identifying the nonces and keys used in these sessions.This gives us

a system described as a set of transitions that can be taken in any order and any number of times but

which refer to afinite set of atomic messages.We then have to prove that the secret is not revealed by these rules.Here,we should emphasize that,for instance,the methods of[6,11]can profit from this abstraction as the obtained abstract system can be,in some cases,taken as starting point.

2.Our second contribution is an original method for proving that a secret is not revealed by a set of rules

that model how the initial set of messages known by the intruder evolves.In contrast to almost all existing methods,we do not try to compute or approximate the sets of messages that can be known by the intruder.

Our algorithm is rather based on the notion of”the secret being guarded,or kept under hat by a message”.

For example,suppose that our secret is the nonce and consider the message.Then, is guarded by,if the inverse of is not known by the intruder.The idea is then to compute a set of guards that will keep the secret unrevealed in all sent messages and such that the inverses of the keys used in this set are also secrets.The difficulty here is that this set is,in general, infinite.Therefore,we introduce pattern terms which are terms used to represent sets of guards.For instance the pattern term says that the secret will be guarded in any message, where the secret is not a sub-message of but may be a sub-message of.The problem is,however, that there might be a rule that will send unencrypted to the intruder if(s)he produces the message.Hence,the pattern will guard the secret except when ing this idea,we develop an algorithm that computes a stable set of pattern terms that guard the secrets in all sent messages.We developed a prototype in Caml that implements this method.We have been able to verify several protocols taken from[4]including,for instance,the corrected version of the Needham-Schroeder protocol,different versions of Yahalom,as well as Otway-Rees.

Related work Dolev,Even and Karp introduced the class of ping-pong protocols and showed its decidability. The restriction put on these protocols are,however,too restrictive and none of the protocols of[4]falls in this class.Recently,Comon,Cortier and Mitchell[6]extended this class allowing pairing and binary encryption while the use of nonces still cannot be expressed in their model.Reachability is decidable for the bounded number of sessions[1,21,16]or when nonce creation is not allowed and the size of messages is bounded[9]. For the general case,on one hand model-checking tools have been applied to discoverflaws in cryptographic protocols[13,22,17,5].The tool described in[5]is a model-cheker dedicated to cryptograhic protocols.On the other hand,methods based on induction and theorem proving have been developed(e.g.[20,3,8]).Closest to our work are partial algorithms based on abstract interpretation and tree automata that have been presented in[18,12,11].The main difference is,however,that we do not compute the set of messages that can be known by the intruder but a set of guards as explained above.

Another remark is that the operational semantics we provide in this paper is well-suited to investigate and relate several existing models that one canfind in the literature such as the semantics using clauses to model transitions(e.g.[2])or linear-logic(e.g.[9]).In an ongoing work,we use this semantics to prove relationships between these models.

References

[1]R.M.Amadio et D.Lugiez.On the reachability problem in cryptographic protocols.In International

Conference on Concurrency Theory,volume1877,pages380–394,2000.

[2]B.Blanchet.Abstracting cryptographic protocols by Prolog rules(invited talk).In Patrick Cousot,editor,

8th International Static Analysis Symposium(SAS’2001),volume2126of Lecture Notes in Computer Science,pages433–436,Paris,France,July2001.Springer Verlag.

116