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
|