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 confidential 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,logicalflaws in the protocol design may lead to incorrect behavior with undesired consequences.Maybe the most prominent example showing that cryptographic protocols are notoriously difficult to design and test is the Needham-Schroeder protocol for authentification.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 verification,the best we can hope for is either to identify decidable sub-classes as in[1,21,16]or to develop correct but incomplete verification algorithms as in[18,12,11].

In this talk,we present a correct but,in general,incomplete verification 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-defined messages,are not revealed to unauthorized agents.Our contribution is two fold:

1.We define 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 specified by messages and are associated to sessions.All of this makes our model infinite.Therefore,we introduce a general and generic abstraction that reduces the problem of secrecy verification 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 tofix 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,.Wefix 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 identifications:

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

115