ñòð. 5 |

of a communication protocol C, then the following holds:

Every L-computed answer is L-correct answer for logic program FC and query ?-

Messages(X,Y) (soundness).

Every L-correct answer is L-computed answer for logic program FC and query ?-

Messages(X,Y) (completeness).

Proof: Standard Logic Programming (LP) theory [28].

Presence of an attack can be expressed as follows (the adversary i knows the message p):

FC |= Messages(i,p).

Definition 3 (L-Safety): Let FC be a logic program that interprets evaluation of a

communication protocol C. Let p,q the secret messages that the participants a,b of the

protocol want to exchange. Let kab be a new session key between a and b.Let i be the

adversary. Then the protocol C represented by logic program FC is L-computionaly safe, if

there is no computed answer for logic program FC and queries:

a) ?-Messages(i,kab)

b) ?-Messages(i,p)

c) ?-Messages(i,q)

and if there exists computed answer for logic program FC and queries:

a) ?-Messages(a,q)

b) ?-Messages(b,p).

3.2.2 Introduction of function Depth_ into classical LP

Now we have whole environment but there are some weaknesses. If we will have

protocol-independent rules in form as in Fig. 1 by reasoning it will lead to infinite cycle,

especially rules [Iâ€™.2], [Iâ€™.3] and [Iâ€™.7]. It is caused by every new word it is possible to use one

of these rules and we get new word and on this new word we can again use one of these rules

13

PDF created with FinePrint pdfFactory trial version http://www.fineprint.com

and so on.... To prevent this infinite cycle we use for description of every protocol constant

MAX (positive integer) that states the maximal relevant depth of used encryption, hash and

handshake in protocol messages plus one. The purpose of that constant is to reduce the

infinite search space. It means that at the beginning we donâ€™t have only set F but also the

constant MAX, and this constant changes the protocol-independent rules into new form:

[I.2] Messages(X, e(T, L)):-Messages(X, T)&Keys(X, L)&DepthE(T)<Max

[I.3] Messages(X, f(T)):-Messages(X, T) &DepthF(T)<Max

[I.7] Messages(X, h(T, L)):-Messages(X, T)&Keys(X, L) &DepthH(T)<Max

Fig. 3.1. Changed protocol-independent inference rules

The function Depth_(X) expresses how many times are in the word X used function e, f or h.

For example:

X= e(m,k) DepthE(X) = 1

X= e([A,B,N,k,e(A,kb)],ka) DepthE(X) = 2

With using this restriction we have a new model and the adversaryâ€™s reasoning we

now describe using a set of formulae HC. The set HC consists of four parts HC =F1âˆªF2 âˆªH3

âˆªF4. H3 represents the modified protocol-independent rules [I.1]-[I.7] restricted with constant

MAX. The sets F1,F2 and F4 remain unchanged. Presence of an attack can be expressed as:

HC |= Messages(i,p).

Definition 4 (LDepth-computed answer): Let HC to be a logic program, that interprets

evaluation of communicating protocol C, HC=F1âˆªF2 âˆªH3 âˆªF4 reduced by constant MAX=n,

nâˆˆN, the substitution Î˜ is said to be a LDepth-computed answer for logic program HC and

query ?-Messages(X,Y) if there is a sequence (G0,Î˜0),...,(Gn,Î˜n) such that G0=Messages(X,Y)

and Gn= , Î˜=Î˜0...Î˜n|Var(G0).

Know we need to prove that this reduction of using protocol-independent rules doesnâ€™t change

the set of results.

Theorem 2: Consider FC= F1âˆªF2 âˆªF3 âˆªF4 and HC = F1âˆªF2 âˆªH3 âˆªF4

1. If Î˜ is LDepth-computed answer for HC and query ?-Messages(X,Y) then Î˜ is also L-

computed answer for FC and query ?-Messages(X,Y).

2. If Î˜ is L-computed answer for FC and query ?-Messages(X,Y) then Î˜ is also LDepth-

computed answer for HC and query ?-Messages(X,Y).

Proof: HC =F1âˆªF2 âˆªH3 âˆªF4 F=F1âˆªF2 âˆªF3 âˆªF4

and

1. So it is clear that if we have a substitution Î˜ the LDepth-computed answer for query ?-

Messages(X,Y) in reduced program HC then Î˜ is also L-computed answer for this query in

FC, because only distinction between FC and HC is in parts H3 and F3. So if in evaluation

the step from Gi to Gi+1 is done with the rule from H3 then it is also possible with the rule

from F3.(the body of such rule is smaller)

14

PDF created with FinePrint pdfFactory trial version http://www.fineprint.com

Conclusion: Every LDepth-computed answer in HC is also L-computed answer in FC.

2. Now we need to show that there donâ€™t exist such enumeration that is in FC and is not in

HC. We try it to prove by confrontation.

Consider, we have computation G=G0,...,Gn that exists in FC and doesnâ€™t exist in HC.

Computation G is a path in computation tree of logic program FC that describes

reasoning from initial knowledge to an attack and from Gi to Gi+1 was used rule ri

from logic program FC.

If G is in FC and is not in HC then it must in the path r1....rm exists the index j such that

rule rj that can be used by evaluation in FC but cannot be used in GC.

What a rule can be the rule rj?

a) rjâˆˆF2 â€“ is not true because in this case rj will be evaluated also in HC, so it holds

original theorem.

b) rjâˆˆF3 â€“ Consider itâ€™s true. Some of the rules from F3 arenâ€™t in HC because of

reduction in HC. If there is not any evaluation in HC, it is because of reduction.

That means that by reasoning the path of attack we used the rules for encryption,

hash or handshake more then MAX times (MAX = the maximal relevant depth of

used encryption, hash and handshake in protocol messages plus one). We have the

enumeration, it means that we have an attack so if the adversary is able to learn the

content of any encrypted message or session key than he learns that all only from

the protocol messages. But in the protocol messages there are not used words with

Depth_ more than MAX. There are two way how can words with depth more than

MAX came into being and than the adversary obtained it:

1. Any of the legitimate users used some of the rules from F3 more than

MAX times and then sent it in some of the protocol messages. â€“ it is not

true because of in the protocol messages there are not used words with

Depth_ more than MAX.

2. The adversary itself generated this word. It means that he obtained at the

beginning of the generation the original word (Depth_=0) or word that

Depth_ is less than MAX. By the attack it is important to obtain original

word not word ciphered by hash, handshake or encryption. So if we have

the enumeration and it leads to an attack. It does not have sense by the

adversary to generate from obtained word new word with Depth_ more

than MAX. Such word can not lead to attack. So it is not true that in

enumeration was used some of reduced rules more than MAX times.

Conclusion is that rjâˆˆF3 is not true.

c) rjâˆˆF4 â€“ is not true because in this case rj will be evaluated also in HC, so it holds

original theorem.

Result: rjâˆ‰F1 and rjâˆ‰F2 and rjâˆ‰F3 so it doesnâ€™t exist such rule rj and it means that we have

contradiction to our assumption of existence of the computed answer that is in FC and is not in

HC.

End of the proof.

15

PDF created with FinePrint pdfFactory trial version http://www.fineprint.com

3.2.3 Abductive approach

As it was mentioned abduction is a reasoning method (beside deduction and induction)

used in artificial intelligence and diagnostic methods. In the step two of our DLA model we

used the abduction for setting the conditions of possible attack on the protocol. Letâ€™s look

how it works. We assume that the reader is common with Abductive Logic Programming [12]

Definition 5 (Abductive Theory): An abudctive theory in ALP (abductive logic

programming) is a triple <FC,A,IC> where FC is a logic program (representing evaluation of

communication protocol C), A is a set of predicate symbols, called abducibles (in our case

predicates about knowledge of keys or key material), which are not defined (or are partially

defined) in FC, and IC is a set of first order closed formulae, called integrity constraints.

In an abductive theory < FC,A,IC>, the program FC models the basic structure of the problem

(in our case describe the evaluation of the protocol C), the abducibles play the role of the

answer-holders, for the solutions to particular tasks (goals) in the problem, and the integrity

constraints IC represent the validity requirements that any solution must respect. A goal G is a

logic programming goal. A solution to a goal G is an abductive explanation of G defined as

follows.

ñòð. 5 |