Sciweavers

Share
FORTE
2003

A Lightweight Formal Analysis of a Multicast Key Management Scheme

10 years 29 days ago
A Lightweight Formal Analysis of a Multicast Key Management Scheme
Abstract. This paper describes the analysis of Pull-Based Asynchronous Rekeying Framework (ARF), a recently proposed solution to the scalable group key management problem in secure multicast. A model of this protocol is constructed in Alloy, a lightweight relational modeling language, and analyzed using the Alloy Analyzer, a fully automatic simulation and checking tool for Alloy models. In this analysis, some critical correctness properties that should be satisfied by any secure multicast protocol are checked. Some flaws, previously unknown to the protocol’s designers are exposed, including one serious security breach. To eliminate the most serious flaw, some fixes are proposed and checked using the Alloy Analyzer. The case study also illustrates a novel modeling idiom that supports better modularity and is generally simpler and more intuitive than the conventional idiom used for modeling distributed systems.
Mana Taghdiri, Daniel Jackson
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2003
Where FORTE
Authors Mana Taghdiri, Daniel Jackson
Comments (0)
books