Les Systemes de Detection d'Intrusions (IDS) ont de nos jours une importance capitale dans la securisation des reseaux, ce qui a fait d'eux des cibles d'attaques privilegiees. Face a cet etat de fait, le test de leur bon fonctionnement est devenu primordial dans tout processus de securisation d'un reseau. Cependant les techniques de test usuelles s'averent aujourd'hui insuffisantes. Nous nous sommes interesses dans ce travail a la modelisation, la specification, et la verification formelle des proprietes, des mecanismes, et des protocoles de securite des IDS. Pour ce faire, nous avons utilise le langage de specification formelle TLA+, et son Model Checker TLC. TLA+ ayant ete concu pour la specification des systemes concurrents et repartis, nous l'avons adopte dans le cadre de ce travail pour couvrir des problematiques de securite. Apres un travail de specification et de validation des IDS, nous avons propose une extension a TLA+ et a TLC, afin de pouvoir detecter les cycles indesirables pouvant surgir suite a une specification erronee."