Cette thèse s’attache à étudier les représentations de la vie intime, réalisées dans des techniques et sur des supports variés (peinture, dessin, gravure), entre 1780 et 1815. À cette période, l’intimité connaît une évolution sémantique et une utilisation plus développée : d’une acception limitée à la définition des liens entre deux individus, progressivement sa signification prend une tournure secrète, et s’étend à tout ce que nous ne dévoilons qu’à un cercle réduit d’individus – qu’il s’agisse du for intérieur, des sentiments affectifs ou encore de la sexualité. Ces changements sémantiques sont accompagnés d’une évolution des pratiques domestiques, culturelles et littéraires qui corroborent l’idée d’une période décisive dans l’histoire de l’intimité. Ce travail analyse ainsi les différentes manières de figurer l’intimité, et interroge en outre la destination et la réception des œuvres, afin de comprendre ce que nous révèle la démonstration de l’intimité sur les mœurs de la société française au tournant du XIXe siècle. L’examen de différents modes de diffusion et d’exposition des images, ainsi que le dépouillement des témoignages écrits offerts par la critique permettent de cerner les goûts du public et d’avoir une idée sur la place qui était accordée à ces images, dans les expositions publiques et dans les collections privées. / This thesis examines the representations of private life, made with diverse technics and mediums (painting, drawing, engraving), between 1780 and 1815. At this time, intimacy shows an evolution in its semantic and its usage : from a limited meaning to the definition of the relationship between two individuals, gradually its signification approaches the notion of secrecy, and extends to everything we reveal only to small cercles of persons, to our heart of hearts, our emotional feelings, or sexuality. These semantic shifts come along a domestic, cultural and literary evolution, which support the idea of a decisive time period in the history of privacy. Therefore this work analyses the different ways of representing intimacy and questions whom those works of art were destined to and how they were received, in order to understand the habits and customs of the french society at the turning point of the 19th century. The study of the various methods of exhibiting the pictures as well as the analyse of the writing accounts of the art critics help to more fully understand the taste of the audience and the place the pictures had in the public expositions and in the private collections.

Nous assistons à la démocratisation des services ducloud et de plus en plus d’utilisateurs (individuels ouentreprises) utilisent ces services dans la vie de tous lesjours. Dans ces scénarios, les données personnellestransitent généralement entre plusieurs entités.L’utilisateur final se doit d’être informé de la collecte, dutraitement et de la rétention de ses donnéespersonnelles, mais il doit aussi pouvoir tenir pourresponsable le fournisseur de service en cas d’atteinte àsa vie privée. La responsabilisation (ou accountability)désigne le fait qu’un système ou une personne estresponsable de ses actes et de leurs conséquences.Dans cette thèse nous présentons un framework deresponsabilisation AccLab qui permet de prendre enconsidération la responsabilisation dès la phase deconception d’un système jusqu’à son implémentation.Afin de réconcilier le monde juridique et le mondeinformatique, nous avons développé un langage dédiénommé AAL permettant d’écrire des obligations et despolitiques de responsabilisation. Ce langage est basé surune logique formelle FOTL ce qui permet de vérifier lacohérence des politiques de responsabilisation ainsi quela compatibilité entre deux politiques. Les politiques sontensuite traduites en une logique temporelle distribuéeque nous avons nommée FO-DTL 3, cette dernière estassociée à une technique de monitorage basée sur laréécriture de formules. Enfin nous avons développé unoutil monitorage appelé AccMon qui fournit des moyensde surveiller les politiques de responsabilisation dans lecontexte d’un système réel. Les politiques sont fondéessur la logique FO-DTL 3 et le framework peut agir enmode centralisée ou distribuée et fonctionne à la fois enligne et hors ligne. / Nowadays we are witnessing the democratization ofcloud services. As a result, more and more end-users(individuals and businesses) are using these services intheir daily life. In such scenarios, personal data isgenerally flowed between several entities. End-usersneed to be aware of the management, processing,storage and retention of personal data, and to havenecessary means to hold service providers accountablefor the use of their data. In this thesis we present anaccountability framework called AccountabilityLaboratory (AccLab) that allows to consideraccountability from design time to implementation time ofa system. In order to reconcile the legal world and thecomputer science world, we developed a language calledAbstract Accountability Language (AAL) that allows towrite obligations and accountability policies. Thislanguage is based on a formal logic called First OrderLinear Temporal Logic (FOTL) which allows to check thecoherence of the accountability policies and thecompliance between two policies. These policies aretranslated into a temporal logic called FO-DTL 3, which isassociated with a monitoring technique based on formularewriting. Finally, we developed a monitoring tool calledAccountability Monitoring (AccMon) which providesmeans to monitor accountability policies in the context ofa real system. These policies are based on FO-DTL 3logic and the framework can act in both centralized anddistributed modes and can run into on-line and off-linemodes.

La notion de gouvernance semble recouvrir des thèmes proches du terme «gouverner», de la prise de décision et de l’évaluation.La gouvernance d’entreprise propose une nouvelle conception du processus de décision, accordant toute sa place à la concertation entre les parties prenantes. Le délégué syndical intervient dans ce sens, en effet, il a une mission de revendication (par exemple concernant la hausse des salaires), il est l’interlocuteur du syndicat auprès de l’employeur, il négocie avec ce dernier les normes de l’entreprise (accords et conventions collectives)Encadrée par des lois assurant l'indispensable transparence, la gouvernance d'entreprise serait théoriquement le moyen d'assurer au mieux les intérêts multiples des acteurs concernés (salariés et employeurs).C’est la raison pour laquelle il parait opportun de faire un parallèle entre l’exercice de la gouvernance d’entreprise par les acteurs concernés et le respect de la vie privée des salariés.Ce parallèle entre vie privée et gouvernance de l’entreprise a notamment été mis en exergue avec l’affaire Novartis (6 octobre 2004).L’entreprise Novartis a mis en place en 1999 un code de bonne conduite pour rappeler certains principes éthiques, seulement ce texte a été complété en juillet 2004 par de surprenantes dispositions jugées attentatoires à la vie privée des salariés par le Tribunal de Nanterre. Ce code de conduite demande notamment aux salariés de Novartis " qu'ils consacrent tout leur temps et toute leur attention au travail de Novartis pendant les heures de travail habituelles... Le temps requis pour une occupation extérieure peut générer une baisse de la productivité ". En outre, le groupe estime que "le temps requis pour une occupation extérieure, qu'elle soit de type gouvernemental, politique ou bénévole, peut générer une baisse de la productivité et de l'efficacité d'un collaborateur créant ainsi un conflit d'intérêts" Aussi Novartis exige également " une autorisation préalable " de la direction pour ce type d'activités.Le tribunal des référés de Nanterre va rendre une décision qui va porter en outre sur le fond en jugeant que ces " alinéas sont susceptibles de nuire à la santé mentale des salariés et portent atteinte à la vie privée ".La direction ne fera finalement pas appel et soumettra au Comité de groupe ainsi qu'au comité d’hygiène, de sécurité et des conditions de travail une nouvelle version de son code éthique.La gouvernance d’entreprise peut donc être limitée par le respect de la vie privée des salariés.La vie privée est l'ensemble des activités d'une personne qui relève de son intimité par opposition à la vie publique.Il parait plus juste de mentionner un "droit à l'intimité de la vie privée".En effet, il s’agit d’un droit fondamental, proclamé par la loi, inscrit dans la déclaration des droits de l'homme de 1948 (article 12), la Convention européenne des Droits de l’Homme et des libertés fondamentales (article 8), à l’article 9 du Code civil et à l’article 226-1 du Code Pénal.Les composantes de la vie privée n'ont pas fait l'objet d'une définition ou d'une énumération limitative afin d'éviter de limiter la protection aux seules prévisions légales. Les tribunaux ont appliqué le principe de cette protection, au droit à la vie sentimentale et à la vie familiale, au secret relatif à la santé, au secret de la résidence et du domicile, et au droit à l'image. Par ailleurs, il convient de préciser que c’est le contrat de travail qui détermine les règles, obligations et devoirs de chacune des parties (l’employeur et le salarié), il ne peut concerner que le temps passé au travail.Des circonstances extérieures à la vie professionnelle et tenant à la vie privée du salarié ne peuvent être prises en considération, sauf si elles affectent la relation salariale. / The notion of governance seems to cover themes close to the term "to govern", of the grip of decision and the evaluation.It represents all the organs and the rules of decision, information (transparency) and supervision allowing the legal successors and the partners of a company, to see their respected interests and their voices in the functioning of this one.The governance of company proposes a new conception of the process of decision, granting all its place to the dialogue between the stakeholders.The union representative intervenes in this sense, indeed, he has a mission of claiming (for example concerning the increase in salaries), he is the interlocutor of the labor union(syndicate) with the employer, he negotiates with the latter the standards of the company (agreements and collective labor agreements)Framed by laws assuring the essential transparency, the governance of company would be in theory the way to assure at best the multiple interests of the actors concerned (employees and employers).It is the reason why it seemed convenient to draw a parallel between the exercise of the governance of company by the concerned actors and the respect for private life of the employees.The governance of company can be limited by the respect for private life of the employees.It is about a fundamental law, proclaimed by the law, registered in the bill of rights of 1948 (article 12), the European Convention on Human Rights and fundamental liberties (article 8), on the article 9 of the Civil code and on the article 226-1 of the Penal code.The components of the private life were not the object of a definition or a restrictive enumeration to avoid limiting the protection to the only legal forecasts. The courts applied the principle of this protection, in the right to life sentimental and in the family life, in the secret concerning the health, concerning the secret of the residence and the place of residence, and concerning the right(law) for the image.

Les mécanismes de réputation sont des outils très utiles pour inciter des utilisateurs ne se connaissant pas à se faire confiance, en récompensant les bons comportements et, inversement, en pénalisant les mauvais. Cependant, pour que la réputation des fournisseurs de service soit précise et robuste aux attaques, les mécanismes de réputation existants requièrent de nombreuses informations qui menacent la vie privée des utilisateurs; par exemple, il est parfois possible de traquer les interactions effectuées par les clients. Des mécanismes de réputation préservant aussi bien la vie privée des clients que celle des fournisseurs sont donc apparus pour empêcher de telles attaques. Néanmoins, pour garantir des propriétés fortes de vie privée, ces mécanismes ont dû proposer des scores de réputation imprécis, notamment en ne permettant pas aux clients de témoigner de leurs interactions négatives.Dans cette thèse, nous proposons un nouveau mécanisme de réputation distribué préservant la vie privée, tout en permettant aux clients d'émettre des témoignages négatifs. Une telle construction est possible grâce à des outils issus des systèmes distribués -- des tierces parties distribuées qui permettent de distribuer la confiance et de tolérer des comportements malveillants -- et de la cryptographie -- par exemple des preuves de connaissance à divulgation nulle de connaissance ou des signatures proxy anonymes. Nous prouvons de plus que ce mécanisme garantit les propriétés de vie privée et de sécurité nécessaires, et montrons par des analyses théoriques et pratiques que ce mécanisme est utilisable. / Reputation mechanisms are very powerful mechanisms to foster trust between unknown users, by rewarding good behaviors and punishing bad ones. Reputation mechanisms must guarantee that the computed reputation scores are precise and robust against attacks; to guarantee such properties, existing mechanisms require information that jeopardize users' privacy: for instance, clients' interactions might be tracked. Privacy-preserving reputation mechanisms have thus been proposed, protecting both clients' privacy and the providers' one. However, to guarantee strong privacy properties, these mechanisms provide imprecise reputation scores, particularly by preventing clients to testify about their negative interactions. In this thesis, we propose a new distributed privacy-preserving reputation mechanism allowing clients to issue positive as well as negative feedback. Such a construction is made possible thanks to tools from the distributed systems community -- distributed third parties that allow for a distribution of trust and that tolerate malicious behaviors -- as well as from the cryptographic one -- for instance zero-knowledge proofs of knowledge or anonymous proxy signatures. Furthermore, we prove that our mechanism guarantees the required privacy and security properties, and we show with theoretical and practical analysis that this mechanism is usable.

L’objet de ce travail est de démontrer que le droit des données personnelles ne se réduit pas au droit à la protection des données personnelles. En effet, il existe une thèse dominante au terme de laquelle le droit des données personnelles a pour objet exclusif la protection de la personne fichée et constitue, en tant que tel, un élément de la protection de la vie privée.Or, une telle lecture procède d’une isolation clinique de certaines dispositions essentielles au sein des instruments relatifs aux données personnelles. Le droit positif invalide cette thèse et révèle que ces normes poursuivent deux enjeux distincts. Le premier tient effectivement à la protection de la personne fichée et a à ce titre été isolé au sein d’un droit à la protection des données personnelles en droit de l’Union européenne. Le second tient dans l’usage sans entraves de l’informatique et implique la liberté de traiter des données personnelles. Au sein des instruments juridiques relatifs aux données personnelles, ces deux intérêts ne constituent pas deux objectifs de rang et d’intérêt égal juxtaposés l’un à côté de l’autre. Ils sont articulés et hiérarchisés. Le but premier de ces instruments est de garantir la liberté de traitement des données personnelles en tant qu’elle conditionne la liberté de l’usage de procédés informatiques. La protection des droits et libertés fondamentales des personnes fichées n’en constitue que la limite, étroitement subordonnée et circonscrite à ce but principal.De ce constat, il est possible de déduire que les instruments juridiques relatifs aux données personnelles constituent une même police administrative spéciale. Cette police a pour but de consacrer et d’aménager une liberté publique à ce jour innommée : la liberté de traitement des données personnelles. Elle a pour effet et non pour objet de protéger la personne fichée, non pas seulement parce que cette dernière serait titulaire d’un droit fondamental mais aussi et surtout au titre de la protection d’un ordre public spécial. / Data law cannot be reduced to data protection law. Data law instruments have two purposes. The main one is not data protection but the organization of the freedom of data treatment. Data protection is just the limit to this main purpose and cannot be thought in an independent manner.

L'objectif principal de la thèse est de proposer une méthode de recommandation prenant en compte la vie privée des utilisateurs ainsi que l'évolutivité du système. Pour atteindre cet objectif, une technique hybride basée sur le filtrage par contenu et le filtrage collaboratif est utilisée pour atteindre un modèle précis de recommandation, sous la pression des mécanismes visant à maintenir la vie privée des utilisateurs. Les contributions de la thèse sont trois : Tout d'abord, un modèle de filtrage collaboratif est défini en utilisant agent côté client qui interagit avec l'information sur les éléments, cette information est stockée du côté du système de recommandation. Ce modèle est augmenté d’un modèle hybride qui comprend une stratégie basée sur le filtrage par contenu. En utilisant un modèle de la connaissance basée sur des mots clés qui décrivent le domaine de l'article filtré, l'approche hybride augmente la performance de prédiction des modèles sans élever l’effort de calcul, dans un scenario du réglage de démarrage à froid. Finalement, certaines stratégies pour améliorer la protection de la vie privée du système de recommandation sont introduites : la génération de bruit aléatoire est utilisée pour limiter les conséquences éventuelles d'une attaque lorsque l'on observe en permanence l'interaction entre l'agent côté client et le serveur, et une stratégie basée sur la liste noire est utilisée pour s’abstenir de révéler au serveur des interactions avec des articles que l'utilisateur considère comme pouvant transgresser sa vie privée. L'utilisation du modèle hybride atténue l'impact négatif que ces stratégies provoquent sur la performance prédictive des recommandations. / The main objective of this thesis is to propose a recommendation method that keeps in mind the privacy of users as well as the scalability of the system. To achieve this goal, an hybrid technique using content-based and collaborative filtering paradigms is used in order to attain an accurate model for recommendation, under the strain of mechanisms designed to keep user privacy, particularly designed to reduce the user exposure risk. The thesis contributions are threefold : First, a Collaborative Filtering model is defined by using client-side agent that interacts with public information about items kept on the recommender system side. Later, this model is extended into an hybrid approach for recommendation that includes a content-based strategy for content recommendation. Using a knowledge model based on keywords that describe the item domain, the hybrid approach increases the predictive performance of the models without much computational effort on the cold-start setting. Finally, some strategies to improve the recommender system's provided privacy are introduced: Random noise generation is used to limit the possible inferences an attacker can make when continually observing the interaction between the client-side agent and the server, and a blacklisted strategy is used to refrain the server from learning interactions that the user considers violate her privacy. The use of the hybrid model mitigates the negative impact these strategies cause on the predictive performance of the recommendations.

Dans notre monde toujours plus connecté, les cartes à puce sont impliquées quotidiennementdans nos activités, que ce soit pour le paiement, le transport, le contrôle d’accès ou encore la santé.Ces cartes contiennent des informations personnelles liées aux faits et gestes de leur possesseur.Le besoin d’interpréter les données contenues dans les mémoires de ces cartes n’a jamais été aussiimportant. Cependant, sans les spécifications de l’application, il est difficile de connaître quellesinformations sont stockées dans la carte, leur emplacement précis, ou encore l’encodage utilisé.L’objectif de cette thèse est de proposer une méthode qui retrouve les informations stockéesdans les mémoires non volatile des cartes à puce. Ces informations peuvent être des dates (e.g.,date de naissance, date d’un événement) ou des informations textuelles (e.g., nom, adresse). Pourretrouver ces informations, un décodage exhaustif des données à l’aide de différentes fonctions dedécodage est possible. Malheureusement, cette technique génère de nombreux faux positifs. Unfaux positif apparaı̂t lorsqu’une fonction de décodage est appliquée sur des données qui ont étéencodées avec une fonction différente. Cette thèse s’appuie alors sur trois contributions exploitantles spécificités des cartes à puce pour éliminer ces faux positifs. La première contribution identifie lesobjets cryptographiques dans les mémoires non volatiles des cartes à puce afin de ne pas effectuer ledécodage sur ces données. Les deux autres contributions retrouvent respectivement des informationstextuelles et des dates dans ces mémoires. Afin de valider ces méthodes, elles sont chacune appliquéessur 371 mémoires de cartes à puce de la vie réelle. / In our increasingly connected world, smart cards are involved in any everyday activity, and theygather and record plenty of personal data. The need to interpret the raw data of smart card memoryhas never been stronger. However, without the knowledge of the specifications, it is difficult toretrieve what are the information stored, their location, and the encoding used to store them.The objective of this thesis is to propose a method retrieving the stored information in thenon-volatile memory of smart cards. This information include dates (e.g., birth date or event date)and textual information (e.g., name, address). In order to retrieve these information, it is possibleto perform an exhaustive decoding of the data with several decoding functions. Unfortunately,this technique generates a lot of false positives. Indeed, a false positive occurs when a decodingfunction is applied to data that have been encoded with another function. This thesis proposesthree contributions exploiting smart cards specificities to eliminate the false positives. The firstcontribution identifies cryptographic material in these non-volatile memories in order to preventthe false positives generated by the decoding of these cryptographic objects. The two otherscontributions retrieve respectively textual information and dates in these memories. In order tovalidate these methods, they are applied on 371 memory dumps of real-life smart cards.

Les bénéfices engendrés par les études statistiques sur les données personnelles des individus sont nombreux, que ce soit dans le médical, l'énergie ou la gestion du trafic urbain pour n'en citer que quelques-uns. Les initiatives publiques de smart-disclosure et d'ouverture des données rendent ces études statistiques indispensables pour les institutions et industries tout autour du globe. Cependant, ces calculs peuvent exposer les données personnelles des individus, portant ainsi atteinte à leur vie privée. Les individus sont alors de plus en plus réticent à participer à des études statistiques malgré les protections garanties par les instituts. Pour retrouver la confiance des individus, il devient nécessaire de proposer dessolutions de user empowerment, c'est-à-dire permettre à chaque utilisateur de contrôler les paramètres de protection des données personnelles les concernant qui sont utilisées pour des calculs.Cette thèse développe donc un nouveau concept d'anonymisation personnalisé, basé sur la généralisation de données et sur le user empowerment.En premier lieu, ce manuscrit propose une nouvelle approche mettant en avant la personnalisation des protections de la vie privée par les individus, lors de calculs d'agrégation dans une base de données. De cette façon les individus peuvent fournir des données de précision variable, en fonction de leur perception du risque. De plus, nous utilisons une architecture décentralisée basée sur du matériel sécurisé assurant ainsi les garanties de respect de la vie privée tout au long des opérations d'agrégation.En deuxième lieu, ce manuscrit étudie la personnalisations des garanties d'anonymat lors de la publication de jeux de données anonymisés. Nous proposons l'adaptation d'heuristiques existantes ainsi qu'une nouvelle approche basée sur la programmation par contraintes. Des expérimentations ont été menées pour étudier l'impact d’une telle personnalisation sur la qualité des données. Les contraintes d’anonymat ont été construites et simulées de façon réaliste en se basant sur des résultats d'études sociologiques. / The benefit of performing Big data computations over individual’s microdata is manifold, in the medical, energy or transportation fields to cite only a few, and this interest is growing with the emergence of smart-disclosure initiatives around the world. However, these computations often expose microdata to privacy leakages, explaining the reluctance of individuals to participate in studies despite the privacy guarantees promised by statistical institutes. To regain indivuals’trust, it becomes essential to propose user empowerment solutions, that is to say allowing individuals to control the privacy parameter used to make computations over their microdata.This work proposes a novel concept of personalized anonymisation based on data generalization and user empowerment.Firstly, this manuscript proposes a novel approach to push personalized privacy guarantees in the processing of database queries so that individuals can disclose different amounts of information (i.e. data at different levels of accuracy) depending on their own perception of the risk. Moreover, we propose a decentralized computing infrastructure based on secure hardware enforcing these personalized privacy guarantees all along the query execution process.Secondly, this manuscript studies the personalization of anonymity guarantees when publishing data. We propose the adaptation of existing heuristics and a new approach based on constraint programming. Experiments have been done to show the impact of such personalization on the data quality. Individuals’privacy constraints have been built and realistically using social statistic studies

Désormais, l'analyse des scènes denses s'impose incontestablement comme une tâche importante pour contrôler et gérer les foules. Notre recherche a pour objectifs d'apporter des solutions à l'estimation de la densité de la foule et de prouver l'utilité de cette estimation comme préalable pour d'autres applications. Concernant le premier objectif, afin de cerner les difficultés de la détection de personnes dans une foule, on se focalise sur l'estimation de la densité basée sur un niveau d'analyse bas. Dans un premier temps, on démontre que nos approches sont plus adéquates que les méthodes de l’état de l’art que ce soit pour compter les individus ou pour estimer le niveau de la foule. Dans un second temps, nous proposons une approche innovante dans laquelle une estimation locale au niveau des pixels remplace l'estimation au niveau global de la foule ou le nombre des personnes. Elle est basée sur l’utilisation des suivis de caractéristiques visuelles dans une fonction de densité. Notre recherche a également pour objectif d'utiliser la densité comme information supplémentaire pour affiner d'autres tâches. D'abord, nous avons utilisé la mesure de la densité qui comporte une description pertinente à la répartition spatiale des individus afin d'améliorer leur détection et leur suivi dans les foules. Ensuite, en prenant en compte la notion de la protection de la vie privée, nous ajustons le niveau de floutage en fonction de la densité de la foule. Enfin, nous nous appuyons sur l’estimation locale de la densité ainsi que sur le mouvement en tant qu'attributs pour des applications de haut niveau telles que la détection des évolutions et la reconnaissance des événements. / Crowd analysis has recently emerged as an increasingly important problem for crowd monitoring and management in the visual surveillance community. In this thesis, our objectives are to address the problems of crowd density estimation and to investigate the usefulness of such estimation as additional information to other applications. Towards the first goal, we focus on the problems related to the estimation of the crowd density using low level features in order to avert typical problems in detection of high density crowd. We demonstrate in this dissertation, that the proposed approaches perform better than the baseline methods, either for counting people, or alternatively for estimating the crowd level. Afterwards, we propose a novel approach, in which local information at the pixel level substitutes the overall crowd level or person count. It is based on modeling time-varying dynamics of the crowd density using sparse feature tracks as observations of a probabilistic density function. The second goal is to use crowd density as additional information to complement other tasks related to video surveillance in crowds. First, we use the proposed crowd density measure which conveys rich information about the local distributions of persons to improve human detection and tracking in videos of high density crowds. Second, we investigate the concept of crowd context-aware privacy protection by adjusting the obfuscation level according to the crowd density. Finally, we employ additional information about the local density together with regular motion patterns as crowd attributes for high level applications such as crowd change detection and event recognition.

La société de l’information dans laquelle nous vivons repose notamment sur notre capacité à échanger des informations de façon sécurisée. Ces échanges sécurisés sont réalisés au moyen de protocoles cryptographiques. Ils explicitent comment les différents agents communicants doivent se comporter et exploitent des primitives cryptographiques (e.g. chiffrement, signature) pour protéger les échanges. Étant donné leur prédominance et leur importance, il est crucial de s’assurer que ces protocoles accomplissent réellement leurs objectifs. Parmi ces objectifs, on trouve de plus en plus de propriétés en lien avec la vie privée (e.g. anonymat, non-traçabilité). Malheureusement, les protocoles développés et déployés souffrent souvent de défauts de conception entraînant un cycle interminable entre découverte d’attaques et amélioration des protocoles.Pour en sortir, nous prônons l’analyse mécanisée de ces protocoles par des méthodes formelles qui, via leurs fondements mathématiques, permettent une analyse rigoureuse apportant des garanties fortes sur la sécurité attendue. Parmi celles-ci, la vérification dans le modèle symbolique offre de grandes opportunités d’automatisation. La plupart des propriétés en lien avec la vie privée sont alors modélisées par l’équivalence entre deux systèmes. Toutefois, vérifier cette équivalence est indécidable dans le cas général. Deux approches ont alors émergé. Premièrement, pour un nombre borné de sessions d’un protocole, il est possible de symboliquement explorer toutes ses exécutions possibles et d’en déduire des procédures de décision pour l’équivalence. Deuxièmement, il existe des méthodes de semi-décision du problème dans le cas général qui exploitent des abstractions, notamment en considérant une forme forte d’équivalence.Nous avons identifié un problème majeur pour chacune des deux méthodes de l’état de l’art qui limitent grandement leur impact en pratique. Premièrement, les méthodes et outils qui explorent symboliquement les exécutions souffrent de l’explosion combinatoire du nombre d’états, causée par la nature concurrente des systèmes étudiés. Deuxièmenent, dans le cas non borné, la forme forte d’équivalence considérée se trouve être trop imprécise pour vérifier certaines propriétés telle que la non traçabilité, rendant cette approche inopérante pour ces propriétés.Dans cette thèse, nous proposons une solution à chacun des problèmes. Ces solutions prennent la forme de contributions théoriques, mais nous nous efforçons de les mettre en pratique via des implémentations afin de confirmer leurs impacts pratiques qui se révèlent importants.Tout d’abord, nous développons des méthodes de réduction d’ordres partiels pour réduire drastiquement le nombre d’états à explorer tout en s’assurant que l’on ne perd pas d’attaques. Nos méthodes sont conçues pour le cadre exigeant de la sécurité et sont prouvées correctes et complètes vis-à-vis de l’équivalence. Nous montrons comment elles peuvent s’intégrer naturellement dans les outils existants. Nous prouvons la correction de cette intégration dans un outil et proposons une implémentation complète. Finalement, nous mesurons le gain significatif en efficacité ainsi obtenu et nous en déduisons que nos méthodes permettent l’analyse d’un plus grand nombre de protocoles.Ensuite, pour résoudre le problème de précision dans le cas non-borné, nous proposons une nouvelle démarche qui consiste à assurer la vie privée via des conditions suffisantes. Nous définissons deux propriétés qui impliquent systématiquement la non-traçabilité et l’anonymat et qui sont facilement vérifiables via les outils existants (e.g. ProVerif). Nous avons implémenté un nouvel outil qui met en pratique cette méthode résolvant le problème de précision de l’état de l’art pour une large classe de protocoles. Cette nouvelle approche a permis les premières analyses de plusieurs protocoles industriels incluant des protocoles largement déployés, ainsi que la découverte de nouvelles attaques. / The information society we belong to heavily relies on secure information exchanges. To exchange information securely, one should use security protocols that specify how communicating agents should behave notably by using cryptographic primitives (e.g. encryption, signature). Given their ubiquitous and critical nature, we need to reach an extremely high level of confidence that they actually meet their goals. Those goals can be various and depend on the usage context but, more and more often, they include privacy properties (e.g. anonymity, unlinkability). Unfortunately, designed and deployed security protocols are often flawed and critical attacks are regularly disclosed, even on protocols of utmost importance, leading to the never-ending cycle between attack and fix.To break the present stalemate, we advocate the use of formal methods providing rigorous, mathematical frameworks and techniques to analyse security protocols. One such method allowing for a very high level of automation consists in analysing security protocols in the symbolic model and modelling privacy properties as equivalences between two systems. Unfortunately, deciding such equivalences is actually undecidable in the general case. To circumvent undecidability, two main approaches have emerged. First, for a bounded number of agents and sessions of the security protocol to analyse, it is possible to symbolically explore all possible executions yielding decision procedures for equivalence between systems. Second, for the general case, one can semi-decide the problem leveraging dedicated abstractions, notably relying on a strong form of equivalence (i.e. diff-equivalence).The two approaches, i.e. decision for the bounded case or semi-decision for the unbounded case, suffer from two different problems that significantly limit their practical impact. First, (symbolically) exploring all possible executions leads to the so-called states space explosion problem caused by the concurrency nature of security protocols. Concerning the unbounded case, diff-equivalence is actually too imprecise to meaningfully analyse some privacy properties such as unlinkability, nullifying methods and tools relying on it for such cases.In the present thesis, we address those two problems, going back and forth between theory and practice. Practical aspects motivate our work but our solutions actually take the form of theoretical developments. Moreover, we make the effort to confirm practical relevance of our solutions by putting them into practice (implementations) on real-world case studies (analysis of real-world security protocols).First, we have developed new partial order reduction techniques in order to dramatically reduce the number of states to explore without loosing any attack. We design them to be compatible with equivalence verification and such that they can be nicely integrated in frameworks on which existing procedures and tools are based. We formally prove the soundness of such an integration in a tool and provide a full implementation. We are thus able to provide benchmarks showing dramatic speedups brought by our techniques and conclude that more protocols can henceforth be analysed.Second, to solve the precision issue for the unbounded case, we propose a new methodology based on the idea to ensure privacy via sufficient conditions. We present two conditions that always imply unlinkability and anonymity that can be verified using existing tools (e.g. ProVerif). We implement a tool that puts this methodology into practice, hence solving the precision issue for a large class of protocols. This novel approach allows us to conduct the first formal analysis of some real-world protocols (some of them being widely deployed) and the discovery of novel attacks.