Cette thèse s'inscrit dans le vaste domaine des équations aux dérivées partielles et des systèmes dynamiques, et s'articule autour de deux sujets distincts. Le premier est relié à l'étude des équations de coagulation-fragmentation discrètes avec diffusion. En utilisant des lemmes de dualité, on établit de nouvelles estimations $L^p$ pour des moments polynomiaux associés aux solutions, sous une hypothèse de convergence des coefficients de diffusion. Ces estimations sur les moments permettent ensuite d'obtenir de nouveaux résultats de régularité, et de démontrer qu'une fragmentation suffisamment forte peut empêcher la gelation dans le modèle incluant la diffusion. Le second sujet est celui des preuves assistées par ordinateur dans le domaine des systèmes dynamiques. On améliore et on applique une méthode basée sur le théorème du point fixe de Banach, permettant de valider a posteriori des solutions numériques. Plus précisément, on élargit le cadre d'application de cette méthode pour inclure des opérateurs avec un terme dominant linéaire tridiagonal, on perfectionne une technique permettant de calculer et de valider des variétés invariantes, et on introduit une nouvelle technique qui améliore de manière significative l'utilisation de l'interpolation polynomiale dans le cadre de ces méthodes de preuves assistées par ordinateur. Ensuite, on applique ces techniques pour démontrer l'existence d'ondes progressives pour l'équation du pont suspendu, et pour étudier les états stationnaires non homogènes d'un système de diffusion croisée. / This thesis falls within the broad framework of partial differential equations and dynamical systems, and focuses more specifically on two independent topics. The first one is the study of the discrete coagulation-fragmentation equations with diffusion. Using duality lemma we establish new $L^p$ estimates for polynomial moments of the solutions, under an assumption of convergence of the diffusion coefficients. These moment estimates are then used to obtain new results of smoothness and to prove that strong enough fragmentation can prevent gelation even in the diffusive case. The second topic is the one of computer-assisted proofs for dynamical systems. We improve and apply a method enabling to a posteriori validate numerical solutions, which is based on Banach's fixed point theorem. More precisely, we extend the range of applicability of the method to include operators with a dominant linear tridiagonal part, we improve an existing technique allowing to compute and validate invariant manifolds, and we introduce an new technique that significantly improves the usage of polynomial interpolation for a posteriori validation methods. Then, we apply those techniques to prove the existence of traveling waves for the suspended bridge equation, and to study inhomogeneous steady states of a cross-diffusion system.

Le calcul rigoureux vise à produire des représentations certifiées pour les solutions de nombreux problèmes, notamment en analyse fonctionnelle, comme des équations différentielles ou des problèmes de contrôle optimal. En effet, certains domaines particuliers comme l’ingénierie des systèmes critiques ou les preuves mathématiques assistées par ordinateur ont des exigences de fiabilité supérieures à ce qui peut résulter de l’utilisation d’algorithmes relevant de l’analyse numérique classique.Notre objectif consiste à développer des algorithmes à la fois efficaces et validés / certifiés, dans le sens où toutes les erreurs numériques (d’arrondi ou de méthode) sont prises en compte. En particulier, nous recourons aux approximations polynomiales rigoureuses combinées avec des méthodes de validation a posteriori à base de points fixes. Ces techniques sont implémentées au sein d’une bibliothèque écrite en C, ainsi que dans un développement de preuve formelle en Coq, offrant ainsi le plus haut niveau de confiance, c’est-à-dire une implémentation certifiée.Après avoir présenté les opérations élémentaires sur les approximations polynomiales rigoureuses, nous détaillons un nouvel algorithme de validation pour des approximations sous forme de séries de Tchebychev tronquées de fonctions D-finies, qui sont les solutions d’équations différentielles ordinaires linéaires à coefficients polynomiaux. Nous fournissons une analyse fine de sa complexité, ainsi qu’une extension aux équations différentielles ordinaires linéaires générales et aux systèmes couplés de telles équations. Ces méthodes dites symboliques-numériques sont ensuite utilisées dans plusieurs problèmes reliés : une nouvelle borne sur le nombre de Hilbert pour les systèmes quartiques, la validation de trajectoires de satellites lors du problème du rendez-vous linéarisé, le calcul de polynômes d’approximation optimisés pour l’erreur d’évaluation, et enfin la reconstruction du support et de la densité pour certaines mesures, grâce à des techniques algébriques. / Rigorous numerics aims at providing certified representations for solutions of various problems, notably in functional analysis, e.g., differential equations or optimal control. Indeed, specific domains like safety-critical engineering or computer-assisted proofs in mathematics have stronger reliability requirements than what can be achieved by resorting to standard numerical analysis algorithms. Our goal consists in developing efficient algorithms, which are also validated / certified in the sense that all numerical errors (method or rounding) are taken into account. Specifically, a central contribution is to combine polynomial approximations with a posteriori fixed-point validation techniques. A C code library for rigorous polynomial approximations (RPAs) is provided, together with a Coq formal proof development, offering the highest confidence at the implementation level.After providing basic operations on RPAs, we focus on a new validation algorithm for Chebyshev basis solutions of D-finite functions, i.e., solutions of linear ordinary differential equations (LODEs) with polynomial coefficients. We give an in-depth complexity analysis, as well as an extension to general LODEs, and even coupled systems of them. These symbolic-numeric methods are finally used in several related problems: a new lower bound on the Hilbert number for quartic systems; a validation of trajectories arising in the linearized spacecraft rendezvous problem; the design of evaluation error efficient polynomial approximations; and the support and density reconstruction of particular measures using algebraic techniques.

A l’instar des juridictions qui l’ont précédé dans la répression des crimes internationaux, la Cour pénale internationale a besoin de la coopération des Etats pour exister. C’est une condition d’effectivité de l’action de la Cour qui se traduit par la participation des Etats à la procédure pénale internationale et par l’harmonisation des législations nationales. Toutefois, en dépit de son affirmation dans le Statut, les Etats parties exécutent difficilement l’obligation de coopération. Ces difficultés s’observent tant au niveau de leur participation à la procédure initiée par la Cour que dans l’exercice de la justice au niveau national. De fait, pour un respect des engagements internationaux devant la Cour, l’institution doit surmonter l’obstacle de la souveraineté nationale. Pour atteindre les objectifs fixés, elle doit amener les Etats à dépasser les critères traditionnels de compétence dans le domaine pénal et à taire les résistances souverainistes en la matière. C’est seulement à ce titre qu’elle peut être fonctionnelle, en opposant aux Etats une conception plus étendue de la justice pour laquelle ils se sont engagés. / Following the example of the jurisdictions which preceded her in the repression of the international crimes, the International Criminal Court needs the cooperation of States to exist. It is a condition of effectiveness of the action of the Court that is translated by the participation of States in the international criminal procedure and by the harmonization of the national legislations. But in spite of its assertion in the Status, States execute with difficulty the obligation of cooperation. These difficulties observe as long at the level of their participation in the procedure in front of the Court that in the exercise of the justice at the national level. Actually, for a respect for the international commitments in front of the Court, the institution has to surmount the obstacle of the national sovereignty. To reach the fixed objectives, she has to bring States to exceed the traditional criteria of skill in the penal domain and to keep silent about the resistances of states on the subject. It is only as such that she can be functional, by setting to States a more vast conception of the justice for which they made a commitment.

Private set intersection(PSI) is a two party protocol where both parties possess a private set and at the end of the protocol, one party (client) learns the intersection while other party (server) learns nothing. Motivated by some interesting practical applications, several provably secure and efficient PSI protocols have appeared in the literature in recent past. Some of the proposed solutions are secure in the honest-but-curious (HbC) model while the others are secure in the (stronger) malicious model. Security in the latter is traditionally achieved by following the classical approach of attaching a zero knowledge proof of knowledge (ZKPoK) (and/or using the so-called cut-and-choose technique). These approaches prevent the parties from deviating from normal protocol execution, albeit with significant computational overhead and increased complexity in the security argument, which includes incase of ZKPoK, knowledge extraction through rewinding. We critically investigate a subset of the existing protocols. Our study reveals some interesting points about the so-called provable security guarantee of some of the proposed solutions. Surprisingly, we point out some gaps in the security argument of several protocols. We also discuss an attack on a protocol when executed multiple times between the same client and server. The attack, in fact, indicates some limitation in the existing security definition of PSI. On the positive side, we show how to correct the security argument for the above mentioned protocols and show that in the HbC model the security can be based on some standard computational assumption like RSA and Gap Diffie-Hellman problem. For a protocol, we give improved version of that protocol and prove security in the HbC model under standard computational assumption. For the malicious model, we construct two PSI protocols using deterministic blind signatures i.e., Boldyreva’s blind signature and Chaum’s blind signature, which do not involve ZKPoK or cut-and-choose technique. Chaum’s blind signature gives a new protocol in the RSA setting and Boldyreva’s blind signature gives protocol in gap Diffie-Hellman setting which is quite similar to an existing protocol but it is efficient and does not involve ZKPoK.

Au cours de la dernière décennie, avec la standardisation d’Internet, le développement des réseaux à haut débit, le paiement à l’usage et la quête sociétale de la mobilité, le monde informatique a vu se populariser un nouveau paradigme, le Cloud. Le recours au cloud est de plus en plus remarquable compte tenu de plusieurs facteurs, notamment ses architectures rentables, prenant en charge la transmission, le stockage et le calcul intensif de données. Cependant, ces services de stockage prometteurs soulèvent la question de la protection des données et de la conformité aux réglementations, considérablement due à la perte de maîtrise et de gouvernance. Cette dissertation vise à surmonter ce dilemme, tout en tenant compte de deux préoccupations de sécurité des données, à savoir la confidentialité des données et l’intégrité des données. En premier lieu, nous nous concentrons sur la confidentialité des données, un enjeu assez considérable étant donné le partage de données flexible au sein d’un groupe dynamique d’utilisateurs. Cet enjeu exige, par conséquence, un partage efficace des clés entre les membres du groupe. Pour répondre à cette préoccupation, nous avons, d’une part, proposé une nouvelle méthode reposant sur l’utilisation de la cryptographie basée sur l’identité (IBC), où chaque client agit comme une entité génératrice de clés privées. Ainsi, il génère ses propres éléments publics et s’en sert pour le calcul de sa clé privée correspondante. Grâce aux propriétés d’IBC, cette contribution a démontré sa résistance face aux accès non autorisés aux données au cours du processus de partage, tout en tenant compte de deux modèles de sécurité, à savoir un serveur de stockage honnête mais curieux et un utilisateur malveillant. D’autre part, nous définissons CloudaSec, une solution à base de clé publique, qui propose la séparation de la gestion des clés et les techniques de chiffrement, sur deux couches. En effet, CloudaSec permet un déploiement flexible d’un scénario de partage de données ainsi que des garanties de sécurité solides pour les données externalisées sur les serveurs du cloud. Les résultats expérimentaux, sous OpenStack Swift, ont prouvé l’efficacité de CloudaSec, en tenant compte de l’impact des opérations cryptographiques sur le terminal du client. En deuxième lieu, nous abordons la problématique de la preuve de possession de données (PDP). En fait, le client du cloud doit avoir un moyen efficace lui permettant d’effectuer des vérifications périodiques d’intégrité à distance, sans garder les données localement. La preuve de possession se base sur trois aspects : le niveau de sécurité, la vérification publique, et les performances. Cet enjeu est amplifié par des contraintes de stockage et de calcul du terminal client et de la taille des données externalisées. Afin de satisfaire à cette exigence de sécurité, nous définissons d’abord un nouveau protocole PDP, sans apport de connaissance, qui fournit des garanties déterministes de vérification d’intégrité, en s’appuyant sur l’unicité de la division euclidienne. Ces garanties sont considérées comme intéressantes par rapport à plusieurs schémas proposés, présentant des approches probabilistes. Ensuite, nous proposons SHoPS, un protocole de preuve de possession de données capable de traiter les trois relations d’ensembles homomorphiques. SHoPS permet ainsi au client non seulement d’obtenir une preuve de la possession du serveur distant, mais aussi de vérifier que le fichier, en question, est bien réparti sur plusieurs périphériques de stockage permettant d’atteindre un certain niveau de la tolérance aux pannes. En effet, nous présentons l’ensemble des propriétés homomorphiques, qui étend la malléabilité du procédé aux propriétés d’union, intersection et inclusion / Recent technological advances have given rise to the popularity and success of cloud. This new paradigm is gaining an expanding interest, since it provides cost efficient architectures that support the transmission, storage, and intensive computing of data. However, these promising storage services bring many challenging design issues, considerably due to the loss of data control. These challenges, namely data confidentiality and data integrity, have significant influence on the security and performances of the cloud system. This thesis aims at overcoming this trade-off, while considering two data security concerns. On one hand, we focus on data confidentiality preservation which becomes more complex with flexible data sharing among a dynamic group of users. It requires the secrecy of outsourced data and an efficient sharing of decrypting keys between different authorized users. For this purpose, we, first, proposed a new method relying on the use of ID-Based Cryptography (IBC), where each client acts as a Private Key Generator (PKG). That is, he generates his own public elements and derives his corresponding private key using a secret. Thanks to IBC properties, this contribution is shown to support data privacy and confidentiality, and to be resistant to unauthorized access to data during the sharing process, while considering two realistic threat models, namely an honest but curious server and a malicious user adversary. Second, we define CloudaSec, a public key based solution, which proposes the separation of subscription-based key management and confidentiality-oriented asymmetric encryption policies. That is, CloudaSec enables flexible and scalable deployment of the solution as well as strong security guarantees for outsourced data in cloud servers. Experimental results, under OpenStack Swift, have proven the efficiency of CloudaSec in scalable data sharing, while considering the impact of the cryptographic operations at the client side. On the other hand, we address the Proof of Data Possession (PDP) concern. In fact, the cloud customer should have an efficient way to perform periodical remote integrity verifications, without keeping the data locally, following three substantial aspects : security level, public verifiability, and performance. This concern is magnified by the client’s constrained storage and computation capabilities and the large size of outsourced data. In order to fulfill this security requirement, we first define a new zero-knowledge PDP proto- col that provides deterministic integrity verification guarantees, relying on the uniqueness of the Euclidean Division. These guarantees are considered as interesting, compared to several proposed schemes, presenting probabilistic approaches. Then, we propose SHoPS, a Set-Homomorphic Proof of Data Possession scheme, supporting the 3 levels of data verification. SHoPS enables the cloud client not only to obtain a proof of possession from the remote server, but also to verify that a given data file is distributed across multiple storage devices to achieve a certain desired level of fault tolerance. Indeed, we present the set homomorphism property, which extends malleability to set operations properties, such as union, intersection and inclusion. SHoPS presents high security level and low processing complexity. For instance, SHoPS saves energy within the cloud provider by distributing the computation over multiple nodes. Each node provides proofs of local data block sets. This is to make applicable, a resulting proof over sets of data blocks, satisfying several needs, such as, proofs aggregation

Les systèmes dynamiques discrets, œuvrant en itérations chaotiques ou asynchrones, se sont avérés être des outils particulièrement intéressants à utiliser en sécurité informatique, grâce à leur comportement hautement imprévisible, obtenu sous certaines conditions. Ces itérations chaotiques satisfont les propriétés de chaos topologiques et peuvent être programmées de manière efficace. Dans l’état de l’art, elles ont montré tout leur intérêt au travers de schémas de tatouage numérique. Toutefois, malgré leurs multiples avantages, ces algorithmes existants ont révélé certaines limitations. Cette thèse a pour objectif de lever ces contraintes, en proposant de nouveaux processus susceptibles de s’appliquer à la fois au domaine du tatouage numérique et au domaine de la stéganographie. Nous avons donc étudié ces nouveaux schémas sur le double plan de la sécurité dans le cadre probabiliste. L’analyse de leur biveau de sécurité respectif a permis de dresser un comparatif avec les autres processus existants comme, par exemple, l’étalement de spectre. Des tests applicatifs ont été conduits pour stéganaliser des processus proposés et pour évaluer leur robustesse. Grâce aux résultats obtenus, nous avons pu juger de la meilleure adéquation de chaque algorithme avec des domaines d’applications ciblés comme, par exemple, l’anonymisation sur Internet, la contribution au développement d’un web sémantique, ou encore une utilisation pour la protection des documents et des donnés numériques. Parallèlement à ces travaux scientifiques fondamentaux, nous avons proposé plusieurs projets de valorisation avec pour objectif la création d’une entreprise de technologies innovantes. / Discrete dynamical systems by chaotic or asynchronous iterations have proved to be highly interesting toolsin the field of computer security, thanks to their unpredictible behavior obtained under some conditions. Moreprecisely, these chaotic iterations possess the property of topological chaos and can be programmed in anefficient way. In the state of the art, they have turned out to be really interesting to use notably through digitalwatermarking schemes. However, despite their multiple advantages, these existing algorithms have revealedsome limitations. So, these PhD thesis aims at removing these constraints, proposing new processes whichcan be applied both in the field of digital watermarking and of steganography. We have studied these newschemes on two aspects: the topological security and the security based on a probabilistic approach. Theanalysis of their respective security level has allowed to achieve a comparison with the other existing processessuch as, for example, the spread spectrum. Application tests have also been conducted to steganalyse and toevaluate the robustness of the algorithms studied in this PhD thesis. Thanks to the obtained results, it has beenpossible to determine the best adequation of each processes with targeted application fields as, for example,the anonymity on the Internet, the contribution to the development of the semantic web, or their use for theprotection of digital documents. In parallel to these scientific research works, several valorization perspectiveshave been proposed, aiming at creating a company of innovative technology.

L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le «dilemme du fabricant de tables» (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'«approximation polynomiale rigoureuse», permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre «vérifieur ISValP» est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en «précision augmentée» pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de «double-arrondi», qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis. / The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the ``Table Maker's Dilemma'' (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of ``Rigorous Polynomial Approximation'', allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel's lemma that we have formalized for both univariate and bivariate cases. In particular, our ``ISValP verifier'' is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of ``augmented-precision'' FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x²+y²) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the ``double-rounding'' phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.