Group Key Transfer (GKT) protocols allow multiple parties to share a common secret key: a trusted Key Generation Center (KGC) selects a uniformly random value that has never been used before and securely distributes it to the legitimate principals. The paper restricts to GKT based on secret sharing; it briefly reviews the security goals and the existing formal security models. We motivate our work by the lack of GKT protocols based on secret sharing that are proved secure in a formal security model. Most of the recent proposals only provide informal and incomplete arguments to claim security, which makes them susceptible to known vulnerabilities. We support our affirmation by exemplifying with three different types of attacks (replay attack, insider attack and known key attack) mounted against protocols published within the last three years. We emphasize that none of these attacks would have been possible against a GKT protocol proved secure in a usual formal security model.