La sécurité est une exigence cruciale dans les applications basées sur l'information et la technologie de communication, surtout quand un réseau ouvert tel que l'Internet est utilisé. Pour assurer la sécurité dans ces applications des protocoles cryptographiques ont été développé. Cependant, la conception de protocoles de sécurité est notoirement difficile et source d'erreurs. Plusieurs failles ont été trouvées sur des protocoles qui se sont prétendus sécurisés. Par conséquent, les protocoles cryptographiques doivent être vérifiés avant d'être utilisés. Une approche pour vérifier les protocoles cryptographiques est l'utilisation des méthodes formelles, qui ont obtenu de nombreux résultats au cours des dernières années.Méthodes formelles portent sur l'analyse des spécifications des protocoles modélisées en utilisant, par exemple, les logiques dédiés, ou algèbres de processus. Les méthodes formelles peuvent trouver des failles ou permettent de prouver qu'un protocole est sécurisé sous certaines hypothèses par rapport aux propriétés de sécurité données. Toutefois, elles abstraient des erreurs de mise en ouvre et les attaques side-channel.Afin de détecter ces erreurs et la vérification des attaques d'exécution peut être utilisée pour analyser les systèmes ou protocoles exécutions. En outre, la vérification de l'exécution peut aider dans les cas où les procédures formelles mettent un temps exponentielle ou souffrent de problèmes de terminaison. Dans cette thèse, nous contribuons à la vérification des protocoles cryptographiques avec un accent sur la vérification formelle et l'automatisation. Tout d'abord, nous étudions les protocoles d'examen. Nous proposons des définitions formelles pour plusieurs propriétés d'authentification et de confidentialité dans le Pi-calcul Appliqué.Nous fournissons également une des définitions abstraites de propriétés de vérifiabilité. Nous analysons toutes ces propriétés en utilisant automatiquement ProVerif sur plusieurs études de cas, et avons identifié plusieurs failles. En outre, nous proposons plusieurs moniteurs de vérifier les exigences d'examen à l'exécution. Ces moniteurs sont validés par l'analyse d'un exécutions d'examen réel en utilisant l'outil MARQ Java.Deuxièmement, nous proposons un cadre formel pour vérifier les propriétés de sécurité de protocoles de monnaie électronique non transférable. Nous définissons la notion de vie privée du client et les propriétés de la falsification. Encore une fois, nous illustrons notre modèle en analysant trois études de cas à l'aide ProVerif, et confirmons plusieurs attaques connues.Troisièmement, nous proposons des définitions formelles de l'authentification, la confidentialité et les propriétés de vérifiabilité de protocoles de réputation électroniques. Nous discutons les définitions proposées, avec l'aide de ProVerif, sur un protocole de réputation simple. Enfin, nous obtenons un résultat sur la réduction de la vérification de la validité d'une route dans les protocoles de routage ad-hoc, en présence de plusieurs attaquants indépendants qui ne partagent pas leurs connaissances. / Security is a crucial requirement in the applications based on information and communication technology, especially when an open network such as the Internet is used.To ensure security in such applications cryptographic protocols have been used.However, the design of security protocols is notoriously difficult and error-prone.Several flaws have been found on protocols that are claimed secure.Hence, cryptographic protocols must be verified before they are used.One approach to verify cryptographic protocols is the use of formal methods, which have achieved many results in recent years.Formal methods concern on analysis of protocol specifications modeled using, e.g., dedicated logics, or process algebras.Formal methods can find flaws or prove that a protocol is secure under ``perfect cryptographic assumption" with respect to given security properties. However, they abstract away from implementation errors and side-channel attacks.In order to detect such errors and attacks runtime verification can be used to analyze systems or protocols executions.Moreover, runtime verification can help in the cases where formal procedures have exponential time or suffer from termination problems.In this thesis we contribute to cryptographic protocols verification with an emphasis on formal verification and automation.Firstly, we study exam protocols. We propose formal definitions for several authentication and privacy propertiesin the Applied Pi-Calculus. We also provide an abstract definitions of verifiability properties.We analyze all these properties automatically using ProVerif on multiple case studies, and identify several flaws.Moreover, we propose several monitors to check exam requirements at runtime. These monitors are validated by analyzing a real exam executions using MARQ Java based tool.Secondly, we propose a formal framework to verify the security properties of non-transferable electronic cash protocols.We define client privacy and forgery related properties.Again, we illustrate our model by analyzing three case studies using ProVerif, and confirm several known attacks.Thirdly, we propose formal definitions of authentication, privacy, and verifiability properties of electronic reputation protocols. We discuss the proposed definitions, with the help of ProVerif, on a simple reputation protocol.Finally, we obtain a reduction result to verify route validity of ad-hoc routing protocols in presence of multiple independent attackers that do not share their knowledge.

Avec les mutations de l’internet induites par le développement des outils collaboratifs (blogs, flux RSS, réseaux sociaux, partage d’informations...) l'information change de nature. Sa production devient de plus en plus simple. L'utilisateur, qui depuis les débuts de l’internet grand-public, se contentait d’un rôle de consommateur tout-court d'informations s'est, petit-à-petit, transformé en « consommateur-producteur ». Il est au cœur du nouveau système de production et de diffusion de l’information. Ce changement qui s'opère dans toutes les couches sociales avec comme caractéristiques principales la floraison des blogs, la veille personnalisée, la customisation des outils, le partage, la collaboration dans les réseaux sociaux ..., s’identifie à travers les appellations « web 2.0 », « web social », « web collaboratif ». Plus que des mots, il s’agit de pratiques informationnelles qui mettraient en cause les acquis des entreprises en matière de veille et d'Intelligence Économique. Ainsi, l'intérêt de mesurer les tenants et les aboutissants de ce renouvellement des usages informationnels nous pousse à travers cette thèse à s’interroger sur leur impact réel ou supposé dans la veille et l'Intelligence Économique. Ce travail propose de mesurer le degré de récupération des compétences des utilisateurs du web 2.0 dans les démarches de veille et d’IE en PME et TPE. À l’issue d’une enquête de terrain portant sur un échantillon de 70 entreprises de différentes régions du monde (France, États-Unis, Grande-Bretagne, Maroc, Sénégal…) il a été intéressant de constater que le web 2.0 est assez bien connu dans les entreprises quelle que soit leur taille. Toutefois, la récupération de ses applications dans une démarche de veille et d’Intelligence Économique reste assez dispersée du fait, notamment, de la méconnaissance des potentialités de certains outils, qui a comme conséquence leur non prise en compte dans les politiques informationnelles. Ce résultat nous a convaincu de proposer aux TPE et aux PME une démarche de mise en place d’un dispositif de veille collaborative qui a l’originalité d’intégrer les outils du web 2.0. S’inscrivant dans la logique d’un dispositif de veille de seconde génération (Lietzelman et al.), la démarche proposée constitue une amélioration de celles déjà existantes (AFNOR, Paul Degoul). Elle prend en compte dans chacune des phases (conception, planification et mise en œuvre) la dimension sociale de l’internet et de ses pratiques. Un exposé de techniques d’exploitation de certains de ces outils pour un problème de veille a été produit afin de sensibiliser sur leurs potentialités dans l’éventualité de leur intégration dans un système de veille et d’intelligence économique / With the web as a platform and the development of collaborative tools (blogs, RSS feeds, social networking, information sharing ...) information is changing and its production becomes increasingly simple. The average user, who since the advent of the Internet has merely a short role as consumer of information, is transformed into a "consumer-producer" of information. He is at the heart of the new system of production and dissemination of information. This change whose characteristics cannot be ignored: blogs, personal monitoring, social bookmarking, personalization tools for research, collaboration in social networks etc. and known under the names "Web 2.0", "social web", "collaborative web" would undermine the achievements of companies in terms of information monitoring and Competitive Intelligence (CI); hence the importance of measuring the ins and outs of this renewal informational practices. In addition to questions about the real or supposed changes in information monitoring and Competitive Intelligence in the Age of social web, our research also wanted to measure the degree of recovery skills of web 2.0’s users in SMEs CI‘s systems. With a field survey covering a sample of 70 companies from different regions of the world (France, USA, Great Britain, Morocco, Senegal ...) we noticed that the Web 2.0 is fairly well known by companies regardless of their size, but the recovery of its applications in a process to monitor information is dispersed (using disparate, breach of certain tools potential, lack of information policy incorporating tools 2.0...). This result has convinced us to propose to the SME an approach of establishing a collaborative information monitoring system which has the originality to include the tools of Web 2.0 since the phases of design, planning and implementation. In order to respect the logic of a second generation Information Monitoring System (Lietzelman et al.), the proposed approach is an improvement of existing ones like the AFNOR system or that of Paul Degoul. It is accompanied, for sensitizing SME by a statement of operational techniques of some social media tools for their possible inclusion in a Competitive Intelligence System