стр. 14 |

kab is derived from SKEYID_D=prf(prf([n,m],[ca,cb]),[xy11,ca,cb,0])

so we need to look for: Messages(i,[ca,cb,n,m,xy11]).

if the intruder knows [ca.cb.n.m.xy11] then he can derive (learn) the key.

Messages ( i, kab ) :- Messages ( i , [ ca, cb, n, m, xy11] ).

[I.6] Messages(i,[ca,cb,n,m,xy11]):-Messages(i,ca)&

&Messages(i,[cb,n,m,xy11]).

true 1.2.1 Messages ( i , ca )

1.2.2 Messages(i, [cb,n,m,xy11])

[I.6] Messages(i, [cb,n,m,xy11]):-Messages(i,cb)&

&Messages(i,[n,m,xy11]).

true 1.2.2.1 Messages(i,cb)

1.2.2.2 Messages(i,[n,m,xy11])

[I.6] Messages(i, [n,m,xy11]):-Messages(i,n)&

&Messages(i,[m,xy11]).

true 1.2.2.2.1 Messages ( i , n )

1.2.2.2.2 Messages(i, [m,xy11])

[I.6] Messages(i, [m,xy11]):-Messages(i,m)&

&Messages(i,xy11).

true 1.2.2.2.2.1 Messages ( i , m )

1.2.2.2.2 Messages(i, xy11)

a) [R.8] Messages(i, xy11):-Number(xy11)&

&DHkey(xy11,g1,x1,exp(g1,y1)&

&Messages(i,x1)&Messages(i,exp(g1,y1))&

&Number(x1)&Number(exp(g1,y1)).

true Number(xy11)

true Number(x1)

true Number(exp(g1,y1))

true DHKey(xy11,g1,x1,exp(g1,y1))

true Messages(i, exp(g1,y1))

Messages(i,x1)

Result: And this fact is impossible to obtain for the

intruder.

b) [R.8] Messages(i, xy11):-Number(xy11)&

&DHkey(xy11,g1,exp(g1,x1),y1)&

&Messages(i,exp(g1,x1))&Messages(i,y1)&

&Number(exp(g1,x1))&Number(y1).

true Number(xy11)

true Number(exp(g1,x1))

true Number(y1)

true DHKey(xy11,g1,x1,exp(g1,y1))

true Messages(i, exp(g1,x1))

Messages(i,y1)

Result: And this fact is impossible to obtain for the

intruder.

Fig. 5.14. Abduction for question (i,p) in IKE with PKE

40

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

6 Conclusions and future work

We understood the problem of analysis of communication protocols as two-

dimensional problem. One dimension is the method used by analysis of protocols and second

dimension is the complexity of analyzed protocols. The analysis of protocols is focused

especially on the key exchange protocols, because if we know to make an attack on such

protocol we can disabled or learn all following traffic.

We can distinguish two types of key exchange protocols:

1. with key server that distributes the new keys

2. without key server and without key distribution (the participants exchange only key

material used for key derivation}

The complexity of analysis of these groups is much different. The analysis of first

group of protocols is simple (in this group are simple protocols as Needham-Schroeder). The

complexity of second group is not simple. In such protocols we must include into analysis

also the key derivation. In this group belong protocols like IKE protocol. In Fig. 6.1 it is

shown comparison of methods and analyzed protocols.

Explanations: Y/N вЂ“ Y = analyzed / N = no attack found

? вЂ“ no information about analsis

Y/Y вЂ“ Y = analyzed / Y = an attack found

N/- вЂ“ N = not analyzed / -

Methods of analysis

BAN logic NRL Analyzer Dexter prover DLA method

Protocols

Needham-Schroeder

Simple Y/N Y/N Y/N Y/N

Otway-Rees ? ? Y/Y Y/Y

with SIG Y/N Y/Y N/- Y/Y

Complex with PSK Y/N Y/N N/- Y/N

IKE

(aggressive mode) with PKE Y/N Y/N N/- Y/N

Fig. 6.1. Methods and analyzed protocols

Some type of analyzes based on logic approaches have some weak places. As we

mentioned using of some protocol independent rules can lead to infinity cycles There are

logicвЂ™s analyses that ignore. In our method we try to minimize such problem with infinite

search space and we limited by analysis the number of possible evaluation of all functions

(decryption, encryption, concatenation and others). We also try to use new methods by

analysis and to show that such methods and limitations are correct and sound.

41

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

Another weak place analyses is description of the possibilities of the attacker. It is

because the description of an attacker strongly depends on known flaws of protocols.

The most of methods are independent on used cryptographic algorithms in protocol

and this can lead that these methods declare that an protocol is correct and secure but by using

with some cryptographic algorithm it is possible to do an attack on this protocol. The

influence of such relationship (between the protocol and used cryptographic algorithm) was

shown by Rajsky in [32]. He shows that in Needham-Schroeder protocol using with cipher of

Feistel type in ECB mode is possible to find direct attack on session key.

In the future work we want to improve our program for translation of the protocol into

inference rules. In this field it will be useful to translate a protocol such way that no additional

correct will be needed. But it is hard to say whether or not it will be possible to do this. The

problem is if we want to use this method by analysis of the key distribution protocols without

key server. In such protocols we need to make a lot of additional extensions, that are specific

for chosen protocol. But our DLA method was successfully used by this type of protocols too.

We also want to use our method by analysis of others protocols.

Bibliography

1. Bellare M., Rogaway P.: Entity authentication and key distribution. Advances in

Cryptology вЂ“ CryptoвЂ™93 Proceedings, (1993).

2. Bieber P.: A logic of Communication in a Hostile Environment. Proceedings the

Computer Security Foundations Workshop III. IEEE Computer Society Press, (1990) 14-

22

3. Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Transactions

on Computer Systems, (1990)

4. Carlsen U.: Cryptographic protocol flaws: Know your enemy. Computer security

Foundations Workshop VII, IEEE Computer Society Press (1994)

5. Carrel D., Harkins D.: Internet Key Exchange Protocol, RFC 2409 (1998).

6. Compton K.J., Dexter S.: Proofs Techniques for Cryptographic Protocols. Workshop at

ECAIвЂ™98, (1998) 25-39

7. Dexter S.: An Adversary-Centric Logic of Security and Authenticity. PhD thesis,

University of Michigan (1998).

8. Diffie W., van Oorschot P.C., Wiener M.J.: Authentication and authenticated key

exchanges. Design, Codes and Cryptography (1992).

9. Ferguson N., Schneier B.: A Cryptographic evaluation of IPSec.

http://www.counterpane.com (1999)

10. JenДЌ uЕЎovГЎ E., JirГЎsek J.: Formal methods of analysis of security protocols.

TATRACRYPT 2001 (2001). Submitted to Tatra Mountains Math. Publ.

11. Kakas A.C., Michael A.: An Abductive-Based Scheduler for Air-Crew Assignment.

12. Kakas A.C., Michael A.: Abductive Logic Programming. Journal of Logic and

Computation 2, (1993).

13. Kemmerer R., Meadows C., Millen J.: Three systems for cryptographic protocol analysis.

стр. 14 |