Les politiques permettent de définir les règles de la sécurité et de la gestion des différents composants du système. Cela implique l'emploi d'un langage pour exprimer les règles d'affaires et les règles non fonctionnelles, et de donner aux utilisateurs la possibilité de tester et de corriger les politiques. Plusieurs langages tels que XACML, Rei ou PONDER, sont utilisés pour exprimer les politiques par rapport aux objectifs du système d'information. Ces langages peuvent définir plusieurs règles et politiques, mais la plupart de ces langages ne donnent pas de mécanisme pour tester et vérifier la présence des conflits et de l'incohérence entre les politiques du système. Ce mémoire vise la vérification des politiques de contrôle d'accès. Notre approche consiste à traduire les politiques XACML sous forme d'un ensemble de machines abstraites de la méthode B. Nous exprimons aussi les propriétés à vérifier par des formules logiques. L'approche offre aux utilisateurs des moyens pour vérifier les politiques afin de s'assurer que les règles expriment bien les objectifs régissant le comportement et les interactions des systèmes gérés. Dans la première phase, les composantes des politiques XACML ont été exprimées avec des expressions formelles basées sur la logique du premier ordre. Par la suite, les outils développés pour la méthode B, comme le langage Event-B sous la plate forme Rodin, ont été utilisés pour vérifier les règles des politiques par rapport à un ensemble de propriétés que nous avons définies. Notre approche est plus flexible et permet aux utilisateurs de tester et de vérifier les règles avant l'implémentation de ces politiques. Une telle vérification est fondée sur les preuves avec logique du premier ordre, où des propriétés importantes de la politique peuvent être énoncées et prouvées. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Politique, XACML, Méthode formelle, Event-B, Vérification.