Les Syst mes de D tection d'Intrusions (IDS) ont de nos jours une importance capitale dans la s curisation des r seaux, ce qui a fait d'eux des cibles d'attaques privil gi es. Face cet tat de fait, le test de leur bon fonctionnement est devenu primordial dans tout processus de s curisation d'un r seau. Cependant les techniques de test usuelles s'av rent aujourd'hui insuffisantes. Nous nous sommes int ress s dans ce travail la mod lisation, la sp cification, et la v rification formelle des propri t s, des m canismes, et des protocoles de s curit des IDS. Pour ce faire, nous avons utilis le langage de sp cification formelle TLA+, et son Model Checker TLC. TLA+ ayant t con u pour la sp cification des syst mes concurrents et r partis, nous l'avons adopt dans le cadre de ce travail pour couvrir des probl matiques de s curit . Apr s un travail de sp cification et de validation des IDS, nous avons propos une extension TLA+ et TLC, afin de pouvoir d tecter les cycles ind sirables pouvant surgir suite une sp cification erron e.