06086738

a

06086738 Wang, Ting Ji, Dongyao Active attacking multicast key management protocol using Alloy. Derrick, John (ed.) et al., Abstract state machines, Alloy, B, VDM, and Z. Third international conference, ABZ 2012, Pisa, Italy, June 18--21, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-30884-0/pbk). Lecture Notes in Computer Science 7316, 164-177 (2012). 2012 Berlin: Springer EN Alloy multicast key management active intruder security protocol analysis

doi:10.1007/978-3-642-30885-7_12

Summary: 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.