Dans ce rapport, nous validons notre protocole de gestion de clés de groupe multicast, dénommé BALADE, afin de détecter les éventuelles failles de sécurité qui peuvent exister. Notre approche de validation suit trois étapes essentielles : (1) spécification des sous protocoles de BALADE de manière générale, (2) spécification des scénarii de ces protocoles en HLPSL, et finalement (3) vérification de ces scénrii avec l'outil AVISPA.