CertiCrypt est une bibliothèque qui permet de vérifier la sécurité exacte de primitives cryptographiques dans l'assistant à la preuve Coq. CertiCrypt instrumente l'approche des preuves par jeux, et repose sur de nombreux domaines comme les probabilités, la complexité, l'algèbre, la sémantique des langages de programmation, et les optimisations de programmes. Dans cette thèse, nous présentons deux exemples d'utilisation d'EasyCrypt: le schéma d'encryption Hashed ElGamal, et les protocoles à connaissance nulle. Ces exemples, ainsi que les travaux antérieurs sur CertiCrypt, démontrent qu'il est possible de formaliser des preuves complexes; toutefois, l'utilisation de CertiCrypt demande une bonne expertise en Coq, et demeure laborieuse. Afin de faciliter l'adoption des preuves formelles par la communauté cryptographique, nous avons développé EasyCrypt, un outil semi-automatique capable de reconstruire des preuves formelles de sécurité à partir d'une ébauche formelle de preuve. EasyCrypt utilise des outils de preuves automatiques pour vérifier les ébauches de preuves, puis les compiles vers des preuves vérifiables avec CertiCrypt. Nous validons EasyCrypt en prouvant à nouveau Hashed ElGamal, et comparons cette nouvelle preuve avec celle en CertiCrypt. Nous prouvons également le schéma d'encryption Cramer-Shoup. Enfin, nous expliquerons comment étendre le langage de CertiCrypt à des classes de complexité implicite, permettant de modéliser la notion de fonctions en temps polynomial.

Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.

Le traitement des questions scientifiques est aujourd'hui un enjeu majeur pour les acteurs du contentieux interétatique : au-delà de son coût, il s'avère souvent décisif lorsqu'il s'agit pour les états de défendre leurs intérêts et pour le juge international de promouvoir la légitimité et la pérennité de son institution. La science est en effet considérée comme un gage d'objectivité, un outil capable de dire "le vrai" qui s'avère d'autant plus précieux pour les acteurs du contentieux interétatique que l'ordre juridique international est décentralisé. Pourtant, l'on ne peut manquer de constater le profond désenchantement suscité par la science au cours des dernières décennies : outre l'allongement souvent indu des délais, la multiplication des batailles d'experts dans le prétoire a fait naître un sentiment de méfiance grandissant à l'égard de la preuve scientifique, un doute quant à la part de vérité intrinsèque qu'elle est supposée pouvoir revendiquer. Pour déstabilisante qu'elle puisse être au regard de l'enjeu particulier du maintien de la paix, cette constatation ne doit néanmoins pas conduire à dénier à la science sa place et sa pertinence dans le cadre du règlement des différends interétatiques. La présente étude montrera ainsi que, dépouillé de toute prétention particulière à la vérité, l'expertise est susceptible de s'illustrer (et s'illustre parfois déjà) comme un outil utile et productif dans le cadre du règlement juridictionnel des différends entre états ; au-delà, l'on montrera encore que, dans certaines circonstances, l'expert possède même le pouvoir d'apaiser et de rapprocher les parties, favorisant ainsi l'émergence d'un règlement amiable entre elles / Dealing with scientific issues is nowadays a major concern in inter-state disputes : beyond the question of costs, these issues are often decisive for states in succeeding to defend their case and they are no less critical for international tribunals when it comes to promote their legitimacy and ultimately, their survival. Science is indeed perceived as possessing extraordinary qualities for the pursuit of the truth (in the widest sense of this word) and for this reason, it has traditionally been considered a very powerful and precious instrument, mostly in the international legal order which is naturally decentralized. Nevertheless, one cannot but notice the disenchantment science has given rise to over the last decades : the multiplication of expert battles in court has frequently induced an undesirable loss of time as well as a growing feeling of mistrust, both the litigants and the international judiciary finally doubting the power of science for ascertaining the real truth. However destabilizing this reality may be in the particular context of the maintenance of the peace, this study is dedicated to show that science is definitely relevant in the settling of inter-state disputes. Most often deprived nowadays of their alleged (and misleading) capacities for perfect objectivity and the search for truth, experts will be shown to be paradoxically useful and productive actors in the course of international judicial settlement ; moreover, they will be shown to possess, under certain circumstances, a real power for relieving pressure and promoting appeasement between the litigants, thus making it easier for them to reach an amicable settlement of their conflict

Mémoire présenté en cotutelle : Université Laval, Québec, Canada, Maître en droit (LL. M.) et Université des science sociales Toulouse I, Toulouse, France, Master (M.) / Notre présent mémoire se propose de mener une étude comparative entre deux systèmes de droit reposant sur deux traditions juridiques opposées : la France et le Canada. Il entreprend d'étudier leur matière criminelle et pénale pour constater que, dans ces deux systèmes ainsi arborés, toute contrevenance à la loi entraîne une sanction, principe valant également pour les autorités chargées de l'administration de la preuve criminelle qui méconnaissent les règles de procédure destinées à protéger son équilibre et les droits des parties. En France, cette sanction se traduit par la nullité de la procédure pénale qui consiste en l'annulation des preuves et autres obtentions découlant d'actes réalisés irrégulièrement par les autorités chargées de l'enquête. Pour reprendre la définition livrée par le Professeur Gérard Cornu, la nullité est la « sanction encourue par un acte juridique entaché d'un vice de forme ou d'une irrégularité de fond qui consiste dans l'anéantissement de l'acte ». Cependant, le concept de « nullités de la procédure pénale » ne revêt pas d'équivalent terminologique en droit criminel canadien. Si les nullités, qui rendent ineffectifs les actes réalisés et preuves obtenues relativement à des actes viciés ont un équivalent au Canada qui se traduit par l'annulation d'actes ou encore l'exclusion de la preuve obtenue indument, il n'en demeure pas moins que le terme de « nullités » n'est pas employé sauf à de très rares exceptions. De sucroît, le Canada prévoit en plus des sanctions-réparations, là encore adoptant diverses formes, ce qui constitue une originalité incontestable par rapport au droit français. Ce mémoire portant sur les sanctions des procédures défaillantes implique de définir la notion de sanction. Cette dernière peut être comprise comme la conséquence attachée à l'utilisation, ou encore à l'application d'une règle de droit. Cette sanction peut alors émaner de la violation d'une règle de droit qui nécessite son application. Cependant, le terme même de « sanction » n'est pas nécessairement négatif : la sanction peut très bien émaner de sa propre nécessité, indépendante de toute violation. Par exemple, en droit civil français, une sanction peut être une mesure qui sera mobilisée pour approuver un acte et le rendre exécutoire, comme une homologation. Cette notion de sanction sera pourtant ici employée dans son sens défavorable, puisqu'il s'agira d'étudier la conséquence que constitue la sanction comme une résultante négative émanant de la violation de normes préétablies, par les autorités chargées de l'administration de la preuve, suivant un strict cadre normatif. En outre, ce concept est ici employé au pluriel puisque dans le cadre de ce projet, plusieurs sanctions seront exposées, notamment des sanctions de deux types en particulier : les sanctions-annulations et les sanctions-réparations. Ces sanctions trouveront application en présence de procédures criminelles ou pénales défaillantes, c'est-à-dire les procédures qui porteront en elles un ou plusieurs vice(s) résultant de la violation des normes procédurales de forme ou de fond, et nécessitant que les actes entachés par ces violations soient annulés, que les preuves découvertes conformément à ces actes soit exclues, que les procédures soient arrêtées ou encore que le préjudice occasionné à la partie qui le subit, soit réparé ou compensé, à tout le moins. Une procédure défaillante peut donc être entendue comme une procédure qui, parce qu'elle est viciée, compromet l'équilibre des droits des parties et méconnaît les droits fondamentaux d'une partie en particulier : le mise en cause dans une affaire pénale. Partant, le présent mémoire exposera les différentes sanctions existantes face aux violations procédurales, avant d'exposer la pratique autour de l'application de ces sanctions.

.

"Mémoire présenté à la faculté des études supérieures en vue de l'obtention du grade de maîtrise en droit (L.L.M.)" / Il est devenu commun de dire que notre société se transforme inexorablement en une société dite de « l'information ». Cette transformation se caractérise entre autres par une utilisation accrue des technologies de l'information afin de communiquer, d'échanger ou de transiger. Les supports traditionnels de communication (tel que le papier) cèdent progressivement leur place à de nouveaux supports technologiques favorisant l'efficacité et la rapidité des échanges, et par la même occasion le développement du commerce électronique. Qu'on le souhaite ou non, un constat s'impose: la montée en puissance des réseaux virtuels a eu raison du monopole du papier. Sur le plan juridique, cette nouvelle réalité bouleverse aussi considérablement les règles de droit civil largement pensées et ancrées dans un contexte papier. L'avènement de la numérisation et du phénomène de la dématérialisation des supports ont effectivement soulevé plusieurs questions d'ordre juridique tout à fait nouvelles que nous pourrions résumer de la manière suivante: Quels sont les rapports entre l'écrit et son support autre que le papier? Quelles sont les caractéristiques de l'écrit faisant appel aux technologies de l'information? Ce type d'écrit peut-il être admis en tant que moyen de preuve? Si oui, quelle sera sa force probante? Ce type d'écrit doit-il être conservé? Le présent mémoire vise précisément à identifier certains éléments de réponses à ces diverses questions en étudiant spécifiquement les cadres juridiques français et québécois. Ce mémoire traite d'une part des enjeux liés à l'évolution et au rôle de l'écrit face à l'avènement des technologies de l'information et d'autre part du cadre juridique de la preuve et de la conservation de l'écrit dans la société de l'information. / It is becoming commonplace to say that we have entered a so-called "information society". In the process, we have witnessed a transformation characterized by an increased use of information and communication technologies that has revolutionized the way we communicate, learn and conduct business. The traditional communication formats (i.e., paper) gradually yield their place to new technological formats which affect the effectiveness and the speed of transactions, there by enabling the rise of ecommerce. The advent of virtual networks calls into question the monopoly of paper. From a legal perspective, the new paradigm has a huge impact on civil law rules, which were largely anchored in a paper context. The advent of the digitization and the phenomenon of the dematerialization of formats raised several new legal issues that we could summarize in the following manner: What is the relationship between writing and its various formats (e.g., other than paper)? What characterizes writing in an electronic environment? Can this type of writing act as evidence? If so, what will be its conclusive force? How can the integrity of documents be ensured? This thesis examines these various questions within the context of two different legislations: France and Québec. Two issues are addressed: 1) the evolution ofwriting in an electronic, networked environment; 2) the legal framework around evidence and archiving ofwriting in the information society.

L'expertise psychiatrique est requise au tribunal dans plusieurs situations juridiques tant en matière criminelle que civile et elle est soumise aux mêmes règles de preuve que n'importe quelle expertise. Pourtant, la psychiatrie et son objet sont tout à fait particuliers. La relation que peuvent entretenir le juge et l'expert-psychiatre est teintée par plusieurs éléments de nature sociale et professionnelle, mais aussi simplement juridique et procédural. Alors que les juristes parlent de cette relation comme d'une usurpation du rôle du juge par l'expert-psychiatre, les psychiatres, au contraire, croient que leur expertise est totalement pervertie dans le processus judiciaire. Mais la réalité n'est pourtant pas univoque: si l'expertise psychiatrique est de façon générale une preuve parmi les autres, elle peut également occuper une place centrale dans le mécanisme décisionnel. / Psychiatric report is required at the court in several legal statements as weIl in criminal matters as in civic matters and is subject to the same codes of proofs as any other expert report. Still, psychiatry and its object are absolutely peculiar. The relation that may be kept between the judge and the expert psychiatrist is tinged with many elements of social and professional nature but also of judicial and quibbling nature, simply. While lawyers and legal experts quote that relationship of an usurpation of the judge part by the expert psychiatrist , psychiatrists on the other hand reckon that the expert report is completely perverted by the judicial process. Yet, reality is not univocal. If the psychiatric report is globally a proof among many others, it can still have a crucial impact in the ruling machinery.

Ce projet de mémoire de maîtrise portera sur Descartes et la preuve dite "ontologique" de l'existence de Dieu. La présentation qui sera faite de cette preuve, de ses tenants et de ses aboutissants, tiendra compte: premièrement, du rôle et du statut de celle-ci dans l'ordre des raisons métaphysiques; deuxièmement, des relations entre la preuve "ontologique" et la preuve dite "par les effets"; et troisièmement, des différentes oeuvres de Descartes dans lesquelles il est question de l'argument ontologique. Ainsi, cette analyse permettra de noter les différences relatives qu'il pourrait y avoir chez Descartes quant au fond ou à la forme de cet argument. Nous évoquerons notamment la position différente qu'occupe cette preuve dans deux écrits, soient les Méditations métaphysiques (1641) et les Principes de la philosophie (1644). Ce genre d'analyse nous permettra de nous pencher sur le débat initié par Martial Guéroult et Henri Gouhier concernant la place de la preuve "ontologique" de l'existence de Dieu au sein de l'ordre des raisons métaphysiques ainsi que ses relations avec la preuve "par les effets". La postérité de ce débat sera également considérée. Aussi, nous serons à même de poser la question à savoir s'il y a une évolution de la preuve "ontologique" de l'existence de Dieu au fil des oeuvres dans la pensée de Descartes. En résumé, dans ce mémoire, nous aborderons deux problématiques: la question de l'autonomie ou de la non autonomie de la preuve "ontologique" par rapport à la preuve "par les effets", et le questionnement quant à la possibilité d'une évolution de la place et de la nature de la preuve dite "ontologique" de l'existence de Dieu dans les écrits de Descartes. / This master thesis project will focus on Descartes and the "ontological" proof of the existence of God. The presentation will be made of this proof, its ins and outs. It will take into account: first, the role and status of the latter in the order of metaphysical reasons; second, the relationship between the "ontological" proof and the "through the effects" proof; and third, the various writings of Descartes in which it is question of the ontological argument. Thus, this analysis will note the differences there might be in Descartes thought regarding the substance or form of this argument. We will discuss on the different position this proof occupied in two writings: the Meditations (1641) and the Principles of Philosophy (1644). This type of analysis will allow us to focus on the debate initiated by Martial Guéroult and Henri Gouhier concerning the place of the "ontological" proof of the existence of God in the order of metaphysical reasons as well as its relations with the "through the effects" proof. The posterity of this debate will also be considered. Also, we will be able to ask the question whether there is an evolution of the "ontological" proof of the existence of God in the thought of Descartes over his writings. In summary, in this thesis, we address two issues: the question of autonomy or non-autonomy of the "ontological" proof in relation with the "through the effects" proof; and the question about the possibility of an evolution of the place and nature of the "ontological" proof of the existence of God in the writings of Descartes.

Le contrat unilatéral désigne en droit français un contrat par lequel « une ou plusieurs personnes sont obligées envers une ou plusieurs autres, sans que de la part de ces dernières il y ait d’engagement » (article 1103 du Code civil). Procéder à l’analyse fonctionnelle de la notion de contrat unilatéral consiste ainsi à s’interroger sur l’utilité de distinguer dans une catégorie spécifique les contrats qui n’obligent que d’un côté. A quoi cela sert-il de penser les contrats à partir du caractère unilatéral des obligations qu’ils produisent ? Cette interrogation invite d’abord à éprouver la fonction normative de la notion de contrat unilatéral, c’est-à-dire sa capacité à justifier l’application de règles spécifiques. Les résultats de cette première démarche révèlent que la notion de contrat unilatéral ne commande pas l’application d’un régime spécifique et que son utilité principale ne tient donc pas à la faculté qu’elle aurait de déterminer l’application de règles de droit particulières. Une étude attentive de ses origines et de son utilisation en droit positif montre au contraire que la notion de contrat unilatéral remplit principalement une fonction définitoire de la notion de contrat elle-même. Contre la tentation de réduire le contrat aux conventions qui obligent réciproquement toutes les parties, elle rappelle expressément que le droit français ne distingue pas selon le caractère unilatéral ou réciproque des obligations produites pour retenir la qualification de contrat. Ainsi, la notion de contrat unilatéral se présente, en quelque sorte, comme le gardien de la définition large du contrat posée par l’article 1101 du Code civil. / Under French law, a unilateral contract is contract by which “one or several persons obligate themselves to one or several others without any commitment on the part of the latter” (article 1103 of the Civil Code). The functional analysis of the notion of the unilateral contract raises the question of the utility in identifying a specific category of contracts which bind only one party. As a first step, this question is an invitation to challenge the normative function of the notion of unilateral contract, that is to say its ability to cause the application of specific rules. The results of this first step show that the notion of unilateral contract does not cause the application of a specific system of rules and that its main purpose is therefore not to determine the application of specific legal rules. A thorough study of its origins and its use in case law shows, instead, that the notion of unilateral contract mainly fulfills a definitional function of the concept of contract itself. Against the temptation to reduce the definition of contract solely to agreements that oblige all parties to each other, the notion of unilateral contract is a reminder that French law does not distinguish between the unilateral or reciprocal nature of the obligations provided in the agreement. Such an agreement qualifies as a contract. Thus, the notion of unilateral contract arises, somehow, as the guardian of the broad definition of the contract provided for by Article 1101 of the Civil Code.

Nous nous intéressons au développement prouvé de composants formels pour un générateur de code pré-qualifié. Ce dernier produit un code séquentiel (C et Ada) pour des modèles d'entrée qui combinent les flots de données et de contrôle et qui présentent des possibilités d'exécution concurrente (Simulink/Stateflow et Scicos). Le développement prouvé permet de réduire le coût des tests et d'augmenter l'assurance des outils développés avec cette approche vis-à-vis de la qualification. Les phases de spécification, de développement et de vérification des outils développés sont effectuées avec l'assistant de preuve Coq. Ce dernier permet d'extraire le contenu calculatoire des composants en préservant les propriétés prouvées en Coq. Ce code extrait est ensuite intégré dans une chaîne complète de développement (chaîne de GeneAuto). Nous présentons un cadre formel, inspiré de l'analyse statique, qui s'appuie sur la sémantique abstraite et qui est instanciable sur plusieurs composants du générateur de code. Nous nous basons sur les ensembles partiellement ordonnés et sur le calcul de point fixe pour définir le cadre et effectuer les différentes analyses des composants du générateur de code. Ce cadre formel comporte toutes les preuves communes aux composants et indépendantes des analyses effectuées. Deux composants sont étudiés : l'ordonnanceur et le typeur des modèles d'entrée. / We are interested in the proved development of formal components for a pre-qualified code generator. This produces a sequential code (C and Ada) for input models that combine data and control flows, with potential concurrent execution (Simulink/Stateflow and Scicos). The proved development reduces test cost and increases insurance of components developed with this approach regarding the qualification. Phases of specification, development and verification of the developed components are done with the Coq proof assistant. This allows to extract the computational content of the components preserving the properties proved in Coq. The extracted code is then integrated into the complete development tool-chain (GeneAuto tool-chain). We present a formal framework, inspired from static analysis, based on the abstract semantics which is instantiable to several components of the code generator. We rely on partially ordered sets and fixed-point to define de formal framework and to perform the various analysis of components of the code generator. This formal framework includes all proofs common to the components and independent from the performed analyses. Two components are studied : the scheduler and the type checker of input models.