Analyzing Multicast Key Management Schemes
In this project Alloy is used to construct a framework for modelling a class of key management schemes used in secure multicast, aimed at checking them against some critical correctness properties that should be satisfied by all secure multicast protocols.
The framework is used to model pull-based Asynchronous Rekeying Framework (ARF) and Iolus, two very different proposed schemes addressing the scalability issue inherently involved in group key management problem. The models can be automatically analyzed using the Alloy Analyzer.
The proposed framework introduces a novel idiom for modelling distributed systems. Compared to the conventional way of modelling these systems, our idiom is simpler and more intuitive while supporting better modularity.