Model-based Group Communication Security Analysis Techniques And Applications

Protocol reverse engineering is important to trusted software verification, protection and malware analysis. Because of protocol's complexity, it's particularly helpful to reconstruct high-level model which is consistent with the protocol's source code among which the finite state machine (FSM) model is the most widely used. The authenticated group key exchange protocol is one of the most foundamental security components in netwok environment, particularly in contamprary wireless mobile/ad hoc networks. However, the group key exchange protocol (or more generally, any group secure protocol) has a series of new requirements and problems, making it much more complicated than its traditional 2-party counterparts.This paper firstly proposes an efficient method to reconstruct network protocol's FSM model from the recorded transcripts and execution traces in protocol's sessions via decompilation and enhanced formal analysis/verification techniques, resulting in state instances, transition relations and state-transition conditions in the FSM. As a result, a generic FSM model is reconstructed from execution trace instances with practical efficiency and provable soundeness. This paper secondly establishes the UC ideal model for authenticated group key exchange and group secure communication channels, which specifies almost all-known important requirenments for group secure communications, then a concrete group key exchange protocol is constructed based-upon decisional group Diffie-Hellman problem's hardness. This construction is not only adaptive to dynamic group environment, multual-authenticated and key-secret but also post-specified identified and anonymous (w.r.t. illegal group members or even among legal members). In addition, this construction is well-structured to adaptive to different design objectives and balances.