On the formal verification of group key security protocols