L’essor des nouvelles technologies, et en particulier la Communication en Champ Proche (NFC), a permis l’apparition de nouvelles applications. Á ce titre, nous pouvons mentionner le paiement sans contact, les clefs mains libres ou encore les carte d’abonnement dans les transports en commun. Afin de sécuriser l’ensemble de ces applications, des protocoles de sécurité, appelés protocoles délimiteurs de distance on été développés. Ces protocoles ont pour objectif d’assurer la proximité physique des appareils mis en jeu afin protocole cryptographique, protocole de paiement de limiter le risque d’attaque. Dans ce manuscrit, nous présentons diverses approches permettant une analyse formelle de ces protocoles. Dans ce but, nous proposons un modèle symbolique permettant une modélisation précise du temps ainsi que des positions dans l’espace de chaque participant. Nous proposons ensuite deux approches : la première développant une nouvelle procédure de vérification, la seconde permettant la ré-utilisation d’outils existants tels que Proverif. Tout au long de ce manuscrit, nous porterons une attention parti- culières aux protocoles de paiement sans contact.