Publisher's Synopsis
Dans cet ouvrage, nous abordons le probl�me de la v�rification de protocoles de s�curit�. Plus sp�cifiquement, nous proposons une m�thode g�n�rale de sp�cification et de validation pour cette famille de protocoles, qui inclue les protocoles cryptographiques. Nous pr�sentons une nouvelle alg�bre de processus, nomm�e SPPA, qui permet une sp�cification explicite des �changes de messages entre les participants d'un protocole et des manipulations cryptographiques accomplies par chacun. Une extension symbolique de cette alg�bre de processus est �galement offerte. Nous introduisons ensuite la propri�t� de s�curit� BNAI qui est une formalisation du concept d'interf�rence admissible munie d'une m�thode de v�rification bas�e sur l'�quivalence de bisimulation. Nous d�montrons que BNAI satisfait certaines propri�t�s de compositionalit� par rapport aux principaux op�rateurs de SPPA. Nous prouvons aussi que BNAI n'est pas d�nissable dans le �-calcul et nous montrons comment utiliser BNAI afin de valider certaines propri�t�s de s�curit�, notamment la confidentialit�, l'authentification et la vuln�rabilit� face aux attaques de d�ni de service.
