Active Attacking Multicast Key Management Protocol Using Alloy

In this paper, we use Alloy Analyzer, a fully automatic checker, to detect vulnerabilities in the multicast key management protocol proposed by Tanaka and Sato, and discover some previously unknown attacks. We model an active intruder in Alloy, and use Alloy Analyzer to test whether the active intruder can successfully attack the protocol. In this analysis, we check four critical properties that should be satisfied by any secure multicast protocol. However, none of these properties are satisfied. The protocol cannot resist the active intruder. Two unknown flaws caused by the active intruder are disclosed, and another two flaws found by CORAL are identified.

Authors and Affiliations

1. The State Key Laboratory of Information Security, Graduate University of the Chinese Academy of Sciences Institute of Information Engineering, Chinese Academy of Sciences, No.89 Minzhuang Road, Haidian District, Beijing, 100195, P.R. China

   Ting Wang & Dongyao Ji

Editors and Affiliations

1. Department of Computer Science, University of Sheffield, Regent Court, 211 Portobello Street, S1 4DP, Sheffield, UK

   John Derrick

2. Newcastle University, UK

   John Fitzgerald

3. Consiglio Nazionale delle Ricerche, Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, Via Moruzzi 1, 56124, Pisa, Italy

   Stefania Gnesi

4. Electrical and Computer Engineering, The University of Texas at Austin, 1 University Station C5000, 78712-0240, Austin, TX, USA

   Sarfraz Khurshid

5. Heinrich-Heine-University of Düsseldorf, Germany

   Michael Leuschel

6. Department of Computer Science, The University of Waikato, 3240, Hamilton, New Zealand

   Steve Reeves

7. Department of Information Technology, Università degli Studi di Milano, via Bramante 65, 26013, Crema, Italy

   Elvinia Riccobene

Reprints and permissions

© 2012 Springer-Verlag Berlin Heidelberg

Policies and ethics