Mes travaux de doctorat ont porté sur la certification de programmes impératifs utilisés dans des applications critiques. Les certificats établissent la validité des propriétés sémantiques des programmes et sont produits sous forme de preuves déductives vérifiables par machine. Le défi relevé dans cette thèse est d'automatiser la construction des preuves de correction de programmes. Nous avons suivie l'approche de Floyd-Hoare pour prouver que les propriétés sémantiques sont des invariants du programme et nous avons utilisé le le système Coq pour vérifier la validité des preuves. On considére ici le cas où les propriétés sémantiques sont calculées par des analyseurs statiques de programmes qui s'appuient sur la théorie de l'interprétation abstraite. Nous proposons une méthode d'instrumentation des analyseurs statiques de programmes afin de leur faire générer automatiquement un certificat pour chaque propriété sémantique calculée. L'instrumentation consiste à associer à certaines fonctions d'un analyseur statique des patrons de preuve qui à l'exécution généreront les certificats. De tels analyseurs instrumentés ne sont pas pour autant certifiés puisque leur correction pour toutes leurs entrées possibles n'est pas garantie, néanmoins ils sont capables de justifier par une preuve formelle la correction du résultat de chacun de leurs calculs. Bien sûr, si pour une entrée possible l'exécution de l'analyseur est boguée le résultat sera erroné et la justification produite ne sera pas une preuve valide; elle sera rejettée par le vérificateur de preuves. Cette approche permet de certifier avec un très haut-niveau de confiance (celui du vérificateur de preuves) les résultats d'outils existants, même à l'état de prototypes. Pour que l'instrumentation soit applicable en pratique, nous avons cherché à limiter le nombre de fonctions à instrumenter. Nous avons dégagé un ensemble restreint de fonctions, commun à tout analyseur, à instrumenter pour qu'un analyseur existant devienne un outil de certification automatique. Nous avons appliqué cette technique d'instrumentation à un analyseur de programmes manipulant des tableaux qui s'appuie sur des domaines abstraits non triviaux. Cet analyseur calcule des propriétés sur le contenu des tableaux manipulés par les programmes et, grâce à notre instrumentation, génère désormais des certificats vérifiables par Coq attestant de la validité des propriétés découvertes par l'analyse statique. Nous montrons enfin comment utiliser cet analyseur instrumenté pour certifier un protocole de communication pour systèmes multi-tâches destiné à l'avionique. La garantie de la correction des programmes est cruciale dans le domaine des systèmes embarqués. Face aux coûts et la durée d'une procédure de certification formelle, le développement d'outils automatiques de certification représente un enjeu économique majeur. La transformation, par instrumentation, d'outils d'analyses existants en outils de certification est une réponse possible qui évite la certification des outils d'analyse.

Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées

Dans cette th ese, nous proposons et utilisons de nouvelles briques conduisant a des protocoles e caces dans le cadre d'une approche modulaire de la cryptographie. Tout d'abord dans un contexte non-interactif en s'appuyant sur les preuves Groth-Sahai, puis avec des interactions en permettant aux Smooth Projective Hash Functions de g erer de nouveaux langages. Dans un premier temps cette th ese s'appuie sur la m ethodologie introduite par Groth et Sahai pour des preuves de connaissance non-interactives pour d evelopper divers protocoles de signatures de groupe dans le mod ele standard, puis de signatures en blanc. Pour cela, nous proposons un syst eme permettant de signer un chi r e de mani ere telle que, sous r eserve de connaissance d'un secret ind ependant du protocole de signature, il soit possible de retrouver une signature sur un clair. Cette approche nous permet entre autre de proposer un protocole de signatures en blanc avec un nombre optimal d'interactions a la n duquel le demandeur peut utiliser une signature usuelle et ce sous des hypoth eses classiques dans le mod ele standard. Ensuite nous proposons une nouvelle m ethodologie pour faire des preuves implicites de connaissance dans un contexte interactif sans oracle al eatoire. Pour cela nous utilisons les smooth projective hash functions, dans un premier temps pour faire des Oblivious Signature-Based Envelopes, puis dans des protocoles d'authenti cation et de mise en accord de cl es. Ce faisant nous pr ecisons la notion de langage, et elargissons grandement le spectre des langages pouvant ^etre trait es a l'aide de ces SPHF. Gr^ace a ce r esultat nous introduisons le concept de LAKE (Language Authenticated Key Exchange) ou encore Echange de cl es authenti e par un langage : un moyen pour deux utilisateurs de se mettre d'accord sur une cl e si chacun poss ede un secret v eri ant une contrainte esp er ee par l'autre. Nous montrons alors comment instancier plusieurs protocoles d' echange de cl e sous ce regard plus effi cacement qu'avec les techniques actuelles, et nous prouvons la s ecurit e de nos instanciations dans le mod ele UC sous des hypoth eses usuelles.

Cette thèse présente une coopération entre l'assistant de preuve Coq et certains prouveurs externes basée sur l'utilisation de traces de preuves. Nous étudions plus particulièrement deux types de prouveurs pouvant renvoyer des certicats : d'une part, les réponses des prouveurs SAT et SMT peuvent être vériées en Coq afin d'augmenter à la fois la confiance qu'on peut leur porter et l'automatisation de Coq ; d'autre part, les théorèmes établis dans des assistants de preuves basés sur la Logique d'Ordre Supérieur peuvent être exportés en Coq et re-vérifiés, ce qui permet d'établir des preuves formelles mêlant ces deux paradigmes logiques. Cette étude a abouti à deux logiciels : SMTCoq, une coopération bi-directionnelle entre Coq et des prouveurs SAT/SMT, et HOLLIGHTCOQ, un outil important les théorèmes de HOL Light en Coq. L'architecture de chacun de ces deux développements a été pensée de manière modulaire et efficace, en établissant une séparation claire entre trois composants: un encodage en Coq du formalisme de l'outil externe qui est ensuite traduit avec soin vers des termes Coq, un vérificateur certifié pour établir les preuves, et un pré-processeur écrit en Ocaml traduisant les traces venant de prouveurs différents dans le même format de certicat. Grâce à cette séparation, un changement dans le format de traces n'affecte que le pré-processeur, sans qu'il soit besoin de modier du code ou des preuves Coq. Un autre composant essentiel pour l'efficacité et la modularité est la réflexion calculatoire, qui utilise les capacités de calcul de Coq pour établir des preuves à la fois courtes et génériques à partir des certificats.

Les méthodes formelles ont atteint un degré de maturité conduisant à la conception de systèmes de preuves généralistes, permettant à la fois de vérifier la correction de systèmes logiciels complexes ou de formaliser des mathématiques avancées. Mais souvent, l'accent est mis davantage sur la facilité du raisonnement sur les programmes plutôt que sur leur exécution efficace. L'antagonisme entre ces deux aspects est particulièrement sensible pour les algorithmes de calcul formel, dont la correction repose habituellement sur des concepts mathématiques élaborés, mais dont l'efficacité pratique est une préoccupation importante. Cette thèse développe des approches à l'étude formelle et l'exécution efficace de programmes en théorie des types, et plus précisément dans l'assistant à la preuve \coq{}. Dans un premier temps, nous présentons un environnement d'exécution permettant de compiler en code natif de tels programmes tout en conservant la généralité et l'expressivité du formalisme. Puis, nous nous intéressons aux représentations de données et plus particulièrement au lien formellement vérifié et automatisé entre représentations adaptées aux preuves ou au calcul. Ensuite, nous mettons à profit ces techniques pour l'étude d'algorithmes en algèbre linéaire, comme le produit matriciel de Strassen, le procédé d'élimination de Gauss ou la mise en forme canonique de matrices, dont notamment la forme de Smith pour les matrices sur un anneau euclidien. Enfin, nous ouvrons le champ des applications à la formalisation et au calcul certifié des groupes d'homologie de complexes simpliciaux issus d'images numériques.

Les interventions visant l'arrêt du tabac ont réalisé des progrès importants. Pourtant, des facteurs minorent le maintien de l'arrêt du tabac à long terme, en particulier l'existence d'un trouble dépressif. Cette thèse étudie la contribution de la pratique d'activité physique en tant que facteur protecteur de la rechute dans le cadre du sevrage tabagique. Les études longitudinales 1 et 2 explorent l'impact de l'activité physique sur la rechute tabagique à long terme, chez des fumeurs avec ou sans trouble dépressif. L'étude 1 retrouve un effet protecteur de l'interaction antidépresseur - activité physique sur la rechute chez des fumeurs tout venant (n= 227). L'étude 2 met en exergue le rôle protecteur de l'activité physique chez des fumeurs touchés par un trouble dépressif (n= 133) ainsi que le niveau d'éducation, la prise d'anxiolytiques et d'antidépresseurs, ainsi que les tentatives d'arrêt précédentes. L'étude 3 évalue l'efficacité d'un programme d'activité physique adapté couplé à du conseil comme traitement adjuvant de l'arrêt du tabac chez des fumeurs touchés par un trouble dépressif. Cet essai clinique randomisé contrôlé (n = 70) a été réalisé au sein du CHRU de Montpellier. Le critère de jugement principal est l'abstinence continue trois mois après le début de l'intervention. L'analyse en intention de traiter souligne une différence en fin de programme (OR = 0.14 ; 95% CI .02 - .72 ; p = .018) et une différence non significative à trois mois (OR = 0.87 ; 95% CI .62 – 1.21 ; p = .08).Pour conclure, nous faisons l'état des mécanismes testés empiriquement expliquant l'effet de l'activité physique sur la consommation de tabac et la dépression. Nous proposons des pistes méthodologiques pour construire des modélisations et des interventions dans le domaine de la santé à partir d'une approche transdisciplinaire. / Current depressive disorders are associated with a lower likelihood of quitting smoking and with greater likelihood of smoking relapse.The aim of this thesis project was to study the protective role of physical activity on relapse rate after a smoking-cessation program. Studies 1 and 2 have explored the role of physical activity on relapse at long term in smokers with and without depressive disorders. First study has shown a significant interaction between antidepressant and physical activity as protecteur factor on relapse (n= 227) among smokers recruited at the smoking-cessation unit of Montpellier University Hospital. Second study has confirmed that physical activity was a protector factor on relapse in smokers with depressive disorders. Furthermore, antidepressants, anxiolytics, level of education, and number of attempts to quit were associated with relapse. The efficacy of exercise intervention and counseling as an adjuvant therapy in smoking cessation for smokers with current depressive disorders (n= 70) has been investigated in third study. Compared with control subjects, exercise subjects achieved significantly higher levels of continuous abstinence at the end of treatment (OR = 0.14 ; 95% CI .02 - .72 ; p = .018) while results were not significant at 3 months following treatment (OR = 0.87 ; 95% CI .62 – 1.21 ; p = .08). We have also reviewed the current literature investigating the mechanisms between exercise-depression and exercise-smoking. Methodological and transdisciplinary approaches are proposed to developp future studies.

I. Introduction01. La caractéristique d’un État de droit est que « l’ensemble des autorités politiques, administratives, centrales et locales, agit en se conformant effectivement aux règles de droit en vigueur et dans lequel tous les individus bénéficient également de libertés publiques et de garanties procédurales et juridictionnelles. » De la réponse apportée par notre société à la sanction procédurale de la violation des formalités instaurées en procédure pénale dépend directement la définition concrète que nous retenons de la notion d’État de droit. La question est donc de savoir si en acceptant l’utilisation d’une preuve obtenue par l’autorité malgré la violation de la loi, l’État de droit dispose de la qualité dont il se targue :garantir que les poursuites sont menées conformément au droit. 02. Le 14 octobre 2003, dans un arrêt dit « Antigone », la Cour de cassation de Belgique, section néerlandophone, a réformé une jurisprudence constante de plus d'un siècle, inversant le principe de l'irrecevabilité des preuves irrégulièrement obtenues. Elle a posé le principe d’admissibilité de la preuve irrégulière, depuis lors coulé en force de loi à l'article 32 du Titre préliminaire du Code de procédure pénale :« La nullité d'un élément de preuve obtenu irrégulièrement n'est décidée que si :– le respect des conditions formelles concernées est prescrit à peine de nullité, ou ;– l'irrégularité commise a entaché la fiabilité de la preuve, ou ;– l'usage de la preuve est contraire au droit à un procès équitable. »Des sous-critères sont retenus par la Cour de cassation pour apprécier l’équité du procès, en particulier celui de la proportionnalité entre la gravité de l’infraction et la gravité de l’irrégularité. 03. Dans un premier temps, la réflexion est portée sur le caractère convaincant ou non du système actuel. Est-il justifié à long terme ou les craintes formulées quant à un allègement des garanties, en particulier, contre les immixtions dans la vie privée par les autorités policières et judiciaires relèvent-elles de la rhétorique d’intellectuels éloignés des soucis réels des citoyens ?Permet-il, pour reprendre un adjectif discuté d’un récent arrêt de la Cour de cassation, de rendre une justice idéale ?La réflexion est prolongée par un examen détaillé de la jurisprudence de la Cour européenne des droits de l'Homme.Dans un deuxième temps de réflexion, il est procédé à une analyse de droit comparé avec les systèmes français, anglais, américain, allemand, grec, espagnol, irlandais, italien, turc, suisse, hollandais, canadien, écossais, néo-zélandais et australien. L'intérêt de cette comparaison est de trouver inspiration dans ces autres solutions nationales, mais aussi de vérifier s'il ne se dégage pas un consensus international sur le sort procédural à réserver aux preuves irrégulièrement obtenues.Enfin, il est proposé, sur la base de ces réflexions, un système national d'exclusion des preuves irrégulières.II. La pertinence de la règle Antigone04. La Cour de cassation a manifestement modifié sa jurisprudence suite à l’évolution d’une partie de la doctrine du nord du Pays. Si une certaine doctrine francophone l’avait également anticipée, aucun auteur n’avait pris position en faveur de l’admissibilité de la preuve irrégulière. Cette véritable révolution jurisprudentielle n’a pas été faite en symbiose entre les deux sections de la Cour de cassation et jamais la question n’a été soumise à une séance plénière. En définitive, la section française de la Cour de cassation s’est ralliée à la position de la section néerlandophone le 2 mars 2005 et le principe est aujourd’hui consacré à l’article 32 du Titre préliminaire du Code de procédure pénale. 05. L’élaboration de ces nouveaux principes n’est pas née d’une réflexion aboutie sur la pertinence d’une nouvelle approche, cohérente, du sort des preuves irrégulières, mais consiste avant tout dans le rejet de l’ancien système, qui consistait à exclure les preuves obtenues en violation d’une formalité substantielle. Non seulement le rejet du système précédent est le fruit d’affirmations peu ou prou étayées scientifiquement, mais en outre, le fondement des nouveaux principes n’a jamais été exposé. Ces principes ont été imposés, sans la moindre justification, sans motivation du système ainsi choisi.Depuis l’application des principes Antigone, aucune sanction procédurale n’a été prononcée en raison d’une violation d’une formalité protectrice de la vie privée. 06. En inversant le principe, la Cour de cassation met en péril le respect effectif des droits et libertés individuels. Le législateur s’est trompé en ne percevant pas que ce débat-là touchait à la notion même d’État de droit et appelait une réflexion approfondie. La seule solution raisonnable consiste à réaffirmer le principe d’exclusion de la preuve irrégulière. III. La jurisprudence de la Cour européenne des droits de l’Homme07. Lorsqu’il est question d’une preuve obtenue en violation de l’article 3 de la Convention ou d’une atteinte aux droits de la défense, le principe demeure l’exclusion de la preuve irrégulière sous couvert de l’atteinte au droit à un procès équitable.La Cour européenne des droits de l’homme a validé la jurisprudence de la Cour de cassation lorsqu’il est question d’une preuve obtenue en violation de l’article 8. Certes, la Cour européenne des droits de l’homme a considéré que l’application de cette jurisprudence n’impliquait pas de violation du droit à un procès équitable, mais en aucun cas, cette juridiction n’est habilitée à trancher d’autres questions. C’est en tout cas la limite qu’elle s’est imposée. Elle est habilitée à constater la violation de l’article 8 de la Convention, mais se refuse à établir un lien automatique entre une violation de cette disposition et la notion de droit à un procès équitable.Et pour cause, le droit à un procès équitable tend essentiellement à garantir les droits de la défense, l’impartialité du juge, le respect de la présomption d’innocence. Mais il ne s’agit pas d’une prolongation de l’article 8. En cette matière, c’est le législateur qui fait loi et non la jurisprudence, qu’elle soit de la Cour européenne des droits de l’homme ou de la Cour de cassation. Et c’est bien là le paradoxe. Le pouvoir judiciaire a espéré qu’un choix réfléchi soit effectué en cette matière et lorsque les parlementaires ont abordé le débat, ils en ont conclu qu’il appartenait au pouvoir judiciaire de faire évoluer la jurisprudence et se sont limités à acter la jurisprudence en l’état, et ce a minima.IV. L’analyse de droit comparéA. L’absence d’uniformité au sein de l’Union européenne08. L’analyse des systèmes nationaux précités met en évidence l’absence d’uniformisation des règles d’admissibilité ou d’exclusion des preuves irrégulières au sein l’Union européenne, et la très grande disparité de réactions nationales des pays membres. Ce constat est tempéré par les exceptions prévues dans les régimes favorables au principe d’exclusion de la preuve irrégulière, et à celles apparues au sein des régimes d’admissibilité de la preuve irrégulière. 1. Les divergences09. L’Angleterre assume traditionnellement le principe d’admissibilité de la preuve irrégulière, le rôle du juge n’étant pas de sanctionner les actes posés par les autorités chargées de l’enquête. Il peut, aux termes de l’article 78 du PACE, décider d’écarter la preuve si son usage est contraire à l’équité du procès, de sorte que les irrégularités liées à la violation du droit à la vie privée n’entraînent pas d’exclusion de la preuve. L’article 76 du PACE impose des règles différentes pour l’admissibilité de l’aveu. L’Ecosse, malgré un système d’exclusion relativement ferme, connaît une évolution favorable au rapprochement avec le système anglais, le critère de l’équité du procès prédominant.La Belgique a, depuis 2003, inversé la règle de l’exclusion vers celle de l’admissibilité. Le juge pénal doit admettre la preuve, sauf s’il constate que son admissibilité serait en contradiction avec l’équité du procès. Des sous-critères sont retenus par la Cour de cassation, en particulier celui de la proportionnalité entre la gravité de l’infraction et la gravité de l’irrégularité. Les cas d’exclusion des preuves en raison d’une atteinte au droit à la vie privée sont quasi inexistants. Le juge hollandais n’est pas contraint de procéder à l’exclusion de la preuve. Il en a la possibilité, mais non l’obligation. En cela, il se rapproche du système anglais. Le système néerlandais s’en éloigne par contre en ce que l’équité de la procédure n’est pas le critère clef soumis au juge. Les critères sont ceux de l’intérêt que sert le droit violé, de la gravité de la violation constatée et du dommage causé par la violation. S’il n’existe pas de cas d’exclusion automatique en l’hypothèse d’une violation du droit à la vie privée, le juge peut, sur la base de ces critères, décider d’exclure la preuve, à l’inverse des conséquences concrètes du recours au critère d’équité en droits anglais et belge. Le système hollandais se distingue encore des autres par la possibilité pour le juge de décider d’autres sanctions procédurales, telle qu’une diminution de la peine. Aucun autre pays de l’Union Européenne, soumis à la présente analyse, ne prévoit une diminution de peine en cas de violation d’un droit fondamental. Enfin, tout comme le système français, l’irrégularité doit, aux Pays-Bas, avoir causé un grief à celui qui s’en prévaut pour qu’une sanction procédurale soit prononcée par le juge pénal.La France fonde ses règles sur le principe de la nullité des preuves obtenues en violation des formalités substantielles, ce qui la distingue des systèmes anglais, belge et hollandais .Le principe prévaut également en cas de violation du droit à la vie privée. Par contre, le principe selon lequel il ne peut y avoir de nullité sans grief est consacré par la loi, à tout le moins pour les cas de nullités relatives, ce qui converge avec le système néerlandais. Dans leur appréciation, les juges tiennent compte du critère de proportionnalité. Les règles espagnoles se rapprochent des françaises, le principe étant l’exclusion de la preuve et la règle d’absence d’exclusion à défaut de grief étant emprunté au système américain. Une différence est faite entre la preuve directement obtenue par la violation constatée et les preuves dérivées. Pour décider, ou non, de l’exclusion de ces dernières, les cours et tribunaux ont recours au critère de proportionnalité.Ce critère de proportionnalité n’est par contre pas retenu, in se, en Allemagne ,en Irlande et en Grèce. L’Allemagne connaît des règles d’exclusion, notamment en cas d’atteinte à la vie privée. Les cours et tribunaux vérifient s’il y a une atteinte concrète aux droits fondamentaux. Les preuves dérivées de celles obtenues en violation du droit au silence sont exclues et ne peuvent pas être utilisées à charge en cas de violation du droit à la vie privée.En Irlande, la violation d’un droit constitutionnel implique automatiquement l’exclusion de la preuve irrégulière. Le principe d’inviolabilité du domicile étant constitutionnellement garanti, sa transgression est nécessairement sanctionnée par l’exclusion de la preuve. Dans les autres cas, l’exclusion est une possibilité pour le juge pénal, qui appréciera notamment le caractère délibéré ou non de l’irrégularité. Enfin, la Constitution et le Code de procédure pénale grecs prévoient des règles d’exclusion très strictes, en ce compris des preuves dérivées et quel que soit le droit fondamental auquel il est porté atteinte. Sous un autre angle, tous les États ne privilégient pas, au-delà de ce qu’impose la jurisprudence de la Cour européenne des droits de l’Homme, l’exclusion des preuves obtenues en violation des droits de la défense, et en particulier, du droit de ne pas être contraint de s’auto-incriminer. Seuls l’Allemagne et la Grèce semblent avoir pris une voie claire en ce sens. En conclusion, aucun des systèmes ne présente une parfaite similitude, et là où certaines règles sont communes, d’autres s’opposent. On trouve en outre, au sein de l’Union Européen, des systèmes apparemment drastiquement opposés, tels que l’Angleterre et la Grèce.2. Les exceptions qui atténuent ces divergences10. Dans son ouvrage « La légalité de la preuve dans l’espace pénal européen » ,le Docteur Marie Marty relativise ces différences en raison de la tendance générale à admettre la preuve illégalement ou irrégulièrement recueillie .L’auteur conclut l’analyse du déclin de la légalité de la preuve par le constat d’une cruelle similitude entre ces systèmes :« l’incapacité des législateurs et juridictions nationaux d’établir un régime de recevabilité de la preuve cohérent, soucieux des droits fondamentaux des individus et adapté aux nécessités répressives contemporaines. » L’auteure précise néanmoins que les règles en matière de sanction des preuves irrégulières ne seront pas uniformisées à bref délai de l’espace pénal européen. Tout comme la Cour européenne des droits de l’homme, les institutions européennes se refusent à s’immiscer directement dans la question de la recevabilité de la preuve pénale, ce débat étant réservé aux droits nationaux.11. Cette appréciation nous paraît devoir être nuancée. Elle est essentiellement fondée sur la comparaison entre trois systèmes, l’Angleterre, la Belgique et la France. Or, les divergences restent profondes avec d’autres pays, et en particulier avec l’Allemagne, l’Irlande ou encore la Grèce. Une unanimité se manifeste à tout le moins. Tous les pays de l’Union Européenne excluent, par principe, les preuves recueillies en violation de l’article 3 de la Convention. Cette circonstance est évidente dès lors que tous les pays de l’Union sont membres du Conseil de l’Europe et que cette exclusion découle de la jurisprudence de la Cour européenne des droits de l’Homme, sous les réserves exprimées dans l’affaire Gäfgen c. Allemagne. Il en va de même en cas de provocation policière et pour les mêmes raisons. Cette position est imposée par la position adoptée par la Cour européenne des droits de l’Homme, tout comme pour l’atteinte au droit de ne pas s’auto-incriminer.Au-delà de ces points de convergence, les approches nationales diffèrent fondamentalement et en particulier en cas d’atteinte à la vie privée. 12. Enfin, en raison des exceptions retenues dans les systèmes nationaux aux principes, d’admissibilité ou d’exclusion des preuves irrégulières, la plupart des systèmes tendent à se rapprocher. L’Angleterre a évolué vers des cas d’exclusion, tandis que plusieurs pays privilégiant l’exclusion ont évolué vers une plus grande admissibilité. C’est indiscutablement le cas de la Belgique, mais c’est aussi ce que nous avons constaté à l’analyse des systèmes français et hollandais. C’est encore le cas, dans une moindre mesure, des règles écossaises et espagnoles. L’évolution reste néanmoins plus difficile à appréhender en Allemagne et en Irlande, tandis qu’elle semble ne pas avoir lieu en Grèce. B. L’absence de cohérence entre les pays de même tradition juridique13. Les différences d’approche ne peuvent pas non plus être expliquées par les traditions anglo-saxonnes ou continentales. Malgré une volonté d’uniformité, le système anglais et gallois – et, dans une moindre mesure, le système écossais, diffère fondamentalement quant à son principe d’admissibilité de la preuve irrégulière des systèmes américains, australiens, canadiens, irlandais et néo-zélandais. Les États-Unis retiennent une exclusion de principe tandis que les autres privilégient une approche concrète du juge sur la base de critères, notamment de proportionnalité. C. Le fondement du système14. Pour quatre des seize pays analysés, il ne nous a pas été possible de disposer des sources suffisantes pour répondre à cette question. Il s’agit de la Turquie, de l’Ecosse, de l’Australie et de la Nouvelle-Zélande. La comparaison est donc limitée, sur ce point, à douze pays.Quatre pays privilégient, en théorie, la protection des droits fondamentaux et libertés individuelles, non limités à ceux de l’accusé. Il s’agit de la Suisse, de l’Espagne, de la Grèce, de l’Allemagne et de l’Irlande .L’Italie peut y être ajouté, faisant prévaloir le principe de légalité. Il en va de même pour le Canada, la Cour suprême retenant une interprétation favorable à la protection des droits et libertés considérés de manière générale sous couvert du principe d’intégrité de la justice. En d’autres termes, six pays sur douze, soit la moitié, privilégient le fondement de la protection des droits et libertés.La France, les Pays-Bas et l’Espagne justifient la règle de l’exclusion par la nécessité de protéger les droits et libertés du suspect. Seuls les États-Unis retiennent comme fondement principal la confiscation de la preuve aux services de police.Enfin, l’Angleterre et la Belgique sont les deux seuls pays à privilégier la pertinence de la preuve, n’autorisant l’exclusion de la preuve irrégulière qu’en cas de violation de l’équité du procès.15. Les observations qui précèdent doivent néanmoins être nuancées. La justification de l’exclusion d’une preuve irrégulière est rarement exprimée clairement et, le plus souvent, le choix d’exclure ou non une preuve est dictée par d’autres justifications que celles initialement exprimées. Ainsi, dans huit cas sur quatorze, l’exclusion de la preuve peut aussi être dictée par la volonté de dissuader les autorités de violer les formalités prescrites par la loi. Les États-Unis ont, à l’inverse, retenu la standing doctrine, qui révèle l’importance du droit de l’accusé plutôt que la sanction du comportement policier. Il n’en demeure pas moins que le protective principle est le plus généralement privilégié au titre de fonction de la sanction d’exclusion. D. Le principe d’exclusion ou d’admissibilité de la preuve irrégulière16. Parmi les pays membres de l’Union Européenne, la règle est l’exclusion par principe des preuves irrégulières en cas de violation concrète d’un droit, à l’exception de l’Angleterre, de la Belgique et des Pays-Bas. Au total, dans treize des seize pays analysés, il peut être avancé que le principe est l’exclusion de la preuve irrégulièrement obtenue. Dans douze cas, le principe d’exclusion prévaut aussi en cas de violation du droit à la vie privée. Il est difficile de classer le système canadien, même si la jurisprudence de la Cour suprême tend à considérer l’exclusion comme de principe.E. L’automaticité de l’exclusion17. La preuve est toujours automatiquement exclue en cas de violation de l’article 3 de la convention. La plupart des pays connaissent des cas d’exclusion automatique en cas de violation des droits de la défense, et toujours en cas de provocation policière. La loi ne prévoit pas toujours l’exclusion des déclarations du suspect et des preuves dérivées lorsqu’il a été porté atteinte au droit de ne pas s’auto-incriminer, mais en pratique, tel est le plus souvent le cas.Dans huit États, il existe des cas d’exclusion automatique en cas de violation de formalités du droit à la vie privée. F. La discrétion du pouvoir judiciaire18. En dehors de ces cas d’exclusion automatique communs aux États, seuls deux pays connaissent un principe drastique d’exclusion des preuves irrégulières, à tout le moins dans leur formulation :la Turquie et la Grèce.Tous les autres systèmes accordent une marge d’appréciation au pouvoir judiciaire et, le plus souvent, ce pouvoir d’appréciation du juge est étendu.Tel n’est pas le cas, à tout le moins en cas d’atteinte à la vie privée, en Belgique et en Angleterre où le critère de l’équité du procès limite considérablement la latitude du pouvoir judiciaire d’exclure une preuve irrégulière.G. Les critères pris en considération19. La nature du droit est toujours prise en considération, de même que l’intensité de l‘atteinte au droit.La gravité du comportement de l’autorité responsable de la violation est retenue de manière très majoritaire. Il en va de même du critère de proportionnalité, exprimé différemment suivant les systèmes, entre la gravité de la violation (comportement policier/atteinte au droit individuel) d’une part, l’intérêt d’aboutir à une décision sur le fond d’autre part. Dans cette appréciation, il est tenu compte de l’importance que la preuve revêt pour aboutir à une décision de condamnation et, partant, de sa valeur probante lorsque les faits reprochés sont graves, dans six pays .H. La règle suivant laquelle il n’y a pas de nullité sans grief20. Il ne peut pas être dégagé de généralités quant à l’application de ce principe. Il est clairement établi par la loi en France, par la jurisprudence en Espagne et les États-Unis. Il n’est clairement pas retenu en Grèce et en Irlande. L’application du critère d’équité du procès nous paraît impliquer l’admissibilité de la preuve en cas de violation du droit d’un tiers en Belgique et en Angleterre. Aux Pays-Bas, l’exclusion ne peut en principe être décidée par le juge que si l’irrégularité est soulevée par sa victime, mais le juge dispose d’une marge de manœuvre pour en décider. Pour les autres pays, soit nous n’avons pas pu répondre à cette question sur la base des sources consultées, soit il n’existe pas solution univoque.V. Les constats issus de l’analyse comparéeA. Un système isolé de refus d’exclusion de la preuve irrégulière21. Les principes retenus en droit belge font de notre État l’un des seuls pays qui retient le principe d’admissibilité de la preuve irrégulière. La Belgique est d’ailleurs le seul État de droit qui pose comme principe l’obligation pour le pouvoir judiciaire d’admettre la preuve illégale et/ou irrégulière. En effet, même l’Angleterre, réticente à toute forme d’exclusion, a veillé à formuler le principe sous la forme d’une autorisation pour le juge d’exclure, et non d’une interdiction de le faire. Ce constat n’est pas sans confirmer l’inquiétude profonde et légitime que suscite la règle écrite à l’article 32 du TPCPP. Les cours et tribunaux se sont vus confisquer le contrôle réel de la légalité de la procédure. Ce choix est unique. Nous n’avons trouvé trace d’aucun système aussi affirmatif de l’usage de la preuve irrégulière. B. La nécessité de réaffirmer le principe d’exclusion ?22. L’exclusion de la preuve irrégulière doit redevenir le principe. Il en va avant tout d’une question d’éthique, ou de symbole, et la justice est aussi affaire de symboles. Formuler le principe de la légalité de la procédure n’a aucun sens si son corollaire naturel, soit l’interdiction d’exploiter une preuve autrement que dans le respect de la loi n’est pas formulé dans la suite immédiate.Ce choix relève directement de la notion d’État de droit, comme il a été souligné en guise d’introduction. Il est, en outre, conforme aux principes édictés dans la très large majorité des pays analysés.C. Un nécessaire pouvoir d’appréciation au détriment de la sécurité juridique ?23. L’affirmation d’une exclusion automatique de toute preuve irrégulière est caricaturale. Qui plus est, s’il faut élaborer des règles les plus précises possibles, notamment en vue de garantir la sécurité juridique, le fait de tout régler dans la loi et par la loi est un espoir vain. Outre que cela s’avère impossible, toutes les subtilités des cas rencontrés ne peuvent pas être pleinement appréhendées dans des normes légales. Il faut donc privilégier des cas d’exclusion automatique pour les atteintes les plus sévères aux droits fondamentaux, comme la violation de l’article 3 de la Convention pour ensuite fixer, dans la loi, des critères d’appréciation laissés au juge. D. La difficulté de fixer des critères d’appréciation stricts24. Ces critères doivent être justifiés par une réflexion de fond sur le principe d’exclusion de la preuve irrégulière. Il faut exposer au juge chargé de contrôler la régularité de la preuve les fonctions de la sanction mise à sa disposition, soit l’exclusion d’une preuve.Les critères classiquement retenus sont pour la plupart justifiés. Ce qui fait cruellement défaut, c’est l’exposé de ce qui les justifie pour en permettre une meilleure appréciation. Sur la base de ces réflexions, développées dans l’ouvrage, nous nous proposons d’élaborer un système cohérent d’exclusion des preuves irrégulières. VI. Conclusion :le modèle proposéA. L’objet de l’exclusion25. L’élément qu’il convient d’exclure n’est pas limité par sa valeur probante. Lorsque l’exclusion est décidée, elle ne porte pas seulement sur une preuve de culpabilité, mais sur une information quelconque, de sorte que nous ne retenons le terme « information » et non preuve.26. Par contre, la règle de l’exclusion ne doit pas amener à des solutions absurdes. Par exemple, si un cadavre est découvert, il ne peut pas être question d’exclure son existence pour ouvrir une enquête, de même que le fait que ce cadavre était criblé de balles, ce qui démontre un cas de mort violente.En ce sens, la constatation matérielle d’une infraction ne peut pas être tenue pour inexistante, même si elle est la conséquence d’une irrégularité. En pareil cas, il appartient au ministère public d’apprécier les suites qu’il y a lieu d’y donner et s’il paraît possible d’en recueillir une preuve régulière.Il n’en va autrement que lorsque l’exclusion est dictée par une violation de l’article 3 de la Convention.B. La torture et le traitement inhumain et dégradant – exclusion automatique de la preuve irrégulière27. Toute atteinte à l’article 3 de la Convention européenne des droits de l’homme en vue de l’obtention d’une preuve implique l’exclusion de la preuve irrégulièrement obtenue et de toutes les preuves dérivées qui s’en suivent.Ce choix est fondé sur le souci de confisquer la preuve, de protéger ou réparer le droit, individuel et général, et sur la nécessité de conserver l’intégrité de la Justice.Cette sanction procédurale doit être inscrite dans la loi, malgré qu’elle soit déjà unanimement admise. Cette première règle participe du modèle général mis en place. C. Les autres atteintes aux droits et principes essentiels28. Il n’y a pas d’exclusion de principe s’il n’y a pas d’atteinte à un droit ou un principe.Plutôt que de prévoir que la violation des prescriptions d’ordre n’implique aucune exclusion, il a été choisi de limiter le principe de l’exclusion par le constat d’une atteinte concrète à un droit ou à un principe.1. Le principe de l’exclusion de la preuve irrégulière29. Nous privilégions le principe d’exclusion de la preuve obtenue en violation du droit à la vie privée, les droits de la défense, le droit à l’intégrité et la violation des sources journalistiques. Dans ce modèle, la loi revendique la valeur de ce droit fondamental et le caractère essentiel de son respect. La loi protège et privilégie le respect du droit. Le pouvoir judiciaire n’est, par principe, intègre que s’il ne fonde pas une condamnation sur une preuve obtenue en violation de ces droits et valeurs.Il en va donc autant de l’intégrité du système dans son ensemble que de la nécessité de promouvoir le respect des droits individuels. Cette affirmation de principe est majoritaire dans les pays analysés.30. Le juste équilibre paraît pouvoir être trouvé avec un minimum d’exclusions légales attachées à des irrégularités spécifiques mettant concrètement en cause le droit à la vie privée. Les autres infractions au droit à la vie privée, et aux autres droits et valeurs énumérés ci-avant, justifient l’exclusion de la preuve irrégulière, mais le juge du fond peut décider de la conserver en application des critères les plus pertinents retenus de l’analyse de droit comparé.2. Les cas d’exclusion automatique31. Le législateur a réservé les atteintes les plus sévères aux droits fondamentaux à l’autorisation d’un juge indépendant et impartial et, en particulier, au juge d’instruction au cours d’une enquête pénale. Le législateur a donc déjà réalisé une analyse des actes les plus sensibles. Nous proposons de nous y référer et de ne prévoir l’exclusion qu’en cas de défaut d’autorisation.Il est donc proposé de prévoir l’exclusion lorsque l’acte a été posé sans que cette autorisation n’ait été obtenue. La disposition légale proposée serait, en ce sens, libellée dans les termes suivants :« Lorsqu’un acte d’enquête relevant de la seule compétence du juge d’instruction a été accompli sans que son autorisation n’ait été délivrée, les informations qu’il a permis d’obtenir sont exclues des débats, de même que les informations qui en sont dérivées. »32. Dans ces hypothèses, le juge de la régularité de la preuve n’a pas le choix. Il doit écarter la preuve. Sa seule marge d’appréciation consiste à déterminer si la violation de la formalité implique effectivement une violation du droit individuel que la formalité a vocation à garantir. 33. Compte tenu des fondements retenus, les preuves dérivées sont également exclues à condition qu’il soit constaté un lien causal entre la preuve irrégulière et la preuve dérivée. À défaut, cette dernière n’est tout simplement pas qualifiée de dérivée. La même sanction est appliquée que le prévenu ou l’accusé soit la victime de l’irrégularité ou non. Le texte pourrait être formulé de la manière suivante :« Hormis les hypothèses spécifiquement visées par la loi, le principe d’exclusion des informations s’applique même lorsque le prévenu n’a pas subi d’atteinte personnelle à ses droits. »Ce principe prévaut que la violation soit une atteinte au droit à la vie privée, à l’intégrité, aux droits de la défense ou encore au secret des sources journalistiques.3. Les cas d’exclusion régulés par le jugea- Le principe est l’exclusion de la preuve irrégulière34. Dans tous les autres cas d’atteinte aux droits de la défense, au droit à la vie privée, au droit à l’intégrité ou au secret des sources journalistiques, les irrégularités impliquent, en principe, l’exclusion de la preuve. Le juge saisi d’une demande d’exclusion doit écarter la preuve irrégulière dès lors qu’il constate une atteinte au droit à la vie privée. Il doit même le faire d’office. Le juge a néanmoins la possibilité d’admettre la preuve malgré l’irrégularité constatée, sur la base des critères cumulatifs / Doctorat en Sciences juridiques / info:eu-repo/semantics/nonPublished

Les problématiques de respect de la vie privée sont aujourd'hui indissociables des technologies modernes. Dans ce contexte, cette thèse s'intéresse plus particulièrement aux outils cryptographiques et à la façon de les utiliser pour répondre à ces nouvelles questions.Dans ce mémoire, je m'intéresserai tout d'abord aux preuves de connaissance sans divulgation qui permettent notamment d'obtenir la propriété d'anonymat pour les usagers de services de télécommunications. Je proposerai ainsi une nouvelle solution de preuve de connaissance d'un secret appartenant à un intervalle, ainsi que la première étude comparative des preuves existantes sur ce sujet. Je décrirai ensuite une nouvelle méthode permettant de vérifier efficacement un ensemble de preuves de type "Groth-Sahaï'', accélérant ainsi considérablement le travail du vérifieur pour de telles preuves. Dans un second temps, je m'intéresserai aux signatures caméléons. Celles-ci permettent de modifier, sous certaines conditions, un message signé. Ainsi, pour ces schémas, il est possible d'exhiber, à l'aide d'une trappe, une signature valide du signataire initial sur le message modifié. Je proposerai d'abord un nouveau schéma qui est à ce jour le plus efficace dans le modèle simple. Je m'intéresserai ensuite à certaines extensions de ce modèle qui ont pour vocation de donner au signataire les moyens de garder un certain contrôle sur les modifications faites a posteriori sur le message initial. Je décrirai ainsi à la fois le nouveau modèle de sécurité et les schémas associés prenant en compte ces nouvelles extensions. Enfin, je présenterai un ensemble d'applications se basant sur les briques cryptographiques introduites ci-dessus et qui permettent d'améliorer la protection de la vie privée des utilisateurs. J'aborderai tout particulièrement les problématiques d'abonnement, d'utilisation ou de facturation de services, ainsi que la gestion de contenus protégés dans un groupe hiérarchisé. / Privacy is, nowadays, inseparable from modern technology. This is the context in which the present thesis proposes new cryptographic tools to meet current challenges.Firstly, I will consider zero-knowledge proofs of knowledge, which allow in particular to reach the anonymity property. More precisely, I will propose a new range proof system and next give the first comparison between all existing solutions to this problem. Then, I will describe a new method to verify a set of ``Groth-Sahaï'' proofs, which significantly decreases the verification time for such proofs.In a second part, I will consider sanitizable signatures which allow, under some conditions, to manipulate (we say ``sanitize'') a signed message while keeping a valid signature of the initial signer. I will first propose a new scheme in the classical case. Next, I will introduce several extensions which enable the signer to obtain better control of the modifications done by the ``sanitizer''. In particular, I will propose a new security model taking into account these extensions and give different schemes achieving those new properties.Finally, I will present different applications of the above cryptographic tools that enhance customer privacy. In particular, I will consider the questions of subscription, use and billing of services and also address the issue of managing protected content in a hierarchical group.

Cette thèse traite de la theorie de la preuve pour les logiques a points fixes, telles que le μ-calcul, lalogique lineaire a points fixes, etc. ces logiques sont souvent munies de systèmes de preuves finitairesavec des règles d’induction à la Park. Il existe néanmoins d’autres sytèmes de preuves pour leslogiques à points fixes, qui reposent sur la notion de preuve infinitaire, mais qui sont beaucoupmoins developpés dans la litterature. L’objectif de cette thèse est de pallier à cette lacune dansl’état de l’art, en developpant la théorie de la preuve infnitaire pour les logiques a points fixes,avec deux domaines d’application en vue: les langages de programmation avec types de données(co)inductifs et la vérification des systèmes réactifs.Cette thèse contient trois partie. Dans la première, on rappelle les deux principales approchespour obtenir des systèmes de preuves pour les logiques à points fixes: les systèmes finitaires avecrègle explicite d’induction et les systèmes finitaires, puis on montre comment les deux approchesse relient. Dans la deuxième partie, on argumente que les preuves infinitaires ont effectivement unréel statut preuve-theorique, en montrant que la logique lineaire additive multiplicative avec pointsfixes admet les propriétés d’élimination des coupures et de focalisation. Dans la troisième partie,on utilise nos developpements sur les preuves infinitaires pour monter de manière constructive lacomplétude du μ-calcul lineaire relativement à l’axiomatisation de Kozen. / The subject of this thesis is the proof theory of logics with fixed points, such as the μ-calculus,linear-logic with fixed points, etc. These logics are usually equipped with finitary deductive systemsthat rely on Park’s rules for induction. other proof systems for these logics exist, which relyon infinitary proofs, but they are much less developped. This thesis contributes to reduce thisdeficiency by developing the infinitary proof-theory of logics with fixed points, with two domainsof application in mind: programming languages with (co)inductive data types and verification ofreactive systems.This thesis contains three parts. In the first part, we recall the two main approaches to theproof theory for logics with fixed points: the finitary and the infinitary one, then we show theirrelationships. In the second part, we argue that infinitary proofs have a true proof-theoreticalstatus by showing that the multiplicative additive linear-logic with fixed points admits focalizationand cut-elimination. In the third part, we apply our proof-theoretical investigations to obtain aconstructive proof of completeness for the linear-time μ-calculus w.r.t. Kozen’s axiomatization.

Le chiffrement à base de réseaux euclidiens a connu un grand essor durant les vingt dernières années. Autant grâce à l’apparition de nouvelles primitives telles que le chiffrement complètement homomorphe, que grâce à l’amélioration des primitives existantes, comme le chiffrement á clef publique ou les signatures digitales, qui commencent désormais à rivaliser avec leurs homologues fondés sur la théorie des nombres. Cela dit les preuves à divulgation nulle de connaissance, bien qu’elles représentent un des piliers des protocols de confidentialité, n’ont pas autant progressé, que ce soit au niveau de leur expressivité que de leur efficacité. Cette thèse s’attelle dans un premier temps à améliorer l’état de l’art en matière de preuves à divulgation nulle de connaissance. Nous construisons une preuve d’appartenance à un sous ensemble dont la taille est indépendante de l’ensemble en question. Nous construisons de même une preuve de connaissance amortie qui est plus efficace et plus simple que toutes les constructions qui la précèdent. Notre second propos est d’utiliser ces preuves à divulgation nulle de connaissance pour construire de nouvelles primitives cryptographiques. Nous concevons une signature de groupe dont la taille est indépendante du groupe en question, ainsi qu’un schéma de vote électronique hautement efficace, y compris pour des élections à grand échelle. / Lattice based cryptography has developed greatly in the last two decades, both with new and stimulating results such as fully-homomorphic encryption, and with great progress in the efficiency of existing cryptographic primitives like encryption and signatures which are becoming competitive with their number theoretic counterparts. On the other hand, even though they are a crucial part of many privacy-based protocols, zero-knowledge proofs of knowledge are still lagging behind in expressiveness and efficiency. The first goal of this thesis is to improve the quality of lattice-based proofs of knowledge. We construct new zero-knowledge proofs of knowledge such as a subset membership proof with size independent of the subset. We also work towards making zero-knowledge proofs more practical, by introducing a new amortized proof of knowledge that subsumes all previous results. Our second objective will be to use the proofs of knowledge we designed to construct novel and efficient cryptographic primitives. We build a group signature whose size does not depend on the size of the group, as well as a practical and highly scalable lattice-based e-voting scheme.