La dépendance de plus en plus grande à l'égard des systèmes informatiques soulève d'importantes questions en terme de vie privée, et nécessite notamment des protocoles de communication garantissant des propriétés de sécurité telles que la non-traçabilité. Spécifier formellement cette propriété est difficile et dépendant du contexte, et la vérifier est d'autant plus complexe. Fournir des bases mathématiques solides et des méthodes assistées par ordinateur devient donc crucial, mais les techniques actuelles ne sont pas satisfaisantes pour analyser la non-traçabilité des protocoles à état. Dans ce manuscrit de thèse, nous abordons à la fois la question de la modélisation et de la vérification. Tout d'abord, nous proposons une définition précise de non-traçabilité et expliquons pourquoi les notions actuelles ne sont pas adaptées à notre classe de protocoles à état. Ensuite, nous abordons la question de la vérification assistée par ordinateur. Nous développons deux approches, illustrées par des études de cas. Notre première approche est une méthode de vérification basée sur des conditions suffisantes dans le modèle symbolique. Notre deuxième approche est un cadre théorique et un assistant de preuve interactif permettant de mécaniser des preuves de protocoles cryptographiques pour un nombre arbitraire de sessions dans le modèle calculatoire.