Aldrin

Formal Analysis of Cryptographi Proto ols Submitted in partial ful llment of the requirements For the degree of Master of Te hnology by Aldrin John D'Souza

(Roll No. 01305009) Supervisor Prof. G. Sivakumar

a

Department of Computer S ien e and Engineering INDIAN INSTITUTE OF TECHNOLOGY, BOMBAY De ember 2002

A knowledgments I take this opportunity to express my sin ere thanks and deep sense of gratitude to my advisor Prof. G. Sivakumar for his valuable guidan e and supervision in all phases of the proje t. I am also thankful to the Center of Formal Design and Veri ation of Software and the Department of Computer S ien e, IIT Bombay for providing the ne essary fa ilities and support. I believe, this work wouldn't have been possible without my parents blessings, I owe it all to them. Aldrin John D'Souza

January, 2003.

i

Abstra t The pro ess of designing a orre t ryptographi proto ol does not end with getting the

ryptographi primitives right. The literature is full of proto ols whi h were initially believed to be orre t, and were later found to have aws. Interestingly, most of these are stru tural aws, i.e. the intruder an subvert the goals of the proto ol without breaking the underlying rypto-system. Given the wide range of operations whi h the intruder uses to ompose these atta ks, it is very diÆ ult for the designer to intuitively reason about these atta ks. Formal methods of analysis should thus be applied before the proto ols are put to use. Su h an analysis involves developing property preserving abstra tions of proto ols, spe i ation languages to express goals and assumptions, and pro edures to de ide whether the proto ol a hieves its intent. The Strand Spa e Model is one of the existing ryptographi proto ol analysis me hanisms. Here, we des ribe how proofs in the strand spa es formalism an be generalized and applied to a range of proto ols. We formalize our generalization in PVS and des ribe how a proto ol des ription in a ommon spe i ation language an be translated to theories, whi h an be used to prove the orre tness of proto ol properties.

ii

Contents

1. Introdu tion

1

1.1. Flaws and Atta ks . . . . . . . . 1.2. Formal Analysis - A Brief Survey 1.2.1. Atta k Constru tors . . . 1.2.2. Proof Generators . . . . . 1.3. S ope of Our Work . . . . . . . . 1.4. Outline . . . . . . . . . . . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

2. The Problem

2.1. Ideal Cryptography . . . . . . 2.1.1. Freeness Assumptions 2.2. The Penetrator . . . . . . . . 2.3. Proto ol Guarantees . . . . . 2.3.1. Authenti ation . . . . 2.3.2. Se re y . . . . . . . .

2 4 5 6 6 7 8

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

3. Spe i ation

8 10 11 11 12 12 13

3.1. CAPSL . . . . . . . . . . . . . . 3.1.1. Type Spe i ations . . . . 3.1.2. Proto ol Spe i ations . . 3.1.3. Environment Spe i ation

. . . .

iii

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

14 15 16 18

Contents

3.2. Intermediate Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4. Modeling

20

4.1. Strand Spa es . . . . . . . . . . . . . 4.1.1. Nodes . . . . . . . . . . . . . 4.1.2. Bundles . . . . . . . . . . . . 4.1.3. Subterms, Interms and Ideals 4.1.4. Origination . . . . . . . . . . 4.1.5. The Penetrator . . . . . . . . 4.2. Modeling Proto ols . . . . . . . . . . 4.2.1. Parameterized Strands . . . . 4.2.2. Freshness . . . . . . . . . . . 4.3. Modeling Corre tness . . . . . . . . . 4.3.1. Se re y . . . . . . . . . . . . 4.3.2. Authenti ation . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

5. Proving Proto ol Corre tness

Using  . . . . . . . . . . . Using  . . . . . . . . . . . Proving Se re y . . . . . . . Proving Authenti ation . . . 5.4.1. Some Notation . . . 5.4.2. Authenti ation Tests 5.5. Using Tests . . . . . . . . . 5.1. 5.2. 5.3. 5.4.

20 21 22 23 24 25 25 26 28 28 28 29 31

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

6. PVS Theories

6.1. Proto ol Independent Theories . 6.1.1. Messages . . . . . . . . . 6.1.2. Penetrator Capabilities . 6.1.3. Proving Se re y . . . . . 6.2. The Translation . . . . . . . . .

32 33 34 34 35 36 38 40

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

41 41 42 43 45 iv

Contents

6.3. Proof in PVS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.4. Otway-Rees Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 7. Con lusion

50

Bibliography

51

A. Intermediate Language DTD

54

B. Otway Rees Example

55

B.1. Intermediate Language Spe i ation . . . . . . . . . . . . . . . . . . . . 55 B.2. PVS Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

v

1. Introdu tion

The need for formally analyzing ryptographi proto ols is emphasized. A brief survey of the work done in this eld is presented. An overview of the our work is given.

Se urity is all about providing guarantees. Authenti ation, for example, is the guarantee that we are indeed ommuni ating with the party we think we are ommuni ating with. Se re y, on the other hand, is the guarantee that the messages we send, are intelligible only to the intended re ipients. Providing these guarantees on the network is diÆ ult, be ause all that we an observe with surety are lo al events, while these guarantees require us to reason about what might have happened a ross the network. This is where network se urity proto ols ome in. A network se urity proto ol - from the perspe tive of a party exe uting it, is a sequen e of lo al events, enough to guarantee the o

urren e of ertain events a ross the network. These global inferen es from lo al observations are enabled by using the properties of

ryptographi transformations that are performed on the messages ex hanged. For instan e, if we send a en rypted message, we an infer than it makes sense only to those who posses the proper de ryption key. The orre tness of this inferen e, obviously, depends on our faith in the underlying rypto-system, but this is not the only fa tor. 1

1.1 Flaws and Atta ks

The literature is full of examples of ryptographi proto ols that were published, believed to be orre t and later found to have aws independent of the strength of the primitives used to implement them. In other words, even if the underlying rypto-system is perfe t, penetrators an subvert the goals of these proto ols. Any new proto ol, must be thoroughly analyzed before being deployed, and this proje t deals with how su h an analysis an be done using formal te hniques of software veri ation.

1.1. Flaws and Atta ks One reason why formal analysis of ryptographi proto ols is required is that, the atta ks are usually hard to gure out intuitively. Cryptographi proto ols rarely have more than four messages per party, but the options available to the penetrator are enough to take all possible exe utions of the proto ol beyond intuitive reasoning. To realize this, onsider the following symmetri key proto ol due to Woo and Lam. (It is assumed that all prin ipals share keys with a xed key server ). S

1.

A

2.

B

3.

A

4.

B

5.

S

! ! ! ! !

B :

A

A :

fNB gKAS fA; fNB gKAS gKBS fNB gKBS

B : S : B :

NB

Figure 1.1.: Woo-Lam Authenti ation Proto ol The authors propose that the proto ol stru ture is enough to provide the guarantee \whenever a responder nishes exe ution of the proto ol, the initiator of the proto ol is in fa t the prin ipal laimed in the initial message."

the orre tness of the proto ol: A

This is how they informally reason

laims its identity in message 1; provides a non e hallenge in message 2; returns B

A

2

1.1 Flaws and Atta ks

this hallenge en rypted under KAS in message 3; passes on this message to for veri ation, bound with 's name en rypted under KBS in message 4; S de rypts fNB gKAS using the key it shares with and re-en rypts the result under 's key and sends it to in the last message. If gets ba k fNB gKBS from , it should be onvin ed that has responded to the non e hallenge, sin e only and know the key KAS . B

S

A

A

B

B

B

S

A

A

S

So far so good, but as we introdu e the penetrator in the system, things start happening. Consider the following run of the proto ol. The penetrator su

eeds in making believe, that it is by starting two on urrent sessions. It uses the information that it derives from one of the sessions to fool into believing that it is in the other session. P

B

A

B

1.

P

1'.

P

2.

B

2'.

B

3.

P

3'.

P

4.

B

4'.

B

5.

S

5'.

S

! ! ! ! ! ! ! ! ! !

A

B :

A

B :

P

A : P : B : B : S : S : B : B :

NB NB0 fNB gKPS fNB gKPS fA; fNB gKPS gKBS fP; fNB gKPS gKBS fNB00 gKBS fNB gKBS

Figure 1.2.: Atta k on Woo-Lam Authenti ation Proto ol Given this atta k, we an reason what is wrong with the proto ol. The last message is intended to be a reply to the query that is presented by to in the fourth message, but nothing in the proto ol stru ture links the two messages. The proto ol impli itly asso iates NB to the laimed identity, and it is pre isely this impli it asso iation that uses to subvert the proto ol goal. The stru ture of the proto ol is awed! B

S

P

The atta k an be avoided if the proto ol makes the relation between 's query and 's response expli it in the last message by repla ing it with fA; NB gKBS . Cryptographi operations aren't wholly heap, and the designer is tempted to do away with parts of B

S

3

1.2 Formal Analysis - A Brief Survey

the messages whi h he thinks aren't ne essary for the orre tness of the proto ol. While su h an optimization is de nitely wel ome, the ee ts of removing information from messages must be thoroughly examined. Apart from the fa t that reasoning intuitively about these proto ols is diÆ ult and error prone, the use of formal methods is essential for another reason. These proto ols are usually omponents of some larger systems, and the riti al nature of the appli ations that these systems support makes it essential to produ e proofs of orre tness before these proto ols are deployed. Systems may be una

eptable to the users in absen e of su h proofs of orre tness. This is indeed one of the reasons, why proto ols like SET

ould never nd widespread usage.

1.2. Formal Analysis - A Brief Survey Formal analysis of ryptographi proto ols has been a eld of a tive resear h in re ent years, several formalisms and me hanisms have been developed and have been used to show that proto ols are orre t. Most of the work done falls into one of the following

ategories Logi s of Knowledge and Belief Dis rete State based Algebrai Systems Complexity Theoreti Analysis The logi al paradigm, makes use of logi s of belief or knowledge to prove orre tness of proto ols. The framework omprises of a set of onstru ts to express the beliefs of proto ol parti ipants and a set of inferen e rules to spe ify how these beliefs hange as the proto ol pro eeds. BAN logi [15℄, introdu ed by Burrows et. al. is the most su

essful attempt that falls under this style of analysis. The approa h enjoys the advantages of being intuitive and easy to use, but the system is abstra ted at a very high level, and several issues like on urren y are ignored. 4

1.2 Formal Analysis - A Brief Survey

Complexity theoreti analysis on the other hand, redu e the problem of atta king the proto ol to some omputationally hard problem, thus proving that it is impossible for a penetrator to atta k the proto ol. This approa h is exible enough to model the proto ol at any level of detail, but an not be generalized or automated. Most of the re ent work done is based on algebrai systems. Here, ryptographi primitives are idealized as types with ertain properties, and the proto ol is onsidered to be a system that uses the properties of these types to provide the required guarantees. Corre tness of proto ols is proved either by sear hing the exe ution spa e for atta ks or by proving mathemati ally that it is impossible for the penetrator to subvert the goals of the proto ol. These orrespond to the two approa hes of analysis namely, atta k

onstru tion and proof generation. 1.2.1. Atta k Constru tors Millen's , Longley and Rigby's sear h tool, are examples of spe ialized exhaustive model he kers whi h attempt to onstru t atta ks. General purpose model

he kers have also been used - Lowe, for instan e used to un over a aw in the Needham-S hroeder proto ol, Mit hell used  to analyze SSL. Ea h of these tools, however sear h the exe ution spa e exhaustively, and require the number of proto ol parti ipants to be spe i ed before the sear h begins. Re ently, Song developed , whi h models the proto ol state symboli ally and an sear h for atta ks with arbitrary number of parti ipants. Another noteworthy tool is Meadows . Like Song's tool, the analyzer onstru ts atta ks ba kward (starting from an undesirable state and sear hing for states that rea hable from the initial state) and thus does not require initial number of parti ipants to be spe i ed. Interrogator

FDR

Mur

Athena

NRL Proto ol Analyzer

NRL

5

1.3 S ope of Our Work

1.2.2. Proof Generators Paulson used to generate indu tive proofs of orre tness of ryptographi proto ols[17℄. Millen used as a proof assistant to obtain proofs based on Paulson's ideas[18℄. S hneider uses to reason about the possibility of events o

urring in the proto ol exe ution [19℄. Thayer et.al. re ently ame up with a graph theoreti model of ausality in a proto ol, alled . Strand spa es form the theoreti al base of our tool, and are des ribed in detail in the following hapters. Abadi and Gordon extend Miller's , to what they all, to prove se re y properties of

ryptographi proto ols[16℄. Isabelle

PVS

rank fun tions

strand spa es

pi- al ulus

spi- al ulus

Having des ribed the problem we are trying to deal with, and the ways it has been dealt with in the past, we present the s ope of our work in the next se tion. Our survey is not exhaustive. The reader is referred to [8, 10, 11℄ for a more detailed des ription of the work done in the eld.

1.3. S ope of Our Work The goal of our proje t is to ome up with an tool that a ryptographi proto ol designer

an use to analyze proto ols that he designs. The following are the features of our tool Graphi al spe i ation of ryptographi proto ols. Read and generate spe i ations. Generation of PVS theories for generating proofs. CAPSL

Strand spa es form the theoreti al base of our tool. Most of the work on proof generation for ryptographi proto ol properties is based on Paulson's indu tive analysis. To the best of our knowledge proofs based on strand spa es haven't been automated. We have developed a framework where

an be used to assist in proving properties of proto ols PVS

6

1.4 Outline

based on the strand spa es formalism.

1.4. Outline We formally de ne the problem of ryptographi proto ol analysis in the next hapter, formalizing the notions of ideal ryptography, the penetrator and the orre tness of a proto ol. The spe i ation language for ryptographi proto ols , is des ribed in Chapter 3. The theoreti al base of our tool, viz. strand spa es in explained in

onsiderable detail in Chapter 4. Strategies for proving proto ol properties are des ribed in Chapter 5. PVS theories for automati proofs are des ribed in Chapter 6.3. CAPSL

7

2. The Problem

The s ope of our analysis is de ned. Notions of ideal ryptography, orre tness, penetrator apabilities are formalized.

Our problem an be informally put as - given a proto ol and the guarantees that it laims to provide, establish whether or not the proto ol a hieves its intent in the presen e of an a tive penetrator, under the assumption that the underlying ryptographi primitives are ideal. This problem statement is in omplete unless we formalize the notions of ideal

ryptography, the apabilities of the intruder and the guarantees that proto ols attempt to provide. We begin with our model of ryptography.

2.1. Ideal Cryptography We treat ryptographi primitives as bla k boxes whi h work exa tly as the proto ol designer expe ts them to. They are formalized as operations de ned on a set of messages. Consider A, the set of all possible messages that an be ex hanged in a proto ol run. We will all elements of A . Terms an belong to the following subsets of A terms

T  A, the set of plain-text omponents like text and non es. N  T, the set of prin ipal names. 8

2.1 Ideal Cryptography

K  A, the set of ryptographi keys, disjoint from T Next, we de ne the ryptographi primitives as operations on the set A. We will restri t ourselves to the following primitives inv

: K!K : KA!A : AA!A

en r join K K

:N!K :NN!K

maps keys to their respe tive inverses. We will denote (K ) by K 1. As a shorthand, we extend to set of keys and denote the the set of inverses of keys in a set S by S 1. denotes en ryption of a term using a key from K. We will denote (K; m) by fmgK . denotes on atenation of two terms. We will denote (a; b) by a b. is overloaded, when given a single prin ipal name it maps it to the publi key orresponding to the prin ipal, we will denote (A) by A, and when given two arguments, it maps to the symmetri key that the two prin ipal share. We will denote (A; B ) by AB . inv

inv

inv

en r

en r

join

join

K

K

K

K

K

Figure 2.1.: The Term Algebra Figure 2.1 gives a pi torial des ription of the term algebra and also the intuitive meaning of the freeness assumption that we des ribe next.

9

2.1 Ideal Cryptography

2.1.1. Freeness Assumptions By abstra ting ryptography as an algebra, we restri ted ourselves to deal with messages as results of operations performed over atomi omponents and not as bit-streams. The 1 restri ts us further. The assumption ensures that there is only one representation of a given message. In parti ular, the following an be inferred from the freeness assumption freeness assumption

A ipher-text an be regarded as a ipher-text in only one way. Formally, fmgK = fm0 gK 0 ) m = m0 ^ K = K 0 A on atenation of two terms an be interpreted in only one way. Formally, m0 m1 = m00 m01 ) m0 = m00 ^ m1 = m01 A on atenation of two terms an not be treated as a valid ipher-text. Formally m0 m1 6= fm00gK 0 A on atenation of two terms an not be taken as a key or a plain-text. Formally, m0 m1 2= K [ T A ipher-text an not be treated as a key or a plain-text. Formally, fm00 gK 0 2= K[T

The most important onsequen e of these assumptions is that we are ignoring what are

alled type- aw atta ks. These atta ks orresponds to situations where the penetrator su

eeds in making a parti ipant read a term as some other term. Avoiding type- aws is mostly an implemention issue, and we, being more on erned with the stru ture of proto ols, will ignore them in our analysis. 1

A

is an algebra freely generated from

T

and

K

by the two operators

en r

and

join.

10

2.2 The Penetrator

2.2. The Penetrator The model of the atta ker that we onsider is was introdu ed by Dolev and Yao[6℄ and is thus alled the . It is apable of the following Dolev-Yao Intruder

Read all network traÆ . Alter or destroy messages. Create new messages. Do anything that a legitimate prin ipal is apable of doing. Apart from these apabilities, another fa tor whi h de nes the strength of the penetrator is its knowledge. The penetrator knows some terms to start with, and it an learn new terms from the messages that are sent over the network. The ability to learn is however limited by the rules of the ryptographi primitives. For instan e, if some proto ol parti ipant sends a term fmgK then the intruder an learn m out of it only if it knows K 1 . The penetrator an also originate a message ontaining terms that it knows or

an reate. To a

ount for dishonest parti ipants, the penetrator is assumed to posses all apabilities of a normal parti ipant. For instan e, it an posses a valid name, an asso iated asymmetri key-pair, and an even share keys with a key server, if any.

2.3. Proto ol Guarantees Se urity proto ols attempt to provide ertain guarantees to the parti ipants, in this se tion we formally de ne these guarantees and des ribe what it means for a proto ol to be orre t. In parti ular, we des ribe the meanings of authenti ation and se re y.

11

2.3 Proto ol Guarantees

2.3.1. Authenti ation In [24℄, Lowe omes up with a hierar hy of authenti ation spe i ations. Our interpretation of authenti ation guarantee orresponds to that of in Lowe's paper. We say a proto ol guarantees authenti ation of B to A i whenever A

ompletes a run of the proto ol, apparently with B, then B has previously been running the proto ol, apparently with A, and the two agents agree on some data values, as required by the proto ol. Note that A and B are parameters to the spe i ation rather than spe i prin ipals. Non-Inje tive Agreement

2.3.2. Se re y Se re y is the requirement that some term doesn't fall into the hands of the penetrator. The formal de nition of depends on how we model the penetrator. It is assumed that the penetrator emits values that it knows, so verifying whether the penetrator an emit a given value in the proto ol run is equivalent to verifying if the proto ol keeps that value se ret.

12

3. Spe i ation

The syntax and semanti s of the spe i ation language

CAPSL

are illustrated with

an example. The features of the intermediate language are des ribed.

In most ases, the system des ription that the analysis me hanism requires does not intuitively orrespond to the analyst's per eption. It is the task of the spe i ation language to provide the analyst with abstra tions loser to what he thinks the system is, and then translate these abstra tions to the formalisms that the analysis me hanism works on. In this hapter, we des ribe , the language whi h does this job for

ryptographi proto ols. CAPSL

As we mentioned, many me hanisms for analyzing ryptographi proto ols exist. In spite of being used su

essfully for analyzing proto ols, it is diÆ ult for analysts other than the original developers to translate onventional proto ol des riptions to the formalisms that these me hanisms require. Also, an analyst wishing to use more than one me hanism has to translate between the spe i ation languages of the two. To summarize, the problems that a ryptographi proto ol analyst fa es are Translating a published des ription of the proto ol to the formalism required by the analysis me hanism is diÆ ult. 13

3.1 CAPSL

Using more than one analysis me hanisms requires translation between the formalisms underlying the me hanisms. It is pre isely to ta kle these problems

[9℄ was developed.

CAPSL

3.1. CAPSL stands for Common Authenti ation Proto ol Spe i ation Language. It was introdu ed by Jonathan Millen, as a ommon spe i ation language that all analysis me hanisms an use. The idea is to in lude all the information needed for analysis in the spe i ation, and allow a \ onne tor" to sele tively hoose and translate the part that its underlying me hanism uses for the analysis. This is made possible by dividing the spe i ation into three modules: CAPSL

- De lare and des ribe ryptographi types, operators and other fun tions axiomati ally. Proto ol Spe i ation Module - De lare the assumptions, messages and goals of the proto ol. Environment Spe i ation Module - De lare run spe i information about the proto ol. Type Spe i ation Module

The types and operations that most ryptographi proto ols use are provided in a , whi h is expe ted to be in luded in all spe i ations. So unless a proto ol uses spe ial fun tions or types, the module an be omitted. Environment spe i ations are used by tools whi h sear h the exe ution spa e of the proto ol for atta ks. This module is optional and an be omitted if su h a sear h is not to be attempted. The most important part of a spe i ation is the proto ol module, des ribing the messages, the assumptions and the goals of the proto ol. prelude

CAPSL

typespe

14

3.1 CAPSL

3.1.1. Type Spe i ations Messages in ryptographi proto ols are onstru ted by ryptographi ally transforming the message omponents. Analysis me hanisms use the properties of these transforming operations to provide guarantees about the possible exe ution of the proto ol. Properties of types and these transformation operations are de lared in the module. A module onsists of some de larations, followed optionally by some axioms. Typespe s usually introdu e a new type and some fun tions de ned on it, but in some

ases they merely extend an existing typespe by de ning new fun tions on existing types. typespe

typespe

Listing 3.1: CASPL Typespe s TYPESPEC PKEY ;

TYPESPEC SPKE ;

IMPORTS FIELD ;

IMPORTS PKEY ;

TYPES Pkey ;

FUNCTIONS

VARIABLES PKl , PKIl : Pkey ;

ped ( Pkey , Atom ): Atom ;

FUNCTIONS

ped ( Pkey , Field ): Field ;

keypair( Pkey , Pkey ): Boolean , COMM ; END ;

AXIOMS IF keypair( PKl , PKIl ) THEN ped( PKIl , ped( PKl , Xl ))= Xl ENDIF ; END;

Listing 1.1. shows two s. The rst de lares a new type Pkey, and a fun tion keypair on it. The fun tion returns a boolean value. The COMM in the de laration spe i es that the fun tion is ommutative. The se ond typespe imports the types de ned in PKEY using the IMPORTS de laration and de nes more fun tions on the type. The de laration ped(Pkey, Atom):Atom de lares a fun tion ped with parameters of type Pkey and Atom respe tively, and a return type Atom. Properties of the fun tions are spe i ed in the AXIOMS de nition. For instan e, the property shown here says that en rypting a term en rypted in a key, with its pair gives us the term again. typespe

15

3.1 CAPSL

3.1.2. Proto ol Spe i ations The proto ol spe i ation is the most important part of a spe i ation. Instead of listing the synta ti details, we illustrate the main features of spe i ation by the means of the adja ent example. For details the reader an refer the proje t report[14℄. CAPSL

CAPSL

CAPSL

.

Variables

PROTOCOL WooLam; VARIABLES S : Server; A, B : Client; Nb : Non e; F : Field; Kbs: Skey; DENOTES Kbs = ssk(S,B): S; Kbs = sk(B): B; ASSUMPTIONS HOLDS A: B;

Proto ol spe i ations begin with a HOLDS B: S; MESSAGES PROTOCOL de laration, whi h is followed 1. A -> B: A; 2. B -> A: Nb; by the proto ol identi er. The VARIABLES 3. A -> B: {Nb} sk(A)%F; de laration is used to de lare message elds 4. B -> S: B,{A, F%{Nb}ssk(S,A)}Kbs; and their orresponding types. Server and 5. S -> B: {Nb}Kbs; GOALS Client are types de ned in the prelude. A PRECEDES A: B | Nb; END; DENOTES de laration allows a variable to Woo-Lam Proto ol be de ned as the value of an expression. CAPSL Spe i ation This is helpful in redu ing the lutter in the messages se tion, when the proto ol uses ti kets or messages with omplex stru ture. The de laration DENOTES Kbs = ssk(S,B): S; spe i es that prin ipal S, obtains the value of the variable Kbs, by omputing the result of the fun tion ssk with its values of S and B. The DENOTES spe i ation is optional, and an be omitted for simpler proto ols. Consider the third message, where A sends a message en rypted with the key it shares with S to B. Sin e B doesn't know the en ryption key, there is no way it an interpret the ontents of the message. It is however required to forward this term to the server, and su h forwarding of uninterpreted message omponents is done using the % notation. 16

3.1 CAPSL

Intuitively, a % spe i es that the senders and the re ipient's view of the same message are dierent due to the la k of some information whi h one party does not posses. borrows the % notation from Lowe's . CAPSL

Casper

.

Assumptions

Proto ols assumptions about the knowledge and the apabilities of the of the parti ipating prin ipals are made expli it in the ASSUMPTIONS lause. The de laration HOLDS A: B spe i es, that on starting its run of the proto ol, prin ipal A knows the value of the proto ol variable B. This in ee t, makes expli it the assumption that A knows whom it wants to talk to. .

Messages

The messages ex hanged in the proto ol are spe i ed in the MESSAGES se tion. A message de laration starts with a message id, is followed by a <sender> -> re eiver:

onstru t, and ends with an expression (whi h is the message to be sent). Some notational onventions allow the expression to be written in more intuitive form. For example, message omponents an be on atenated together, by en losing them in {}, similarly en ryption of a term a with a key K an be expressed as {a}K. For instan e, the {Nb} sk(A) in the third message is a short ut for ped( sk(A), Nb) where ped is the en ryption fun tion de ned in the prelude. sk( lient shared key) is another fun tion from the prelude, mapping names to keys that prin ipals share with a key server. .

Goals

Proto ol spe i ations usually end with a spe i ation of the GOALS of the proto ol. Goals are spe i ed using PRECEDES, AGREE and SECRET keywords. Se re y assertions take the form SECRET V, spe ifying that the value of the proto ol variable V should not be dis losed to the penetrator. A pre eden e assertion of the form PRECEDES A,B | V,

17

3.2 Intermediate Language

spe i es that when prin ipal A nishes its run of the proto ol, there should exists some run of the proto ol for B's role, whi h agrees on the values of A, B and V. This notion

orresponds to Lowe's non-inje tive agreement. Agreement assertions are pre eden e

laims with no laims on the existen e of other party exe utions. AGREE A,B: V|W states that if A and B agree on V then they should agree on W too. 3.1.3. Environment Spe i ation Environment spe i ations provide run-time information that is needed by atta k onstru tors to set up the sear h for unwanted exe utions. Typi ally the information provided here in ludes the a list of agents that are expe ted to be part of the exe ution, and the a list of terms that are assumed to be known to the penetrator, Agent settings are given using AGENT de larations, whi h are a tually assignment of values to the proto ol variables. Penetrator knowledge is spe i ed using EXPOSED de laration, whi h en loses a list of terms that form the initial knowledge of the penetrator. Our des ription of here is in omplete, and was intended to give a feel of the spe i ations of proto ols. There's a lot more to the language synta ti ally as well as semanti ally, and the reader an see the proje t web page[12℄, for a detailed des ription of the language. CAPSL

3.2. Intermediate Language provides abstra tions that make it easy to translate published des riptions of proto ols to the spe i ation required by analysis me hanisms. These abstra tions, however need to be translated to the formalism that the underlying analysis requires. Like

onne tors translating spe i ations for analyzers based on multi-set rewriting systems[13℄ we use an intermediate language.

CAPSL

CAPSL

18

3.2 Intermediate Language

Our intermediate language is des ribed as an XML vo abulary, whose DTD is given Appendix-A. The language has two purposes, rstly it a ts as a onne tor to , ltering those parts of the spe i ation whi h our analysis me hanism an make use of, and se ondly it serves as the language that our GUI writes spe i ation to and reads spe i ations from. CAPSL

The message spe i ation in , is none better than the usual \Ali e-Bob" style of spe ifying proto ols. Given the fa t that the intruder an originate or ush messages, the {A -> B: A} notation doesn't make a lot of sense, sin e we are niether sure of the sender nor of the re eiver. A better approa h would be to spe ify the interfa e of ea h parti ipant i.e. what messages it sends and re eives, without asso iating these messages with any other prin ipal as is done by the intermediate language. CAPSL

As an be done using the DENOTES de laration in , we de lare all terms used in messages before hand. Proto ol roles are parameterized, as required for representing them as parameterized strands. In short, the following are the features of the intermediate language. CAPSL

Separate de nitions for terms, roles and goals. Terms de lared on e and are reused throughout. Interfa es of the parti ipants are spe i ed separately, instead of the \Ali eBob" style.

19

4. Modeling

The strand spa es formalism is des ribed. The behavior of the proto ol parti ipants, the penetrator, and the orre tness riteria are expressed in the formalism.

To reason about the orre tness of ryptographi proto ols, we need a mathemati al model to represent their exe ution. Several formalisms have been developed for this purpose, some of whi h are used spe i ally for modeling ryptographi proto ols, while others are generi enough to be used for the analysis of other systems as well. Our work is based on a formalism, whi h models proto ol exe ution as . A run of the proto ol is modeled as a olle tion of strands, alled a . Proto ol properties are expressed as predi ates on this stru ture and they are veri ed by reasoning indu tively. strands

strand spa e

4.1. Strand Spa es Events in a ryptographi proto ols are ausally dependent on other events. Strand spa es[1℄ are a graph theoreti model of this ausal dependen e. The basi building blo k of this model is a strand. Informally, a strand is a sequen e of events, that represents either a proto ol exe ution by a honest prin ipal or a sequen e of a tions 20

4.1 Strand Spa es

taken by the penetrator. Re all that, A is the set of all possible messages that an be ex hanged in a proto ol run, if we denote the sending of a term t 2 A by +t and its re eipt by t, the exe ution of a proto ol by a given parti ipant an be modeled as a string in (A). A term with its dire tion pre xed to it is alled a . Intuitively, a signed term orresponds to the event of sending or re eiving the term by a proto ol parti ipant or the intruder. A strand is string of signed terms, and a is a set  together with a tra e mapping tr :  ! (A). Figure 4.1 shows a strand spa e with four strands. signed term

strand spa e

4.1.1. Nodes is a pair (s; i) where s 2  and 0  i  jtr(s)j. Given a node n = (s; i), strand(n) = s and index(n) = i. Also, term(n) is the ith signed term in the tra e of s, and unsterm(n) is the same term without the sign. For two nodes n1 and n2 we say n1 ) n2 i n1 = (s; i) and n2 = (s; i + 1). )+ is the transitive losure of ). Intuitively, the )+ relation aptures the fa t that n1 pre edes n2 on the same strand. For two nodes n1 and n2 we say n1 ! n2 if term(n1 ) = +t and term(n2 ) = t form some term t 2 A. Intuitively, n1 ! n2 means that n2 re eives a term that is sent by n1 . A

node

We de ne  as the re exive and transitive losure of () [ !), modeling the ausal dependen y of events in the proto ol exe ution. For example, in Figure 4.1 (s4; 0)  (s1; 1) aptures the fa t that for the event orresponding to (s1; 1) to happen, the event

orresponding to (s4; 0) must happen rst. To be a orre t model of a proto ol exe ution, it is ne essary that a node be in luded only if all nodes that it ausally depends on are already in luded. This requirement is enfor ed in what we all a . bundle

21

4.1 Strand Spa es

Figure 4.1.: A Strand Spa e 4.1.2. Bundles Let be the set of nodes in a strand spa e , and let !C! and )C). A bundle is a subgraph C = h C; ()C [ !C)i of the graph h () [ !)i with the following properties N

N

N

C is nite. If n2 2 NC and term(n2 ) is negative, then there is a unique n1 su h that n1 !C n2 . If n2 2 NC and n1 ) n2 then n1 )C n2 C is a y li . Intuitively, the de nition insures that a node is in luded only if all nodes that ausally pre ede it are already in luded. The graph in Figure 4.1 onstitutes a bundle, so do the nodes and edges en losed in the re tangle labeled . The graphs ontained in the re tangles labeled 0 and 00 are not a bundles be ause they are not ausally losed. 0 is not losed under ). ( is in luded and a ) + but a is not in luded) Similarly 00 is not losed under !. ( f is in luded, but no node that sends f is). S

S

S

S

S

22

4.1 Strand Spa es

Strands in a bundle must be up wards losed, but it is not ne essary for them to be

ompletely in the bundle. We de ne the C-height of a strand in a bundle C as the index of the last node that is in luded in the bundle. If C is a bundle, the re exive and transitive losure of ()C [ !C) is a partial order denoted by C. Moreover every non empty subset of the nodes in C has C minimal members. This well-foundedness of bundles allows us to prove properties indu tively. 4.1.3. Subterms, Interms and Ideals We have de ned ryptographi primitives as operation on A , in this se tion we add more stru ture to A with the help of a relation. We also introdu e the notion of an whi h will be used to obtain bounds on the apabilities of the penetrator. subterm

ideal

We say a term t1 is a of another term t2 (t1  t2) if starting with t1 we

an onstru t t2 by repeatedly on atenating with arbitrary terms or en rypting with arbitrary keys. Formally, the subterm relation relation() is de ned indu tively as the smallest relation su h that: subterm

aa a  fg gK

if a  g

a  g h if a  g _ a  h

Note that K  fggK only if K  g. Subterms of a term are terms that an be extra ted out of it, if we knew the inverses of all the keys that are used in those terms. If none of the keys are known, the subterm relation redu es to the relation(b). In other words, a term a1 b a2 if a1 an be extra ted from a2 without having to de rypt anything. Formally, interm

a b t for t 2 T i a = t; or

23

4.1 Strand Spa es abk

for k 2 i a = k; or a b fg gk i a = fg gk ; or a b gh i a b g _ a b h _ a = gh: K

If a1 b a2 then, a1 is alled a omponent of a2 . The subterm relation with a spe i set of keys in our hands redu es to what we all an . If k K, a of A is a subset I of A su h that for all h 2 I , g 2 A and K 2 k

ideal

k-ideal

h g; g h 2 I

fhgK 2 I . The smallest k-ideal ontaining h is denoted as k [h℄, and the smallest k-ideal ontaining S  A is denoted as k [S ℄. Intuitively, k [S ℄ is the smallest set ontaining S losed under

on atenation with arbitrary terms, and en ryption with keys in k. I

I

I

Note that g  h i h 2 K[h℄. I

4.1.4. Origination We give some de nitions rst A term t at a node n, if t  term(n). A node n is an for a set of terms I if, term(n) = +t for some t 2 I and for all n0 )+ n term(n0 ) 2= I . An unsigned term on n i n is an entrypoint for the set I = ft0 : t  t0 g. An unsigned term is if it originates at only one node. o

urs

entrypoint

originates

uniquely originating

24

4.2 Modeling Proto ols

Intuitively, a term o

urs at a node if the node either sends or re eives a term whi h

ontains it. A node is an entrypoint for a set of terms i it sends a term ontained in the set, and no node before it on the strand, either sends or re eives any term in the set. An originating node for a term is the entrypoint of the set of terms ontaining the given term. Intuitively, originating nodes are those sending nodes on a strand that send a term without re eiving it from somewhere for the rst time. A term is uniquely originating i it is introdu ed into the strand spa e at a unique node. Uniquely originating terms serve as non es and session keys in proto ols. 4.1.5. The Penetrator Two things de ide the power of the penetrator - rst the keys he possesses and se ond, his ability to manipulate terms. denotes the keys that the penetrator knows initially, and these in lude publi keys of all prin ipals, the private keys of the penetrator, and all keys that the penetrator shares with other prin ipals. It also ontains keys that it might have obtained by some ryptanalysis. Kp

The se ond onstituent of the penetrator's power are the atomi operations that enable him to ush messages, generate well known messages, on atenate messages together, and apply ryptographi transformations using the keys that he knows. Atta ks result when the penetrator su

eeds in omposing these atomi a tions together to a hieve something that is undesirable. The following set of penetrator tra es give the penetrator just the same powers as mentioned in the previous hapter.

4.2. Modeling Proto ols Unlike the penetrator tra es, whi h stay the same, honest prin ipals send and re eive terms, the form of whi h, is governed by the proto ol. The messages ex hanged are 25

4.2 Modeling Proto ols

M F T C S K E C

Text Message Flushing Tee Con atenation Separation Key En ryption De ryption

h+ti where t 2 T h gi h g; +g; +gi h g; h; +ghi h gh; +g; +hi h+K i where K 2 h K; h; +fhgK i h K 1 ; fhgK ; +hi

Kp

Figure 4.2.: Penetrator Tra es however parameterized, and the a tual term sent depends on the bindings that are provided to the proto ol parameters when a parti ipant begins exe ution. The strand spa e model, allows us to represent this parameterized exe ution as a . parameterized

strand

4.2.1. Parameterized Strands A parameterized strand is a set of strands, and members of this set an be obtained by assigning values to the parameters. We illustrate the idea using the Otway-Rees proto ol, shown in Figure 6.4. The proto ol has three parti ipants - the initiator, the responder and a xed key server 1.

A

2.

B

3.

S

4.

B

! ! ! !

B : S : B : A :

M A B fNa ; M; A; B gKAS M A B fNa ; M; A; B gKAS fNb ; M; A; B gKBS M fNa K gKAS fNb K gKBS M fNa K gKAS

Figure 4.3.: Otway-Rees Proto ol

26

4.2 Modeling Proto ols

The initiator's interfa e is parameterized by the following: its own identity, A; the identity of the respondent, B ; the text omponent, M ; the identity of the server, S ; the value of the non e, Na and the value of the session key, K . Spe i instan es of the initiator's role send messages of the form shown in the gure, with the parameters repla ed by the values bound to them for that run. The values may get bound to the parameters before the role starts exe ution, or they might be learned from the messages re eived. For instan e B is bound to a value before the initiator starts its run, while K gets its value only after the last message is re eived. However, irrespe tive of the a tual values, the interfa e of the initiator is a tra e of the form - h +M A B fNa; M; A; B gKAS M fNa K gKAS i. Thus, we an use [A; B; S; Na ; M; K ℄ to represent all possible initiator strands. A spe i run of the initiator role, would have some assignments to the parameters, but the str uture of the tra e would remain the same. This notation also allows us express tra es with some ommon feature, for instan e [; ; ; Na0 ; ℄ is the set of all initiator strands, whi h use a spe i vallue of the non e Na . Init

Init

Extending the same to other parti ipants, we an express the entire strand spa e of the Otway-Rees proto ol with the following parameterized strands.

[ h+

a

Init A; B ; S; N ; M ; K M AB

f

℄= gKAS

a M AB

N

[

b

;

M

Resp A; B ; S; N ; M ; K; H; H

h

M AB H ;

[

+

M AB H

a

b

f

f

N

a K gKAS

0℄ = b

N M AB

℄= gKAS f b

gKBS

i

;

M H

0 fN b K g

KBS

;

+

0i

b

gKBS i

M H

Serv A; B ; S; N ; N ; M ; K

h

M AB

f

a M AB

N

N ; M ; A; B

gKBS + f ;

M

a

N ;K

gKAS f

N ;K

27

4.3 Modeling Corre tness

4.2.2. Freshness While parameterized strands represent the interfa e behavior su

in tly, they still don't express the freshness guarantees of non es and session keys. This is done using the notion of origination dis ussed in Se tion 4.1.4. For instan e, spe ifying that Nb in the Woo-Lam Proto ol originates uniquely at the se ond node of the responder strand, establishes it as a non e with the property that it o

urs at no sending node(ex ept the se ond node of the responder strand) in the strand spa e unless there is a re eiving node that pre edes the sending node. Moreover, the requirement that non es be generated fresh every time an be expressed as jResp[; ; ; Nb; ℄j  1. Thus, the notion of origination models the requirements of session keys and non es appropriately, and this beautiful modeling of freshness is one of the strengths of the strand spa es model.

4.3. Modeling Corre tness 4.3.1. Se re y Typi ally, proto ols laim to guarantee se re y of terms like session keys and non es. If we olle t all terms to be kept se ret in a set S , proving that the proto ol guarantees se re y is equivalent to proving that the predi ate S(; S ) holds, where

S(; S ) = 8 C 8 s 8 n (s) ^ n 2 C ) term(n) 2= k [S ℄ I

Here, k = (K n S ) 1. C is a variable ranging over bundles, s ranges over strands, and n over nodes. (s) ontains assumptions about the keys being un ompromised and assumptions about the origination of the terms being ex hanged.

28

4.3 Modeling Corre tness

We begin our explanation of how this predi ate aptures the requirements of Se tion 2.3.2, with the laim that no key in S is in . It makes little sense to talk about the se re y of terms(keys) that are already known to the penetrator. A tually,  will

ontain assumptions about keys in S not being in . In other words, we begin with the penetrator not knowing any key in S . Kp

Kp

For the penetrator to learn any value in S , some node must send a term that is en rypted by keys whose inverse the penetrator might know. All we are sure of, is that the penetrator does not know any key in S ((s) ensures that) but we do not know what other keys are known to it. Any node sending terms en rypted with the inverse of keys (K n S ) an risk the se re y of terms in S . Re all that k [S ℄ is the set of all terms that

an be formed by on atenating terms in S with arbitrary terms and en rypting with keys in k. Our hoi e of k is pre isely those keys whose inverse the penetrator might posses. So proving that no node ever emits terms ontained in k [S ℄ is equivalent to proving that the proto ol never sends its se rets unprote ted. I

I

4.3.2. Authenti ation Like we did for the se re y guarantee, we will translate the requirements of authenti ation mentioned in Se tion 2.3.1 to our model. Authenti ation guarantees an be expressed using the following predi ate A(i; j; ;

) = 8C 8s 9s0 C-height(s) = i ^ (s) ) C-height(s0) = j ^ (s; s0)

Intuitively, the impli ation laims about the presen e of ertain strands if ertain other strands are already in the bundle. Translated to normal language, this is the guarantee of ertain events happening given that some events happened, whi h is pre isely what authenti ation is all about.

29

4.3 Modeling Corre tness (s) spe i es properties that the strand s should posses.

As in the se re y requirement, it also ontains assumptions about terms being uniquely originating, and keys being un ompromised. The on lusion (s; s0) spe i es properties that the strand s0 should posses(s0 is always assumed to be a regular strand). It will also in lude the agreement requirements, i.e. what parameters of s and s0 should have the same values. This on ludes our dis ussion of how ryptographi proto ols, penetrator and the orre tness requirements are modeled in the strand spa es formalism. While we have stated the

orre tness requirements in the last se tion, we haven't des ribed of the way the proofs of these impli ations must be attempted. This forms the subje t of the next hapter.

30

5. Proving Proto ol Corre tness

A general strategy for proving proto ol properties is des ribed. The use of the partial orders

 and  is illustrate.

Se re y

and authenti ation guarantees of OtwayRees Proto ol are proved.

A bundle models one possible exe ution of a proto ol. When we prove a property for all bundles, we establish it for all exe utions of the proto ol. We identi ed properties that we are interested in in the last hapter. In this hapter we dis uss how proofs of properties an be onstru ted in the strand spa es formalism. Proofs in the strand spa es framework, exploit two partial orderings, namely the subterm relation  between terms and the  relation between nodes. Indu tive arguments over the  relation are based on the minimal nodes, while those over  relation are based on ideals. Before des ribing strategies to prove proto ol properties we provide insights on how proofs an use these partial orders.

31

5.1 Using 

5.1. Using



Suppose is a predi ate on nodes, and suppose we want to prove the following statement over all bundles C 8C 8n : n 2 C ) : In words, this is the same as saying that nodes with ertain features(those required by ) do not belong to any bundle, whi h in turn is equivalent to saying that that

ertain events never o

ur in proto ol runs. The proof will use the well-foundedness of bundles. Re all that, every non empty subset of the nodes in a bundle must have minimal nodes. If we assume the set of nodes satisfying as non-empty, we must have -minimal nodes in the set. If we prove that no node an satisfy and the requirements of a minimal node simultaneously, we prove that S is empty. In step iv. of the general i. ii. iii. iv. v.

Let S = fn : node j (n) holdsg. The goal is to prove that S is empty, assume that it isn't. If S is non-empty, is must have a -minimal, say min. Consider all possibilities of min. If no node an be min, we have a ontradi tion, and S is empty. Figure 5.1.: A Generi Proof Strategy

strategy, we are required to onsider both regular and penetrator nodes. Considering all these nodes might seem demanding at rst, but it a tually isn't. Given that we have a xed penetrator model and that the regular strands hardly have more than four nodes, we are never required to onsider a very large number of nodes. Moreover, we have a few results that redu e the number of andidate nodes even further. If has the additional property -

8m; m0 (unsterm(m) = unsterm(m0 )) ) ( (m) i (m0))

32

5.2 Using 

Then all -minimal nodes of S are positive nodes, whi h means we an ignore all negative nodes in step iv. This proposition an be easily proved using the fa t that for every negative node in the bundle, there is a positive node whi h pre edes it. In addition, most that we onsider satisfy this property.

5.2. Using



We reason about the nodes using the  relation, in a similar way we reason about terms, using the  relation. The notion of an ideal orresponds to the notion of a minimal node in the ase of the  relation. Ideals, allow us to obtain bounds on the apabilities of the intruder. Re all that a k-ideal of a set S , denoted by k [S ℄ is the smallest set ontaining S , that is losed under on atenation with arbitrary terms and en ryption with keys in k. Depending on our hoi e of k, and ideal an represent the set of terms that a penetrator

an reate or interpret. We would like to reason about terms that the penetrator an

reate be ause authenti ation guarantees require that ertain terms originate on regular nodes only. On the ontrary, we would like to reason about the terms that the penetrator

an interpret for providing se re y guarantees. The notion of ideals is useful in both these situations. I

The predi ate of the generi proof strategy usually involves ideals, and it is using the properties of ideals, we rule out most andidate nodes onsidered in step iv. In addition, ideals provide us generi bounds on the apabilities of the intruder, allowing us to ompletely skip penetrator nodes if the ideal stru ture is enough for the bound to apply. We mention one of su h bounds, without a proof. If K = S [ k 1 and S \

Kp

is empty, then the entry points of k [S ℄ (if any) are regular. I

33

5.3 Proving Se re y

5.3. Proving Se re y Consider the Otway-Rees proto ol, des ribed in Figure 6.4. The strands of the proto ol parti ipants are given in x4.2.1. Suppose we wish to prove that the proto ol preserves the se re y of the session key K ex hanged and also does not dis lose the shared keys KAB and KBS . We restate the se re y requirement of x4.3.1 -

S(; S ) = 8 C 8 s 8 n (s) ^ n 2 C ) term(n) 2= k [S ℄ I

The set of se rets S in our ase is is fK; KBS ; KAS g.  is expe ted to ontain assumptions about the origination of terms, penetrator knowledge and the stru ture of the strands. We in lude the following assumptions in  is uniquely originating. K 2= . K 2= fKAS : A 2 Ng K=K 1 K

Kp

The generi proof strategy with (n) = term(n) 2 k [S ℄ an be used to prove the property. We give a very brief proof outline next. I

Firstly, note that the onditions required by the bound mentioned in the previous se tion are satis ed. This rules out any penetrator nodes from being minimal. All we need to

he k now is if any of the regular nodes, are minimal in the set. The stru ture of the strands and the assumptions in  do not let that happen too. This proves that the set is empty, and thus the property holds.

5.4. Proving Authenti ation If a prin ipal sends a term en rypted by some other prin ipals key and later re eives it ba k in some ryptographi ally altered form, and if we know that the keys required 34

5.4 Proving Authenti ation

for su h a transformation are not a

essible to the intruder, we an be sure that some regular prin ipal must have operated upon it. An inferen e of this kind is alled an [2℄. We use these to prove authenti ation guarantees.

authenti ation test

5.4.1. Some Notation Re all that a1 is a omponent of a2 if a1 b a2. A term is at a node n, if it is a

omponent of term(n) and not a omponent of term(n0 ) if n0 )+ n. New omponents result from some ryptographi transformations. An edge n1 )+ n2 is a , for a 2 A if n1 is positive, n2 is negative, a  n1 and there is a new omponent t2 of n2 su h that a  t2 . If n1 is negative and n2 is positive, the edge is alled a . new

transformed

edge

transforming edge

A term t = fhgK is a for a in n, if a  t and t is a omponent of n and t is not a proper subterm of any regular node in the strand spa e. test omponent

The edge n0 )+ n1 is a transformed edge for a.

test

for a, if a uniquely originates at n0, and n0 )+ n1 is a

The edge n0 )+ n1 is an for a in t = fhgK if it is a test for a in whi h, K is ina

essible to the intruder; a does not o

ur in any omponent of n0 other than t and t is a test omponent for a in n0 . outgoing test

The edge n0 )+ n1 is an for a in t = fhgK if it is a test for a in whi h, K is ina

essible to the intruder; and t is a test omponent for a in n1. in oming test

An outgoing test, formally expresses the fa t that a prin ipal sends a freshly generated message en rypted by a key that is not known to the intruder and gets it ba k in an altered form. An outgoing test hallenges the other prin ipal to de rypt the test

omponent. On the other hand, for an in oming test, the hallenge is to en rypt a term, whi h is generated fresh and sent by the prin ipal at n0. 35

5.4 Proving Authenti ation

Let be the set of keys in luding those in and those that are learned during proto ol exe utions. If we know what keys belong to , then we an reason about the possible bundle stru tures whi h an ontain these tests. This brings us to the main results of this se tion, the authenti ation tests. P

Kp

P

5.4.2. Authenti ation Tests Having de ned the required notation, we des ribe the main theorems whi h will be used to prove authenti ation guarantees of proto ols. .

Outgoing Authenti ation Test

Let C be a bundle with n0 2 C, and let n0 )+ n1 be an outgoing test for a in t, then There exist regular nodes m; m0 2 C su h that t is a omponent of m and m )+ m0 is a transforming edge for a. Suppose in addition, that a o

urs only in omponent t1 = fh1 gK1 of m0 , that t0 is not a proper subterm of any regular omponent, and that K1 1 is not a

essible to the intruder, then there is a negative regular node n00 with t1 as omponent.

Figure 5.2.: The Outgoing Authenti ation Test

36

5.4 Proving Authenti ation

The intuitive meaning of this theorem is expressed in Figure 5.2. In the gure nodes marked with empty ir les are n and n0 and those marked by lled ir les are m and m0. The theorem says that if a bundle has nodes n and n0 whi h satisfy the onditions then it will also have nodes m, m0 and n00 . The next theorem, uses in oming tests to oer a similar guarantee. .

In oming Authenti ation Test

Let C be a bundle, with n0 2 C, and let n )+ n0 be an in oming test for a in t0 . Then these exists regular nodes m; m0 2 C su h that t0 is a omponent of m0 and m )+ m0 is a transforming edge for a. As shown in Figure 5.3, this test allows us to infer existen e of a regular transforming edge in a proto ol where a non e is sent in plain-text, and is expe ted to be replied en rypted.

Figure 5.3.: The In oming Authenti ation Test

.

Unsoli ited Authenti ation Test

In proto ols whi h involve more than two parti ipants, like those with key servers, a weaker test is often useful. This test uses the fa t that re eption of a term en rypted by some key whi h the intruder doesn't know, provides some hints about the node whi h

37

5.5 Using Tests

originated the term. A negative node n is an for t = fhgK if t is a omponent for any a in n and K 2= P We an use an unsoli ited test to obtain the following theorem, also alled the unsoli ited authenti ation test. unsoli ited test

Let C be a bundle, with n 2 C, and let n be an unsoli ited test for t = fhgK . Then there exists a positive regular node m 2 C su h that t is a omponent of m.

5.5. Using Tests The authenti ation tests, have been proved in [2℄. In this se tion we will use them to prove them to prove authenti ation guarantees of the form mentioned in x2.3.1. A(i; j; ;

) = 8C 8s 9s0 C-height(s) = i ^ (s) ) C-height(s0) = j ^ (s; s0)

One authenti ation requirement of the Otway-Rees proto ol an be obtained by the following assignments - (s) = s 2 Serv[A; B; S; Na; Nb; M; ℄, i=1, (s; s0) = s0 2 Init[A; B; S; Na ; M; ℄, j = 1. This guarantee in plain words says that if the server has re eived a request for a session key, then the request indeed omes from an honest parti ipant with the same bindings. This an be proved, by verifying that the term fNa MAB gKAS is an unsoli ited test and thus by the unsoli ited authenti ation test theorem, there has to exist a regular node whi h sends it. Considering all the positive regular nodes we nd that the only node that is apable of sending it is the rst node on the initiator strand. Thus the strand with the same bindings exist. Another authenti ation requirement of the Otway-Rees proto ol an be obtained by these assigning these values to the general property - (s) = s 2 Init[A; B; Na ; ; M; K ℄, i=2, (s; s0 ) = s0 2 Serv [A; B; S; Na ; ; M; K ℄, j = 2. This an be read as - if the initiator ends its proto ol exe ution, the keys that it gets originates on a server strand. 38

5.5 Using Tests

This an be proved by verifying that the the rst two nodes on the initiator strand

onstitute an outgoing test for Na in fNa MAB gKAS . The outgoing test theorem ensures that there will a regular transforming edge for Na . Again, onsidering the nodes will show that this edge an lie on no strand other than s 2 Serv[A; B; S; Na; ; M; K ℄. This ends our dis ussion of how proofs of properties an be obtained. As is evident from most of the proofs we outlined, a lot of arguments are repeated again and again. Also, a lot of the arguments are independent of the a tual proto ol under onsideration. This allows us to develop a general proof me hanism in PVS. The next hapter des ribes the details of the same.

39

6. PVS Theories

We des ribe a translation s heme from proto ol des riptions to PVS theories. We also illustrate our PVS formalization of the strand spa es proof me hanism

The overall design of our translation s heme is shown in Figure 6.1. spe i ations are rst translated to an intermediate language representation whi h are then onverted to PVS theories required from proving properties of proto ols. Our PVS formalization CAPSL

Figure 6.1.: Automated Generation of Strand Spa e Theories separates the proto ol dependent arguments used in proofs from the independent ones. The proto ol independent arguments reside in theories that are in luded along with the 40

6.1 Proto ol Independent Theories

ore theories that PVS provides, allowing us to reuse these theories over proto ols. Proto ol spe i arguments are ontained in theories that are are generated automati ally from the proto ol des ription.

6.1. Proto ol Independent Theories The message algebra, the penetrator model, and the basi notions of strand spa es do not depend on the proto ol under onsideration. These are formalized as separate theories whi h proto ol spe i theories an use. We on entrate on proofs of se re y properties in this hapter, and thus we des ribe only those portions of the theories that we will need later in the example proofs. The theories, in their entirety are expressive enough to handle any proof des ribed in or based on the te hniques in [1℄. 6.1.1. Messages The set of all possible messages ex hanged during a proto ol run in lude messages of primitive types like text or keys and also ompound types like en rypted or on atenated messages. In general, a message is an instan e of a type rypt_term, whi h is de ned as a PVS data-type. Messages of more spe ialized types an be reated by using their

orresponding onstru tors.

rypt_term : DATATYPE WITH SUBTYPES key , text , name , en rypt, on at BEGIN text ( id : nat ): text ?: text key ( id : nat ): key ?: key name ( id : nat ): name ?: name en r ( plain : rypt_term , en key : key ): en rypt ?: en rypt join ( a : rypt_term , b : rypt_term ): on at ?: on at END rypt_term

41

6.1 Proto ol Independent Theories

Equality of terms is de ned indu tively using the == operator. Note that the de nition takes into onsideration the freeness assumptions des ribed in x2.1. ==(x , y : rypt_term ): INDUCTIVE boolean = CASES y OF text ( tid ): text ?( x ) AND id (x ) = tid , key ( tid ): key ?( x ) AND id (x ) = tid, name ( tid ): name ?( x ) AND id (x ) = tid , en r ( en text, en key ): en rypt?( x ) AND ( en text == plain (x )) AND ( en key == en key ( x )), join ( first , se ond ):

on at ?( x ) AND ( first == a( x )) AND ( se ond == b (x )) ENDCASES

6.1.2. Penetrator Capabilities The keys that the penetrator knows are modeled as a predi ate on the set of keys penetrated: pred[key℄. The penetrator's apability to learn terms given the set of keys he knows, is modeled using the notion of ideals des ribed in x4.1.3. Re all that a -ideal of a term is the set of terms that an be onstru ted by on atenating terms already in the set with arbitrary terms or en rypting them with keys in . Alternatively, -ideal of a term t - k [t℄ is the set of terms from whi h t an be obtained if inverses of keys in are known. The notion of an ideal, and the set penetrated allow us to su

in tly express the set of terms that ould potentially leak some se ret. We use the set se re y_ideal for this purpose. k

k

k

I

k

se re y_ideal( S : set [ rypt_term ℄, x : rypt_term ): INDUCTIVE boolean = S (x ) OR ( EXISTS ( y , z : rypt_term ): x == join ( y , z ) AND ( se re y_ideal( S , y ) OR se re y_ideal(S , z ))) OR ( EXISTS ( y : rypt_term , k : key ): x == en r (y , k ) AND se re y_ideal( S , y ) AND penetrated( inv (k )))

42

6.1 Proto ol Independent Theories

Intuitively, when a prin ipal sends a term term belonging to the se re y_ideal orresponding to a set of se rets S , it sends some element of S without prote ting it with proper keys. Thus, proving that a proto ol preserves se re y of a set of terms is equivalent to proving that no proto ol prin ipal ever sends a term that belongs to the se re y_ideal. Before we des ribe how su h a proof an be attempted, re all that, the  relation models the ausal dependen ies of events in a proto ol and that a bundle is a ausally

omplete sub-graph of the strand spa e of a proto ol. Intuitively, a bundle models one possible exe ution of a proto ol so proving a property for all bundles establishes it for all exe utions of the proto ol. Also re all that a bundle is well-founded i.e. all possible subset of nodes in a bundle posses -minimal nodes, whi h are nodes that are not

ausally dependent on other nodes of the subset. These minimal nodes form the base

ase of the indu tive arguments that we use in proofs 6.1.3. Proving Se re y Thus we have redu ed the problem of proving that a proto ol preserves se re y of a given set of terms to that of proving that the set of nodes, whi h send terms in the se re y_ideal orresponding to the set, is empty. We begin by assuming that the set is non-empty and thus, by the well-foundedness of bundles, must have -minimal nodes. Next using indu tion on the stru ture of the strands of the proto ol, if we an show that no node an satisfy the onditions required to be in the set and those required to be a minimal node, simultaneously, we rea h a ontradi tion, thus proving that S is empty. We will need to onsider both regular and penetrator nodes to apply the strategy des ribed above. While regular nodes depend on the proto ol we analyze, the penetrator nodes are xed and an be in luded in the proto ol-independent part of the overall theory. Moreover, as mentioned in x5.1, using results from [1℄ we an redu e the number

43

6.1 Proto ol Independent Theories

of nodes to be onsidered even further. (Note that these results an be proved in PVS using the axioms of our theories).In parti ular we use the result - If m is minimal in fm : node j term(m) 2 I g then m is an entrypoint for I. Re all that a node is an entrypoint for a set of terms I if it sends a term in I while no node that pre edes it on its strand sends or re eives any term in I . So, given a xed set of penetrator strands, it is possible for us to sele tively hoose only those nodes whi h an possibly be entrypoints. We de ne a formulae no_penetrator_entrypoint whi h returns true i there is no penetrator node apable of being the entrypoint of give set of terms. no_penetrator_entrypoint (I : set [ rypt_term ℄): boolean = NOT (( EXISTS ( t : text ): I (t )) OR ( EXISTS ( k : key ): penetrated(k ) AND I (k )) OR ( EXISTS ( j : on at ): (( NOT I (a( j ))) AND ( NOT I(b (j ))) AND I(j )) OR ( NOT I (j )) AND I (a( j ))) OR ( EXISTS ( e : en rypt): ( NOT I ( plain (e ))) AND ( NOT I( en key ( e ))) AND I(e ) OR (( NOT I( e )) AND ( NOT I ( inv ( en key (e )))) AND penetrated( inv( en key ( e ))) AND ( I( plain (e ))))))

Note that we onsider only positive nodes on the penetrator strands(sin e negative nodes

an not be entry-points), and every time we in lude the terms orresponding to a node in the set, we he k whether terms of nodes pre eding it on the same strand do not belong to the set. A similar no_regular_entrypoint formula is expe ted to be generated by the translation me hanism from the proto ol spe i ation. Thus, if we denote the set of se rets by Se ret, then the set of terms that ould potentially leak the se rets would be LeakingTerms and proving that no node leaks se rets is equivalent to proving NoLeaks. Se ret : set [ rypt_term ℄ = .. % filled by translator % LeakingTerms : set [ rypt_term ℄ = LAMBDA ( t : rypt_term ): se re y_ideal( Se ret , t) NoLeaks: THEOREM no_penetrator_entrypoint ( LeakingTerms) AND no_regular_entrypoint ( LeakingTerms)

44

6.2 The Translation

Thus, all we need now is the formula no_regular_entrypoint, whi h is generated from the proto ol spe i ation.

6.2. The Translation We illustrate the translation using a simple proto ol shown below, that was used by Nessett to demonstrate a aw in the BAN logi analysis. The proto ol laims to distribute a \good" session key between parties A and B , and learly does not a hieve this sin e en ryption with the private key of A does not preserve the se re y of the session key. We will use this simple proto ol to illustrate our translation pro edure and also show how a proof attempt of this proto ol pin-points the aw in its stru ture. 1.

A

2.

B

! !

B : A :

f a g KA 1 f b gK N ;K

N

The proto ol an be spe i ed in or using a GUI, and the spe i ation is then translated to an intermediate language des ription, whi h is de ned as an XML vo abulary. A part of the spe i ation for the urrent proto ol, expressing the stru ture of messages that the proto ol uses, is shown below. CAPSL

< proto ol label =' nesset '> < terms > < name label =' A '/> < name label =' B '/> < text label =' Na '/> < text label =' Nb '/> < key label =' Ka ' type =' private ' prin ipals =' A '/> < key label =' K '/> < en rypt label =' one ' terms =' Na K ' key =' Ka '/> < en rypt label =' two ' terms =' Nb ' key = ' K '/> < roles > ... < goals > ...

45

6.2 The Translation

The message stru ture an be onverted to the PVS representation using the following strategy. if tag is ( key or text or name ) print ' label :< tag >=< tag >(< unique_id >)' if tag is en rypt print ' label : en rypt= en r (< join ( terms )>, key )'

In the pseudo- ode we use tag to denote the urrent element,  to a

ess values of attributes of the urrent element and we en lose names in < > to denote that they must be treated as a fun tions whose return values must be inserted. Also, unique_id is a fun tion returning a identi er that hasn't been used before and join is a fun tion generating the PVS expression for a term whi h is on atenation of the terms in the argument string. For example, a all join("A B C") returns join(A,join(B,C)), whi h is the rypt_term orresponding to the on atenation of the terms in the string. We also use a onstru t for-every to apply a set of statements for every hild element with the spe i ed name. For instan e for-every role {print label} would print the value of the label attribute of all role hildren of the urrent node. The remaining spe i ation des ribes the proto ol roles using the role element. < proto ol> < terms > ... < roles > < role > label =' Init ' self =' A ' parameters =' A B Na Nb K' knows =' B ' originates =' Na '> < send terms =' one '/> < re eive terms =' two '/> < role label =' Resp ' self =' B ' parameters =' A B Na Nb K' originates =' Nb '> < re eive terms =' one '/> < send terms =' two '/> < goals >< se ret terms =' K '/>

46

6.2 The Translation

The role element has many attributes whi h are not required for proving se re y properties whi h are our urrent on ern. All that we need to prove whether or not a proto ol preserves its se rets is the fun tion no_regular_entrypoint whi h is true only if no regular node an be an entrypoint of the given set of terms. Su h a fun tion an be

onstru ted using the terms that a parti ipant sends and re eives. The following translation results in an expression whi h is true if some regular node an be an entrypoint of a set of terms I. for- every role for - every send print ' I( terms )' for - every pre eding- sibling print '( NOT I ( terms ))' endfor endfor print ' OR ' endfor

The assumptions about the penetrator knowledge are translated next using the following strategy. All keys that the proto ol laims to be keep se ret are also assumed to be un ompromised. print ' phi: AXIOM ' for - every key if type = ( private OR session OR shared ) print ' NOT penetrated( label )' if type =' publi ' print ' NOT penetrated( inv( label ))' end - for

Lastly, the set Se ret mentioned in the previous se tion is generated using the following translation print ' Se ret : set [ rypt_term ℄= LAMBDA ( t: rypt_term )' for - every token in se retterms print ' t == < token >' endfor

The omplete PVS le generated using the translation mentioned in this se tion is given next. The theory message_algebra whi h this theory imports in ludes the proto ol 47

6.3 Proof in PVS

independent axioms used by the proofs. nesset : THEORY BEGIN IMPORTING message_algebra A : name = name (1) B : name = name (2) Na : text = text (3) Nb : text = text (4) K : key = key (1) Ka : key = key (2) one : en rypt = en r ( join ( Na , K ), Ka ) two : en rypt = en r ( Nb , K ) Se ret : set[ rypt_term ℄ = LAMBDA ( t : rypt_term ): ( t == K) phi : AXIOM NOT ( penetrated( inv ( Ka )) OR penetrated(K )) LeakingTerms : set [ rypt_term ℄ = LAMBDA ( t : rypt_term ): se re y_ideal( Se ret , t) no_regular_entrypoint ( I : set [ rypt_term ℄): boolean = NOT (( I( one )) OR ( I( two ) AND ( NOT I( one )))) empty_set(s : set [ rypt_term ℄): boolean = no_regular_entrypoint (s ) AND no_penetrator_entrypoint ( s) se ret1 : THEOREM empty_set( LeakingTerms) END nesset

6.3. Proof in PVS Having generated the required theories, we an attempt the proof of the laim that the proto ol guarantees se re y of the session key. As it turns out, the proof gets stu k at the following sequent [-1℄ se re y_ideal( Se ret , join ( text (3), key (1))) [-2℄ penetrated( inv ( key (2))) |------Rule ?

Here, key(2) is the key used to en rypt the session key. Note that the formula [-1℄ holds, sin e key(1) orresponds to the session key whi h is in the Se ret set. So the su

ess of the proof attempt boils down to whether or not penetrated(inv(key(2)) holds, whi h does not. In other words, the proof attempts pin points the aw in the stru ture of the proto ol.

48

6.4 Otway-Rees Example

6.4. Otway-Rees Example The intermediate language representation of the Otway-Rees proto ol and its generated PVS theory is is given in Appendix-B. Note that both the intermediate representation and the PVS theory leanly model the fa t that the responder forwards omponents whi h it an not interpret, for the la k of the required key. A proof attempt provides useful insights on what properties of the uninterpreted terms the responder must be

apable of he king for the proto ol to guarantee se re y.

49

7. Con lusion

The PVS formalization of the strand spa es proof me hanism and the generi translation me hanism are the two ontributions of this report. The des ription of our PVS theories given here is in omplete. The theories an be used to prove mu h more than just the se re y guarantees. For instan e proofs of lemmas and propositions in [1℄ have been su

essfully attempted. Also, the formulas no_regular_entrypoint and no_penetrator_entrypoint that we generate from the proto ol spe i ation are general, and they work with sets of terms, other than ideals. In other words, proof of any property that an be expressed as a predi ate on the terms that nodes send or re eive

an be attempted using our theories. Proofs in the strand spa e me hanism are more intuitive than proofs whi h use other me hanisms[18℄. Moreover, using already proved results[2℄ we an extend our theories to attempt proofs of properties like authenti ation, whi h haven't been proved in an automated setting. We have su

essfully proved authenti ation properties of a few proto ols, and will soon generalize our theories for the same.

50

Bibliography

[1℄

J. Thayer, J. Herzog, J. Guttman. Strand Spa es: Proving Se urity Proto ols Corre t. Journal of Computer Se urity, Volume 7, Issue 2-3:191{230, 1999.

[2℄

Joshua D. Guttman, F. Javier Thayer Fabrega. Authenti ation tests and the Stru ture of Bundles. Journal of Theoreti al Computer S ien e, 2001.

[3℄

D. X. Song, S. Berezin, A Perrig. Athena:

A Novel Approa h to Effi ient

Automati Se urity Proto ol Analysis.

Volume 9, Issue 1-2:47{74, 2001. [4℄

A. Perrig, D. Song A

Journal of Computer Se urity,

First Step Towards the Automati Generation

of Se urity Proto ols

Se urity (NDSS) 2000.

In Symposium on Network and Distributed Systems

[5℄

Joshua D. Guttman Proto ol Design via the Authenti ation Appears in Computer Se urity Foundations Workshop, 2002

[6℄

D. Dolev and A. Yao On the se urity of publi -key Transa tions on Information Theory, 2(29), 1983

51

proto ols

Tests

IEEE

BIBLIOGRAPHY

[7℄

Catherine Meadows The NRL Proto ol Analyzer: nal of Logi Programming, Volume 26(2), 113{131,1996

[8℄

Stefanos Gritzalis, Diomidis Spinellis, Panagiotis Georgiadis. Se urity Proto-

An Overview

Jour-

ols over Open Networks and Distributed Systems: Formal Methods for their Analysis, Design, and Verifi ation.

ni ations, 22(8):695{707, 1999.

Computer Commu-

[9℄

J. Clark and J. Ja ob A Survey of Authenti ation Proto ol Literature Available via http://www. s.york.a .uk/ja /papers/drareview.ps.gz

[10℄

Catherine Meadows

Formal Verifi ation of Cryptographi Proto-

ASIACRYPT: International Conferen e on the Theory and Appli ation of Cryptology

ols: A Survey

[11℄

Levente Buttyan Formal methods in the design of ryptographi proto ols (state of the art)

[9℄

G. Denker, J. Millen

CAPSL and CIL Language Design: A Common

Authenti ation Proto ol Spe ifi ation Language and Its Interme-

CSL Report SRI-CSL-9902, Computer S ien e Laboratory, International, Menlo Park CA 94025, 1999.

diate Language

[11℄

[12℄ [13℄

Martin Abadi Se urity Proto ols and Spe ifi ations Foundations of Software S ien e and Computation Stru tures: Se ond International Conferen e, FOSSACS '99. Vol-1578:1{13, 1999. CAPSL - Webpage

http://www. sl.sri. om/users/millen/ apsl/

G. Denker and J. Millen intermediate language , FLoC Workshop on Formal Methods and Se urity Proto ols, 1999 CAPSL

52

BIBLIOGRAPHY

[14℄

G. Denker and J. Millen, Integrated Proto ol Environment , DARPA Information Survivability Conferen e (DISCEX 2000).207{221, 2000. IEEE Computer So iety

[15℄

M. Burrows and M. Abadi and R. Needham A Logi of ACM Transa tions on Computer Systems, 8(1)18{36,1990

[16℄

M. Abadi and A. Gordon A al ulus for ryptographi proto ols: Spi Cal ulus Digital Systems Resear h Center, SRC-149, 1998

[17℄

L. Paulson The indu tive approa h to verifying ryptographi proto ols Journal of Computer Se urity, 6(1)85{128, 1998

[18℄

H. Rue and J. Millen Lo al Se re y for State-Based Models Formal Methods in Computer Se urity, CAV workshop. Chi ago, July 2000.

[19℄

Steve S hneider Verifying Authenti ation Proto ols with CSP PCSFW: Pro eedings of The 10th Computer Se urity Foundations Workshop, IEEE Computer So iety Press, 1997

[24℄

Gawin Lowe A Hierar hy of Authenti ation Spe ifi ations PCSFW: Pro eedings of The 10th Computer Se urity Foundations Workshop, IEEE Computer So iety Press, 1997

[25℄

Owre, S. and Shankar, N. and Rushby, J.M. and Stringer-Calvert, D.W.J. PVS Language Referen e,Version 2.4 CSL,SRI. De ember 2001

[26℄

Owre, S. and Shankar, N. and Rushby, J.M. and Stringer-Calvert, D.W.J. PVS Prover Guide, Version 2.4 CSL,SRI. November 2001

[27℄

Owre, S. and Shankar, N. and Rushby, J.M. and Stringer-Calvert, D.W.J. PVS System Guide,Version 2.4 CSL,SRI. De ember 2001

CAPSL

Authenti ation

the

53

A. Intermediate Language DTD

54

B. Otway Rees Example B.1. Intermediate Language Spe i ation < proto ol label =' otwayrees '> < terms > < name label =' A '/> < name label =' B '/> < name label =' S '/> < text label =' M '/> < text label =' Na '/> < text label =' Nb '/> < key label =' K '/> < key label =' Kas ' type =' shared ' prin ipals =' A S '/> < key label =' Kbs ' type =' shared ' prin ipals =' B S '/> < term label =' H ' interpret=' one '/> < term label =' H1 ' interpret =' four '/> < en rypt label =' one ' terms =' Na M A B ' key =' Kas '/> < en rypt label =' two ' terms =' Nb M A B ' key =' Kbs '/> < en rypt label =' three ' terms =' Na K ' key =' Kas '/> < en rypt label =' four ' terms =' Nb K ' key =' Kbs '/> < roles > < role label =' Init ' self =' A' parameters =' A B S M Na K ' knows =' S B ' originates =' Na '> < send terms =' M A B one '/> < re eive terms =' M three '/> < role label =' Resp ' self =' B' parameters =' A B S M Nb K H H1 ' knows =' S ' originates =' Nb '> < re eive terms =' M A B H '/> < send terms =' M A B H two '/> < re eive terms =' M H1 four '/> < send terms =' M H1 '/> < role label =' Serv ' self =' S' parameters =' A B S M Na Nb K ' originates =' K '> < re eive terms =' M A B one two '/> < send terms =' M three four '/> < goals > < se ret terms =' K '/>

55

B.1 Intermediate Language Spe i ation

56

B.2 PVS Theory

B.2. PVS Theory otway : THEORY BEGIN IMPORTING message_algebra A : name = name (1) B : name = name (2) S : name = name (3) M : text = text (4) Na : text = text (5) Nb : text = text (6) K : key = key (1) Kas : key = key (2) Kbs : key = key (3) H : rypt_term H1 : rypt_term four : en rypt = en r ( join ( Nb , K ), Kbs) one : en rypt = en r ( join ( Na , join (M , join ( A , B ))), Kas) three : en rypt = en r ( join ( Na , K ), Kas ) two : en rypt = en r ( join ( Nb , join (M , join ( A , B ))), Kbs) Se ret : set[ rypt_term ℄ = LAMBDA ( t : rypt_term ): t == K phi : AXIOM NOT ( penetrated(K ) OR penetrated( Kbs ) OR penetrated( Kas )) inverses : AXIOM inv (K )= K AND inv ( Kas )= Kas AND inv ( Kbs )= Kbs LeakingTerms : set [ rypt_term ℄ = LAMBDA ( t : rypt_term ): se re y_ideal( Se ret , t) no_regular_entrypoint ( I : set [ rypt_term ℄): boolean = NOT (( I( join (M , join ( three , four ))) AND ( NOT I( join (M , join (A , join ( B , join ( one , two ))))))) OR ( I( join ( M , join (A , join ( B , one ))))) OR (I( join (M , join (A , join (B , join (H , two ))))) AND ( NOT I( join (M , join (A , join ( B , H )))))) OR (I( join (M , H1 )) AND ( NOT I( join (M , join ( A , join (B , H ))))) AND ( NOT I ( join (M , join (A , join (B , join ( H , two )))))) AND ( NOT I( join ( M , join ( H1 , four )))))) empty_set(s : set [ rypt_term ℄): boolean = no_regular_entrypoint (s ) AND no_penetrator_entrypoint ( s) se ret3 : THEOREM empty_set( LeakingTerms) END otway

57