Dans cet ouvrage, nous abordons le probleme de la verification de protocoles de securite. Plus specifiquement, nous proposons une methode generale de specification et de validation pour cette famille de protocoles, qui inclue les protocoles cryptographiques. Nous presentons une nouvelle algebre de processus, nommee SPPA, qui permet une specification explicite des echanges de messages entre les participants d'un protocole et des manipulations cryptographiques accomplies par chacun. Une extension symbolique de cette algebre de processus est egalement offerte. Nous introduisons ensuite la propriete de securite BNAI qui est une formalisation du concept d'interference admissible munie d'une methode de verification basee sur l'equivalence de bisimulation. Nous demontrons que BNAI satisfait certaines proprietes de compositionalite par rapport aux principaux operateurs de SPPA. Nous prouvons aussi que BNAI n'est pas denissable dans le u-calcul et nous montrons comment utiliser BNAI afin de valider certaines proprietes de securite, notamment la confidentialite, l'authentification et la vulnerabilite face aux attaques de deni de service."