<p align="justify">The main contribution of this thesis is the emphasis made on the reusability concept, on one side, for designing a simulation environment, and on the other side, for defining two different levels of granularity for reusable network component libraries.</p> <p align="justify">The design of our simulation environment, called AMS for Atelier for Modeling and Simulation, was based on existing pieces of software, which proved their usefulness in their respective fields. In order to carry out this integration efficiently, a modular structure of the atelier was proposed. The structure has been divided into four phases. Each phase is responsible of a part of the performance evaluation cycle. The main novelty of this structure is the usage of a dedicated language as a means to define a clear border between the editing and simulation phases and to allow the portability of the atelier upon different platforms. A prototype of the atelier has been developed on a SUN machine running the SunOs operating system. It is developed in C language.</p> <p align="justify">The kernel of the AMS is its library of Detailed Basic Models (DBMs). Each DBM was designed in order to comply with the most important criterion which is reusability. Indeed, each DBM can be used in aeveral network architectures and can be a component of generic and composite models. Before the effective usage of a DBM, it is verified and validated in order to increase the model credibility. The most important contribution of this research is the definition of a methodology for modeling protocol entities as DBMs. We then tried to partly bridge the gap between specification and modeling. This methodology is based on the concept of function. Simple functions are modeled as reusable modules and stored into a library. The Function Based Methodology was designed to help the modeler to build efficiently and rapidly new protocols designed for the new generation of networks where several services can be provided. These new protocols can be dynamically tailored to the user' s requirements.</p>

Cette thèse propose une nouvelle approche pour la synthèse de valeurs temporelles dans les systèmes temporisés. Notre approche est basée sur la méthode inverse suivante : à partir d’une instance de référence des paramètres, nous synthétisons une contrainte sur les paramètres, garantissant le même comportement que pour l’instance de référence, abstraction faite du temps. Il en résulte un critère de robustesse pour le système. En itérant cette méthode sur des points dans un domaine paramétrique borné, nous sommes alors à même de partitionner l’espace des paramètres en bonnes et mauvaises zones par rapport à une propriété à vérifier. Ceci nous donne une cartographie comportementale du système. Cette méthode s’étend aisément aux systèmes probabilistes. Nous présentons également des variantes de la méthode inverse pour les graphes orientés valués et les processus de décision markoviens. Parmi les prototypes implémentés, IMITATOR II implémente la méthode inverse et la cartographie pour les automates temporisés. Ce prototype nous a permis de synthétiser de bonnes valeurs pour les paramètres temporels de plusieurs études de cas, dont un modèle abstrait d’une mémoire commercialisée par le fabricant de puces STMicroelectronics, ainsi que plusieurs protocoles de communication. / This thesis proposes a novel approach for the synthesis of delays for timed systems, in particular in the framework oftimed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same timeabstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points of a bounded parameter domain, we are then able to partition the parametric space into good and bad zones, with respect to a given property one wants to verify. This gives a behavioral cartography of the system. This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Plusieurs outils ont été développé pour vérifier automatiquement les propriétés de sécurité sur des protocoles cryptographiques. Jusqu'à maintenant, la plupart de ces outils permettent de vérifier des propriétés de trace (ou propriétés d'accessibilité) tel que le secret simple ou l'authentification. Néanmoins, plusieurs propriétés de sécurité ne peuvent pas être exprimés en tant que propriété de trace, mais peuvent l'être en tant que propriété d'équivalence. L'anonymat, la non-tracabilité ou le secret fort sont des exemples classique de propriété d'équivalence. Typiquement, deux protocoles P et Q sont équivalent si les actions d'un adversaire (intrus) ne lui permettent pas de distinguer P de Q. Dans la littérature, plusieurs notions d'équivalence ont été étudiés, par exemple l'équivalence de trace ou l'équivalence observationnelle. Néanmoins, ces équivalences se relèvent être très difficiles à démontrer , d'où l'importance de développer des outils de vérification automatique efficaces de ces équivalences. Au sein de cette thèse, nous avons dans un premier temps travaillé sur une approche reposant sur des techniques de résolution de contraintes et nous avons créé un nouvel algorithme pour décider l'équivalence de trace entre deux protocoles pouvant contenir des conditionnelles avec branches "else", et pouvant également être non-déterministe. Cet algorithme a été appliqué sur des exemples concrets comme le "Private authentification protocol" ainsi que le "E-passport protocol". Cette thèse propose également des résultats de composition pour l'équivalence de trace. En particulier, nous nous sommes intéressé à la composition parallèle de protocoles partageant certains secrets. Ainsi dans cette thèse, nous avons démontré que, sous certaines conditions, la composition parallèle de protocoles préserve les propriétés d'équivalence. Ce résultat fut appliqué au "E-passport protocol". Enfin, cette thèse présente une extension à l'outil de vérification automatique ProVerif afin de démontrer automatiquement plus de propriétés d'équivalence. Cette extension a été implémenté au sein de ProVerif ce qui a permis de démontrer la propriété d'anonymat pour le "Private authentification protocol" . / Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools. We first worked on an approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol. We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties are preserved under parallel composition and under shared secrets. We applied our result on the e-passport protocol. At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allows us to automatically prove anonymity in the private authentication protocol.

Les protocoles de sécurité modernes peuvent impliquer un participant humain de façon à ce qu'il compare ou copie de courtes chaines de caractères faisant le pont entre différents appareils. C'est par exemple le cas des protocoles basés sur une authentification à facteur multiples comme les protocoles Google 2 factor ou 3D-Secure.Cependant, de telles chaines de caractères peuvent être sujettes à des attaques par force brute. Dans cette thèse nous proposons un modèle symbolique qui inclut les capacités de l'attaquant à deviner des secrets faibles et à produire des collisions avec des fonctions de hachage dont de l'application résulte une courte chaine de caractères. Nous proposons une nouvelle procédure de décision pour analyser un protocole (restreint à un nombre borné de sessions) qui se base sur de courtes chaines de caractères. Cette procédure a été intégré dans l'outil AKISS et testé sur les protocoles du standard ISO/IEC 9798-6:2010 / Modern security protocols may involve humans in order to compare or copy short strings betweendifferent devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-Secure are typical examplesof such protocols. However, such short strings may be subject to brute force attacks. In this thesis we propose asymbolic model which includes attacker capabilities for both guessing short strings, and producing collisions whenshort strings result from an application of weak hash functions. We propose a new decision procedure for analyzing(a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in theAKISS tool and tested protocols from the ISO/IEC 9798-6:2010 standard

L'Internet des objets est un principe selon lequel des clients sur Internet peuvent contacter des objets intelligents de notre quotidien, comme des capteurs de température d'une pièce ou des ampoules connectées. Ces objets sont contraints en mémoire, en capacité de calcul et aussi en capacité de communication (taille des paquets, médium partagé). Le travail effectué se focalise sur des problématiques liées à ces contraintes. Lorsqu'un client souhaite envoyer une commande à un objet, il a le choix de s'y connecter directement (architecture bout-en-bout) ou de se connecter à une passerelle réseau (non contrainte en mémoire et en calculs) qui jouera le rôle d'intermédiaire entre les clients et les objets (architecture maître-esclave). Le travail effectué consiste à comprendre les différences entre ces deux architectures et leur viabilité dans des réseaux de l'Internet des Objets. / The Internet of things is a network design where "things" are connected to the Internet, such as thermometers or lights. These objects are constrained in memory, computational capacity and communication (packet size, shared medium). The thesis is focused on issues around those constraints. A client willing to send a request to an object may either establish a direct connection to the object (end-to-end architecture) or establish a connection to the network gateway, which is not constrained in memory or computation capabilities, and will be used as a broker between clients and objects (master-slave architecture). This purpose of the thesis is to understand and to spotlight the differences between those two kinds of architectures and to determine their viability in an IoT context.

L'Internet sert de support de communication à un grand nombre d'applications dans le cadre des réseaux d'entreprise. Cependant, un certain nombre d'applications multimédia (e.g. téléphonie IP) nécessite un support de mécanisme de qualité de service dans le réseau. Chaque mécanisme du QoS est provisionné en fonction du contrat (SLA - Service Level Agreement) établit entre l'utilisateur/application et l'ISP (Internet Service Provider). Le rôle important de la gestion du QoS est de conserver toutes les caractéristiques établies par le SLA pendant toute la durée du contrat. Cette gestion peut être statique ou dynamique. Dans le cas statique, la gestion de la QoS dans le réseau est effectuée d'une manière expérimentale et non-efficace, manuellement par l'administrateur de réseau sur une grande échelle de temps. La gestion dynamique de la QoS est effectuée en utilisant des mécanismes adaptables et de façon automatique pour une gestion flexible et efficace des ressources du réseau. Dans cette thèse, nous considérons les éléments suivants qui compose de l'architecture pour la gestion dynamique des ressources : signalisation, algorithmes d'allocation de la bande passante et de contrôle de ressources, algorithmes de mesure des ressources dans le réseau, algorithmes de négociation entre plusieurs domaines. Nous proposons des critères de classification pour les protocoles QoS de signalisation en Internet et nous avons effectué une analyse des protocoles QoS les plus utilisés utilisant cette classification. Nous avons étudié l'impact entre les paramètres de SLA (bande passante, gigue, délai, perte des paquets) et les paramètres de différents mécanismes de QoS implémentés dans un réseau Linux Diffserv. En utilisant le réseau Linux Diffserv, nous montrons que la gestion statique de la QoS dans certains cas n'est pas efficace. Nous proposons un mécanisme d'allocation dynamique de la bande passante dans les routeurs à l'intérieur du réseau (Linux Diffserv). Avec notre algorithme nous proposons plusieurs règles de partage des ressources.

La problématique de la qualité de service dans les réseaux locaux sans fils IEEE 802.11 demeure l'un des défis délicats à surmonter par la communauté scientifique. L'étude et l'évaluation des approches apportés pour le support de QoS dans ce type de réseaux que ce soit par des simulations, des modèles analytiques ou des mesures réelles montre que ces approches sont toujours insuffisantes pour apporter des vraies garanties de qualité de services aux utilisateurs sans fils. Suite à des travaux effectués au CRAN qui ont porté sur l'équilibrage des charges dans les réseaux Ethernet industriels nous avons opté pour une méthode d'équilibrage de charges dans le contexte des réseaux hotspots 802.11. L'objectif de cette approche étant d'équilibrer les charges des points d'accès pour satisfaire aux besoins en termes de qualité de service de l'ensemble des applications sans fils. Ces besoins sont exprimés en termes de disponibilité, de délais, de bande passante...Nous avons alors définis un algorithme d'équilibrage de charges pouvant établir dynamiquement des associations optimales entre les utilisateurs présents dans un hotspot et les points d'accès en service. Un protocole d'échanges entre les stations sans fils et les points d'accès et entre ces derniers et le serveur d'équilibrage de charges a été établi. Le fonctionnement de ce protocole a été vérifié et simulé en utilisant les outils SDL et MSC. Pour l'évaluation de la performance de l'approche d'équilibrage par rapport à la méthode d'accès de base du protocole, un ensemble de simulations ont été effectués. Ces simulations effectuées sur OPNET montrent que cette approche permet d'améliorer un ensemble de paramètres de qualité de service perçue par les utilisateurs d'un réseau Hotspot.

Nous étudions la mise en œuvre du rendez-vous multiprocessus et de l'équité dans les langages du type csp généralise. Nous proposons une methode de construction des protocoles. Cette methode consiste a mettre en œuvre ces protocoles a partir d'un schéma de protocole, c'est-a-dire un protocole comportant des parties abstraites. La mise en œuvre effective d'un protocole se fait en remplaçant les parties abstraites par du code. Nous discutons le choix de ce code a l'aide d'exemples tires de la littérature. Nous étudions six notions d'équité dites classiques. Nous montrons que parmi ces six notions d'équité seules les notions d'équité dites fortes accroissent la vivacité. Nous montrons aussi qu'en général il est impossible de construire un protocole réalisant une de ces notions d'équité fortes: seule la strong process fairness peut l'être, et cela seulement lorsque le rendez-vous est binaire. Nous etudions la construction des protocoles réalisant la weak interaction fairness et la strong process fairness (avec rendez-vous binaire). Nous dérivons, a partir d'une spécification, un schéma pour chacune de ces notions d'équité

Étude de méthodes de spécification et vérification des protocoles de communication. La méthode de vérification mise en œuvre consiste a évaluer les spécifications du protocole sur un modèle fini qui le représente. Le langage de spécification est basé sur un mu calcul permettant l'expression aussi bien de comportements que de propriétés