Dans cette thèse, nous nous intéressons à la garantie des propriétés d'intégrité et de confidentialité d'un système d'information.<br />Nous proposons tout d'abord un langage de description des activités système servant de base à la définition d'un ensemble de propriétés de sécurité.<br />Ce langage repose sur une notion de dépendance causale entre appels système et sur des opérateurs de corrélation.<br />Grâce à ce langage, nous pouvons définir toutes les propriétés de sécurité système classiquement rencontrées dans la littérature, étendre ces propriétés et en proposer de nouvelles.<br />Afin de garantir le respect de ces propriétés, une implantation de ce langage est présentée.<br />Nous prouvons que cette implantation capture toutes les dépendances perceptibles par un système.<br />Cette méthode permet ainsi d'énumérer l'ensemble des violations possibles des propriétés modélisables par notre langage.<br />Notre solution exploite la définition d'une politique de contrôle d'accès afin de calculer différents graphes.<br />Ces graphes contiennent les terminaux du langage et permettent de garantir le respect des propriétés exprimables.<br />Nous utilisons alors cette méthode pour fournir un système de détection d'intrusion qui détecte les violations effectives des propriétés.<br />L'outil peut réutiliser les politiques de contrôle d'accès disponibles pour différents systèmes cibles DAC (Windows, Linux) ou MAC tels que SELinux et grsecurity.<br />Cet outil a été expérimenté sur un pot de miel durant plusieurs mois et permet de détecter les violations des propriétés souhaitées.

Les protocoles cryptographiques sont cruciaux pour sécuriser les transactions électroniques. La confiance en ces protocoles peut être augmentée par l'analyse formelle de leurs propriétés de sécurité.<br />Bien que beaucoup de travaux aient été dédiés pour les protocoles classiques comme le protocole de Needham-Schroeder, très peu de travaux s'adressent à la classe des protocoles de groupe dont les caractéristiques principales sont : les propriétés de sécurité spécifiques qu'ils doivent satisfaire, et le nombre arbitraire des participants qu'ils impliquent. <br /> Cette thèse comprend deux contributions principales. La première traite la première caractéristique des protocoles de groupe. <br />Pour cela, nous avons défini un modèle appelé modèle de services que nous avons utilisé pour proposer une stratégie de recherche d'attaques se basant sur la résolution de contraintes. L'approche proposée a permis de retrouver d'anciennes attaques et d'en découvrir de nouvelles sur quelques protocoles de groupe. Certaines attaques ont aussi pu être généralisées pour couvrir le cas de $n$ participants. La deuxième contribution principale de cette thèse consiste à définir un modèle synchrone qui généralise les modèles standards de protocoles en permettant les listes non bornées à l'intérieur des messages. Ceci est assuré par l'introduction d'un nouvel opérateur appelé $mpair$ qui représente une liste construite sur un même patron. Dans ce modèle étendu, nous avons proposé une procédure de décision pour une classe particulière des protocoles de groupe appelée classe de protocoles bien-tagués avec clefs autonomes, en présence d'un intrus actif et avec des clefs composées.