[MBONED] Formal Validation of Security Properties for AMT Exchanges

[Bill Atwood <[e-mail]>]

As part of a larger project using AMT to extend the reach of multicast
sessions, we have modeled the exchanges between an AMT gateway and its
associated AMT relay, using the AVISPA tools. (Automated Validation of
Internet Security Protocols and Applications; see
http://www.avispa-project.org/)

If specific attacks by an intruder are also modeled, it is possible to
demonstrate that the message exchanges are free from those attacks.

>From these augmented models, we have learned the following:

Authentication on the MAC
According to the Internet-Draft, the produced MAC is used only for
routability purposes by the respondent, and the originator does not need
to know anything about it in terms of content or hashing algorithm.  As
a result, if any party represents itself as an authentic AMT Relay, the
AMT Gateway has no way to figure out otherwise.  All the scenarios that
we tested produced the same result: a Relay Impersonation attack was
found where the intruder pretended to be a Relay and consequently fooled
the Gateway.  Note that since an intruder can easily present himself as
a Relay, he will be able to easily learn the unsecured parameters
exchanged with the Gateway.

Secrecy of the MAC
The MAC is sent in the clear, so the lack of secrecy of the MAC is
obvious.  While the MAC is composed from some parameters (the example
given in the draft is "the source IP of the request, the source UDP
port, the request nonce and a secret key known only to the respondent"),
it is produced using a one-way cryptographic hash, making it unlikely
that the intruder could figure out the original parameters.  However, an
intruder may be able to make use of the MAC by sending a Membership
update Leave/Done message to the Relay while spoofing the source IP
address of the Gateway.  This can result in the Relay disconnecting the
unicast stream to the Gateway.  An example of this sequence of events
has been demonstrated by AVISPA.

Secrecy of the Local Secret
According to the Internet Draft, the Local Secret ("the secret known
only to the respondent") never has to be shared with the other side; it
is only used to verify return routability of the originator.  The
Gateway does not care what the Local Secret is or what the MAC produced
by the Relay is, since it simply echoes it in the AMT membership update
message.  An intruder cannot figure out the original parameters of the
MAC (see above), and thus will not be able to learn the value of the
Local Secret.  To further confirm this, the validation results from all
of our scenarios showed the protocol to be safe with respect to this
goal for a bounded number of sessions.

Implications

1) The Security Considerations section of the draft should at least
acknowledge the existence of the Relay Impersonation attack, even if the
solution to it is declared to be out-of-scope.

2) The design team should consider whether or not it is necessary to
protect the MAC.  If the decision is made not to alter the protocol to
achieve this, the potential attack should be noted in the Security
Considerations section of the draft.

Bill Atwood
Ali Salem

-- 

Dr. J.W. Atwood, Eng.             tel:   [phone] x3046
Distinguished Professor Emeritus  fax:   [phone]
Department of Computer Science
   and Software Engineering
Concordia University EV 3.185     email: [e-mail]
1455 de Maisonneuve Blvd. West    http: //users.encs.concordia.ca/~bill
Montreal, Quebec Canada H3G 1M8