Une allégation de santé dans l’UE nécessite des preuves cliniques de l’efficacité et de la sécuritéd’une supplémentation nutrititionnelle. Les probiotiques, en particulier les bactéries lactiques,rentrent dans ce cadre règlementaire dans lequel l’EFSA indique que les preuves obtenues chez despatients avec des troubles fonctionnels intestinaux sont transposables chez une population de sujetssains. Le protocole LAPIBSS est un essai clinique de haute qualité méthodologique évaluantl’efficacité de 2 souches de Lactobacillus acidophilus à diminuer la sévérité des symptômes dusyndrome de l’intestin irritable. Les résultats confirment la sécurité d’emploi des souches utiliséesmais ne montrent pas une diminution significative des symptômes comparée au placebo après 8semaines. L’effet global du traitement est statistiquement significatif sur le score de flatulence. Uneffet placebo et l’hétérogénéité importante de la sévérité des symptômes à l’inclusion pourraientexpliquer nos résultats. Une meilleure compréhension des effets physiologiques des probiotiqueschez l’homme pourrait améliorer le rationnel de leur utilisation en recherche clinique. / A health claim across the EU requires clinical evidence about the efficacy and safety of a nutritionalsupplementation. Probiotics, especially lactic acid bacteria, fall within this regulatory framework inwhich EFSA indicates that the evidence from patients with functional gastrointestinal disorder aretransferable in a population of healthy subjects. The LAPIBSS protocol is a high-quality clinicaltrial assessing the efficacy of 2 strains of Lactobacillus acidophilus to reduce the irritable bowelsyndrome symptoms severity. Results confirm the safety of strains used but do not show asignificant decrease of symptoms compared with placebo after 8 weeks. The overall treatment effectis statistically significant on the flatus score. A placebo effect and the considerable heterogeneity ofsymptoms severity at baseline would explain our results. A better understanding of physiologicaleffects of probiotics in human would be needed to upgrade the rationale for their use in clinicalresearch.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Th. doct.--Informatique et réseaux--Paris--ENST, 1992. / Bibliogr. p. 155-158.

Th. doct.-ing.--Lille 1, 1977. N°: 202.

Cette thèse traite de la vérification des protocoles cryptographiques. Son sujet est la modélisation symbolique de protocoles avec pour objectif la preuve de propriétés de sécurité. La thèse comprend deux parties: La première partie définit quatre modèles symboliques différant par les moyens syntaxiques que les concepteur peuvent utiliser pour représenter les primitives cryptographiques. On a observé que les vérificateurs utilisent des astuces de codage dans des modèles peu riches pour représenter les primitives manquantes. Nous montrons que ces codages sont corrects dans le sens où un protocole qui satisfait une propriété dans un modèle peu expressif la satisfait aussi dans un modèle plus riche. Nous terminons cette partie par la description d'un module que nous avons implémenté pour la plate-forme de vérification AVISPA. Ce module est basé sur des résultats permettant le transfert des propriétés d'un protocole, prouvées dans un modèle symbolique, vers un modèle calculatoire. Dans la deuxième partie de cette thèse, nous développons un modèle symbolique pour représenter des protocoles récursifs. Ces protocoles sont difficiles à analyser et peu de résultats de décidabilité existent. Nous montrons que notre modèle symbolique permet de retrouver une attaque connue contre une propriété d'un protocole de commerce électronique. Nous proposons ensuite une modification de ce protocole et montrons que le protocole modifié satisfait cette propriété. / This thesis deals with formal verification of cryptographic protocols. It is about symbolic modelling of protocols with the objective to prove security properties. The thesis is split in two parts: The first part defines four symbolic models which differ in the syntactic resources that protocol designers may use do model cryptographic primitives. We found that engineers employ coding dodges in order to model missing cryptographic primitives in simpler models. We showed that these codings are correct in that protocol properties that are proven in lean models also hold in more elaborated models. We finish this part with the description of a module implementation for the verification plate-form AVISPA. The module is based on results that allow to automatically translate protocol properties, proven in symbolic models, to computational models. In the second part of this thesis, we develop a symbolic model in order to represent ecursive protocols. This class of protocols is difficult to analyse and, so far, there are only few decidability results. We show that our symbolic model allows us to retrieve an previously known attack against a special security property of an e-commerce protocol. We then modify this protocol and show that the property holds for the modified protocol.

Th.--Informatique--Paris-Sud--Orsay, 1988. / 1988 d'après la déclaration de dépôt légal. Thèse préparée au sein du projet CHORUS de l'INRIA. Bibliogr. p. 135-140.

Nous proposons dans notre thèse une nouvelle méthodologie pour le développement des protocoles de communication et des applications réparties en explorant une approche de synthèse automatisée. Après avoir effectué un état de l'art sur les techniques de synthèse de protocoles, nous présentons, dans la première partie de la thèse, une nouvelle méthode de synthèse automatique de spécifications de protocoles à partir de spécifications de services dans un modèle de réseaux de Petri interprétés. Notre approche de synthèse est basée sur un nouveau concept de raffinement de réseaux de Petri qui assure la correction des protocoles construits de façon incrémentale. L'intérêt principal de cette méthode par rapport aux techniques classiques basées sur l'analyse est qu'elle évite la phase supplémentaire de validation du protocole qui passe souvent par une analyse exhaustive dont le problème fondamental est l'explosion combinatoire. De plus, le coût de construction des protocoles est considérablement diminué. Partant d'une description de service, notre technique de synthèse permet de dériver automatiquement au niveau protocole l'ensemble des fonctionnalités suivantes: (1) traitements répartis, (2) flot de contrôle, (3) flot de données, (4) contrôle de la cohérence des données, (5) et choix distribué. Elle constitue, de ce fait, un "bon" compromis entre le pouvoir de synthèse et le pouvoir d'expression des services relativement aux techniques existantes. Dans la deuxième partie de la thèse nous présentons une application réelle de notre méthode de synthèse à la conception du protocole de transport ISO de base (ISO 8073), le point de départ de la conception étant la spécification du service de transport ISO 8072. Dans la troisième partie de la thèse, nous présentons un ensemble d'outils logiciels pour la synthèse automatique de protocoles que nous appelons STEPS (Software Toolset for automatEd Protocol Synthesis). Nous avons développé cet ensemble d'outils afin de démontrer l'utilité et la faisabilité de l'approche de synthèse que nous proposons. La sémantique de notre modèle de spécification étant assez proche de celle du langage Estelle, nous proposons une extension de notre démarche pour la synthèse de spécifications de protocoles dans le langage Estelle. L'intérêt est que ces spécifications peuvent être directement exploitées par des outils existants afin de générer automatiquement du code exécutable ou d'effectuer des simulations et des évaluations de performances.

Dans une infrastructure logicielle, les systèmes critiques ont souvent besoin de garder des clés cryptographiques sur des HSM ou des serveurs consacrés à la gestion de clés. Ils ont pour but de séparer les opérations cryptographiques, très critiques, du reste du réseau, qui est plus vulnérable. L'accès aux clés est fourni au travers des APIs de sécurité, comme par exemple le standard PKCS#11 de RSA, CCA d'IBM, ou encore l'API du TPM, qui ne permettent qu'un accès indirect aux clés. Cette thèse est composée de deux parties. La première introduit des méthodes formelles qui ont pour but l'identification des configurations dans lesquelles les APIs de sécurité peuvent améliorer le niveau de sûreté des protocoles existants, par exemple en cas de compromission d'un participant. Un paradigme prometteur considère les APIs de sécurité comme des participants d'un protocole afin d'étendre l'emploi des méthodes traditionnelles d'analyse de protocole à ces interfaces. À l'opposé des protocoles réseau, les APIs de sécurité utilisent souvent une base de données interne. Ces outils traditionnels d'analyse ne sont adaptés que pour le cas où le nombre des clés est borné a priori. Nous exposons également des arguments pour l'utilisation de la réécriture de multi-ensembles (MSR), lors de la vérification. De plus, nous proposons un langage dérivant du pi-calcul appliqué possédant des opérateurs qui permettent la manipulation d'un état explicite. Ce langage se traduit en règles MSR en préservant des propriétés de sécurité qui s'expriment dans une logique de premier ordre. La traduction a été implémentée sous forme d'un prototype produisant des règles spécifiquement adapté au prouveur tamarin. Plusieurs études de cas, dont un fragment de PKCS#11, le jeton d'authentification Yubikey, et un protocole de signature de contrat optimiste ont été effectuées. Le deuxième partie de la présente thèse a pour but l'identification des propriétés de sécurité qui a) peuvent être établies indépendamment du protocole b) permettent de trouver des failles au niveau de la cryptographie b) facilitent l'analyse des protocoles utilisant cette API de sécurité. Nous adoptons ici l'approche plus générale de Kremer et al. dans un cadre qui permet la composition universelle, à travers une fonctionnalité de gestion de clés. La nouveauté de ce genre de définition est qu'elle dépend des opérations mises à disposition par l'API. Ceci est seulement possible grâce à la composition universelle. Une API de sécurité n'est sûre que si elle réalise correctement la gestion des clés (selon la fonctionnalité présentée dans ce travail) et les opérations utilisant les clés (selon les fonctionalités qui les définissent). Pour finir, nous présentons aussi une implémentation de gestion de clés définie par rapport à des opérations arbitraires utilisant des clés non concernées par la gestion des clés. Cette réalisation représente ainsi un modèle générique pour le design des APIs de sécurité. / Security critical applications often store keys on dedicated HSM or key-management servers to separate highly sensitive cryptographic operations from more vulnerable parts of the network. Access to such devices is given to protocol parties by the means of Security APIs, e.g., the RSA PKCS#11 standard, IBM's CCA and the TPM API, all of which protect keys by providing an API that allows to address keys only indirectly. This thesis has two parts. The first part deals with formal methods that allow for the identification of secure configurations in which Security APIs improve the security of existing protocols, e.g., in scenarios where parties can be corrupted. A promising paradigm is to regard the Security API as a participant in a protocol and then use traditional protocol analysis techniques. But, in contrast to network protocols, Security APIs often rely on the state of an internal database. When it comes to an analysis of an unbounded number of keys, this is the reason why current tools for protocol analysis do not work well. We make a case for the use of MSR as the back-end for verification and propose a new process calculus, which is a variant of the applied pi calculus with constructs for manipulation of a global state. We show that this language can be translated to MSR rules while preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a back-end. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and a contract signing protocol. The second part of this thesis aims at identifying security properties that a) can be established independent of the protocol, b) allow to catch flaws on the cryptographic level, and c) facilitate the analysis of protocols using the Security API. We adapt the more general approach to API security of Kremer et.al. to a framework that allows for composition in form of a universally composable key-management functionality. The novelty, compared to other definitions, is that this functionality is parametric in the operations the Security API allows, which is only possible due to universal composability. A Security API is secure if it implements correctly both key-management (according to our functionality) and all operations that depend on keys (with respect to the functionalities defining those operations). We present an implementation which is defined with respect to arbitrary functionalities (for the operations that are not concerned with key-management), and hence represents a general design pattern for Security APIs.

Les protocoles cryptographiques sont cruciaux pour sécuriser les transactions électroniques. La confiance en ces protocoles peut être augmentée par l'analyse formelle de leurs propriétés de sécurité. Bien que beaucoup de travaux aient été dédiés pour les protocoles classiques comme le protocole de Needham-Schroeder, très peu de travaux s'adressent à la classe des protocoles de groupe dont les caractéristiques principales sont : les propriétés de sécurité spécifiques qu'ils doivent satisfaire, et le nombre arbitraire des participants qu'ils impliquent. Cette thèse comprend deux contributions principales. La première traite la première caractéristique des protocoles de groupe. Pour cela, nous avons défini un modèle appelé modèle de services que nous avons utilisé pour proposer une stratégie de recherche d'attaques se basant sur la résolution de contraintes. L'approche proposée a permis de retrouver d'anciennes attaques et d'en découvrir de nouvelles sur quelques protocoles de groupe. Certaines attaques ont aussi pu être généralisées pour couvrir le cas de n participants. La deuxième contribution principale de cette thèse consiste à définir un modèle synchrone qui généralise les modèles standards de protocoles en permettant les listes non bornées à l'intérieur des messages. Ceci est assuré par l'introduction d'un nouvel opérateur appelé mpair qui représente une liste construite sur un même patron. Dans ce modèle étendu, nous avons proposé une procédure de décision pour une classe particulière des protocoles de groupe appelée classe de protocoles bien-tagués avec clefs autonomes, en présence d'un intrus actif et avec des clefs composées. / Cryptographic protocols are crucial for securing electronic transactions. The con?dence in these protocols can be increased by the formal analysis of their security properties. Although many works have been dedicated to standard protocols like Needham-Schroeder, very few address the class of group protocols whose main characteristics are : the speci?c security properties that they must satisfy, and the arbitrary number of participants they imply. This thesis provides two main contributions. The ?rst one deals with the ?rst characteristic of group protocols. For that, we de?ned a model called the services model which we used to propose a strategy for ?aws detection based on constraints solving. The suggested approach allows us to ?nd known attacks and new ones on some group protocols. Some attacks have been also generalized to cover the case of n participants. The second main contribution of this thesis consists in de?ning a synchronous model, that generalizes standard protocol models by permitting unbounded lists inside messages. This is ensured by the introduction of a new operator called mpair which represents a list built on the same pattern. In this extended model, we have proposed a decision procedure for a particular class of group protocols called the class of well-tagged protocols with autonomous keys, in presence of an active intruder and with composed keys.