Sp cification Et Validation de Protocoles de S curit

Dans cet ouvrage, nous abordons le problme de la vrification de protocoles de scurit. Plus spcifiquement, nous proposons une mthode gnrale de spcification et de validation pour cette famille de protocoles, qui inclue les protocoles cryptographiques. Nous prsentons une nouvelle algbre de processus, nomme SPPA, qui permet une spcification explicite des changes de messages entre les participants d'un protocole et des manipulations cryptographiques accomplies par chacun. Une extension symbolique de cette algbre de processus est galement offerte. Nous introduisons ensuite la proprit de scurit BNAI qui est une formalisation du concept d'interfrence admissible munie d'une mthode de vrification base sur l'quivalence de bisimulation. Nous dmontrons que BNAI satisfait certaines proprits de compositionalit par rapport aux principaux oprateurs de SPPA. Nous prouvons aussi que BNAI n'est pas dnissable dans le -calcul et nous montrons comment utiliser BNAI afin de valider certaines proprits de scurit, notamment la confidentialit, l'authentification et la vulnrabilit face aux attaques de dni de service.