Verifying Secrecy by Abstract Interpretation

Verifying Secrecy by Abstract Interpretation

septembre2002–S´Ecurit´e des Communications sur Internet–SECI02 Verifying Secrecy by Abstract Interpretation

L.Bozga&khnech&M.P´e rin

V´e rimag

2,avenue de Vignate

38610Gires,France

lbozga,lakhnech,perin@imag.fr

1.Introduction

At the heart of almost every computer security architecture is a set of cryptographic protocols that use cryptography to encrypt and sign data.They are used to exchange con?dential data such as pin numbers and passwords,to authentify users or to guarantee anonymity of participants.It is well known that even under the idealized assumption of perfect cryptography,logical?aws in the protocol design may lead to incorrect behavior with undesired consequences.Maybe the most prominent example showing that cryptographic protocols are notoriously dif?cult to design and test is the Needham-Schroeder protocol for authenti?cation.It has been introduced in1978[19].An attack on this protocol has been found by G.Lowe using the CSP model-checker FDR in1995[13];and this led to a corrected version of the protocol[14].Consequently there has been a growing interest in developing and applying formal methods for validating cryptographic protocols[15,7]. Most of this work adopts the so-called Dolev and Yao model of intruders.This model assumes idealized cryptographic primitives and a nondeterministic intruder that has total control of the communication network and capacity to forge new messages.It is known that reachability is undecidable for cryptographic protocols in the general case[10],even when a bound is put on the size of messages[9].Because of these negative results, from the point of view of veri?cation,the best we can hope for is either to identify decidable sub-classes as in[1,21,16]or to develop correct but incomplete veri?cation algorithms as in[18,12,11].

In this talk,we present a correct but,in general,incomplete veri?cation algorithm to prove secrecy without putting any assumption on messages nor on the number of sessions.Proving secrecy means proving that secrets, which are pre-de?ned messages,are not revealed to unauthorized agents.Our contribution is two fold:

1.We de?ne a concrete operational model for cryptographic protocols,that are given by a set of roles

with associated transitions.In general,each transition consists in reading a message from the network and sending a message.Our semantic model allows an unbounded number of sessions and participants, where a participant can play different roles in parallel sessions.Secrets are then speci?ed by messages and are associated to sessions.All of this makes our model in?nite.Therefore,we introduce a general and generic abstraction that reduces the problem of secrecy veri?cation for all possible sessions to verifying a secret in a model given by a set of constraints on the messages initially known by the intruder and a set of rules that describe how this knowledge evolves.Roughly speaking,the main idea behind this abstraction step is to?x an arbitrary session running between arbitrary agents.Then,to identify all the other agents as well as their cryptographic keys and nonces.Thus,suppose we are considering a protocol where each session involves two participants playing the role,respectively,.We?x arbitrary participants, and,and an arbitrary session.We identify all participants other than and and also identify all sessions in which neither nor are involved.Concerning the sessions,where or are involved except,we make the following identi?cations:

all sessions where plays the role(resp.),plays the role(resp.),

115

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 a?nite 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 pro?t 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 dif?culty here is that this set is,in general, in?nite.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,differ …… 此处隐藏：5933字，全部文档内容请下载后查看。喜欢就下载吧 ……