Subject: Re: [eap] Formal Analysis of EAP methods

From: "Bernard Aboba" <[email-masked]>
Date: Wed, 17 Jan 2007 07:23:13 -0800

I'm not familiar with AVISPA, but there has been a formal analysis of 
EAP-TLS using murphi, by He:

[He]         He, C., Sundararajan, M., Datta, A. Derek, A. and J. C.
               Mitchell, "A Modular Correctness Proof of TLS and IEEE
               802.11i", ACM Conference on Computer and Communications
               Security (CCS '05), November, 2005.

This proof included 11i, the 4-way handshake, but not the AAA exchange (no 
pass-through).

Adding in the AAA exchange would be an interesting extension, because it 
would enable other EAP methods to be modelled more completely.  However, 
such an analysis would be likely to disclose that AAA is the weak link in 
most cases.

The RFC 3579 and the EAP Key Management Framework document talk about some 
of the assumptions that would need to be made for the modelling of the AAA 
exchange, such as:

a. Unique shared keys for each NAS - AAA server.  If this is not true, then 
NASes can impersonate each other, and the AAA server will never be clear 
which NAS has received the transported key.

b. Global and temporal uniqueness of the Request Authenticator.  If the RA 
is not globally and temporally unique, then the key transport messages can 
be replayed.

c. Shared secret with full entropy.  Otherwise, the RADIUS shared secret 
itself can be cracked.

d. No usage of PAP along with EAP on the same NAS.  As noted in RFC 3579, 
the User-Password attribute is vulnerable to known plaintext attacks.

e. Credible keywrap.  RFC 2548 probably doesn't qualify.

In practice, assumptions a-e are probably not simultaneously true in most 
situations unless special measures are taken (e.g. RADIUS over IPsec as 
recommended in RFC 3579).

=========================================================

Security Properties Analysis of EAP-IKEv2
From: Salekul Islam (isalekulhotmail.com)
Date: Mon, 15 Jan 2007 07:38:05 -0800 (PST)
Hi All,

I like to know about the formal analysis of EAP-IKEv2. In the Security 
Considerations section of draft-tschofenig-eap-ikev2, some specific security 
terminologies required by RFC 3748 are described.

I have found an AVISPA model, which is three years old. Is there any other 
model or formal analysis approach of EAP-IKEv2? Can we assume this AVISPA 
model a good interpretation of the EAP-IKEv2 to validate most of the 
security properties?

I am more interested in the pass-through mode of EAP-IKEv2. I am aware of 
the vulnerabilities of the AAA key transport (e.g., MITM attack), but I am 
focusing the EAP method only. More specifically, if we follow the EAP Key 
Management Framework draft, I am concerned about the security properties 
analysis of phase 1a (see section 1.3 of draft-ietf-eap-keying) of 
EAP-IKEv2.

I have a general question to ask. I have noticed that most (not all) of the 
EAP methods are not modeled and analyzed formally using a tool. All of them 
have Security Considerations section where their security properties are 
described in terms of RFC 3748. Is this the standard (and only) way of 
dealing with security of these methods? Or the WG has some future plan to 
deal this more concretely?

Thanks and regards,

Salekul

_________________________________________________________________
To unsubscribe or modify your subscription options, please visit:
http://lists.frascone.com/mailman/listinfo/eap

Arhives: http://lists.frascone.com/pipermail/eap

---

From: Salekul Islam <[email-masked]>
Date: Wed, 17 Jan 2007 17:05:58 +0000

Hi Bernard,Thank you for your reply. > Adding in the AAA exchange would be an interesting extension, because it > would enable other EAP methods to be modelled more completely.  However, > such an analysis would be likely to disclose that AAA is the weak link in > most cases.I  am discussing about analyzing the communication of the EAP methods only (not the AAA key transport messages). The EAP methods (e.g., EAP-IKEv2) are presented in peer-to-peer fashion by showing  the communication of the responder and the peer.  If  we add  NAS  in  pass-through  mode  it  may  raise  vulnerabilities. That's why an EAP method should be analyzed formally in pass-through mode.    Regards,Salekul
_________________________________________________________________
Be one of the first to try Windows Live Mail.
http://ideas.live.com/programpage.aspx?versionId=5d21c51a-b161-4314-9b0e-4911fb2b2e6d