Dans la plupart des systèmes radio, la correction des erreurs de transmission se base sur un protocole ARQ hybride (HARQ), qui combine un code correcteur d'erreurs (FEC) avec un protocole de retransmission (ARQ). La grande majorité des études portant sur l'HARQ se focalise essentiellement sur l'analyse et l'optimisation du code correcteur d'erreurs. Dans cette thèse, nous proposons une optimisation conjointe inter-couches du protocole ARQ hybride, en considérant à la fois des aspects de communications numériques et des aspects protocolaires. Dans les schémas HARQ classiques, dits simple paquet (SP), les paquets de redondance transmis sont tous relatifs au même paquet de données. Chaque retransmission réduit alors significativement le débit utile lorsque la taille des paquets est fixe. D'autre part, le débit est également très sensible à la présence d¿erreurs sur la voie retour. Nous proposons donc une nouvelle approche dite multi-paquets (MP), qui vise à réduire le nombre moyen de retransmissions par paquet grâce à la construction de paquets de redondance pouvant aider au décodage simultané de plusieurs paquets de données. Cette approche offre un gain significatif en débit par rapport aux schémas HARQ-SP lorsque le rapport signal à bruit (RSB) est suffisamment élevé. Les schémas HARQ classiques demeurent toutefois plus performants à faible RSB. Nous montrons par ailleurs que l'approche MP est plus robuste aux erreurs sur la voie de retour que l'approche SP. Ces résultats nous ont conduits à proposer un protocole hybride SP/MP qui bénéficie des avantages propres à chaque stratégie. Nous montrons par une analyse théorique ainsi que par simulation, que ce schéma hybride réalise un très bon compromis entre SP et MP sur toute la plage de RSB.

Nos travaux abordent le problème de l'efficacité des techniques d'implémentation hautes performances du système de communication. Car si les principes généraux sont désormais bien connus, il n'en va pas toujours de même de leur application. Des résultats obtenus sur notre plate-forme expérimentale, nous tirons des conclusions quant aux aspects machine hôte, système, et protocoles. Pour l'aspect machine hôte nous montrons que la parallélisation des piles de communication est décevante et grandement limitée par les contentions d'origine système. Nous montrons également comment la technique ILP, destinée à limiter les accès mémoire, peut être intégrée à la méthode d'accès d'une pile TCP/IP. Les bénéfices de cette technique restent largement dépendants des conditions d'utilisation, de la nature de l'application, et des manipulations de données. Du point de vue système, l'étude de deux environnements d'exécution de protocoles opposés, BSD et Streams, a permis d'identifier leurs faiblesses, et notamment pourquoi l'environnement Streams actuel n'est pas adapté aux hautes performances. Nous en déduisons un ensemble de principes qu'un environnement performant se doit de respecter. L'architecture de la pile de communication est essentielle. Nous montrons qu'une architecture démultiplexée, avec des chemins de données directs entre applications et drivers réseaux, permet un excellent support du contrôle de flux local et des mécanismes systèmes de QoS. En revanche, les implémentations de niveau utilisateur souffrent de nombreuses limitations. Elles sont cependant indispensables à certaines techniques. Du point de vue protocoles, nous montrons que la présence d'options dans les en-têtes de paquets n'est pas contraire à l'obtention de bonnes performances. A la notion trop rigide d'en-têtes de taille fixe nous substituons celle d'en-tétes de taille prédictible. Enfin, il ressort deux notions clés de ces travaux, la simplicité et la flexibilité, dont dépendent les performances et les fonctionnalités du système de communication.

Au cours des vingt dernières années, c'est une évolution très rapide non seulement en termes de nombre d'éléments inter-connectés mais surtout en termes de capacités des liens qui a pu être constatée au sein des réseaux de communications. A la création du réseau ARPANET en 1969, il y a plus de quarante ans, quatre ordinateurs, tous situés aux États-Unis étaient connectés avec des liens avec un débit de 50 kilobits par seconde. En 1986, à la création du réseau des universités américaines, le NSFNET, le nombre de machines dépassait déjà plusieurs milliers mais le débit des liens de coeur était encore de 56 kilobits par seconde. A partir de ce moment, la croissance à la fois en termes de nombre d'éléments inter-connectés et de capacités des liens a été exponentielle, grâce au succès de nouvelles applications populaires comme le WWW ou les avancées technologiques comme SDH, SONET ou DWDM dans le domaine des réseaux de fibres optiques et ATM et les protocoles DSL qui en dérivent. L'Internet actuel interconnecte des milliards d'utilisateurs (un demi-milliard de machines fin 2006) répartis partout dans le monde, pouvant utiliser des liens de coeur dont les débits cumulés sont supérieurs à plusieurs Térabits par seconde et dont les liens d'accès peuvent atteindre jusqu'à 10 Gigabits par seconde. Une autre évolution technologique fondamentale est que, aujourd'hui, certains liens d'accès ont des débits du même ordre de grandeur que les débits des liens de coeur auxquels ils sont connectés. Il est aujourd'hui courant de trouver des fermes de serveurs où les noeuds sont interconnectés avec des liens à 1 Gbps ou 10 Gbps et qui ont une connexion vers l'extérieur avec un débit similaire. Cette modification est importante car désormais quelques connexions suffisent à provoquer une saturation des liens de coeur. Cette situation risque d'empirer au fur et à mesure du remplacement des technologies DSL par la Fibre-Jusqu'à-La-Maison (FTTH). Des connexions à 5 Mbps agrégées sur des liens OC48 (2.5 Gbps) vont alors être remplacées par des connexions à 100 Mbps, voire 1 Gbps, agrégées sur des liens à 10 Gbps, voire moins suivant la technologie optique utilisée sur le réseau d'accès. Il est fort probable que dans de tels environnements des niveaux de congestion élevés ne soient pas rares, engendrant des perturbations pour de nombreuses applications. Un grand nombre d'applications prometteuses ont émergé et pourraient bénéficier de capacités de communication accrues, comme par exemple la Vidéo-à-la-Demande (VoD) qui permet aux utilisateurs de regarder des films en haute définition chez eux quand ils le désirent ou les expériences scientifiques générant des quantités massives de données (comme le LHC) qui doivent être acheminées dans des centres de calcul répartis tout autour du globe. L'interaction d'utilisateurs avec des objets distants via un réseau de communication ou Téléprésence commence également à prendre un rôle prépondérant dans de nombreux domaines allant du médical au militaire en passant par l'exploration spatiale. Mais ces applications sont encore construites au dessus de logiciels ou de protocoles à succès comme TCP et IP, conçus il y a longtemps pour un contexte de réseaux bas-débit. Le conception était dirigé par un but principal: fournir une interconnexion robuste entre des réseaux existants. Plongés maintenant dans un contexte de réseaux très haut-débit, ces protocoles extrêmement robustes et capables de passer à l'échelle sont toujours en activité mais commencent à montrer leurs limites en termes de performance, sécurité, fonctionnalités et flexibilité. L'exemple le plus typique est TCP au niveau de la couche de transport. TCP a été conçu comme un protocole ``à tout faire'' mais à mesure que la capacité des liens augmente dans les réseaux fixes, que les caractéristiques intrinsèques changent pour les réseaux sans fils et que les besoins des applications divergent, TCP n'est plus capable de permettre une utilisation performante pour tous des capacités nominales des liens du réseau. De nombreuses solutions ont été proposées, mais les concepteurs de protocoles d'aujourd'hui ont un large désavantage par rapport à ceux d'il y a quarante ans. Faire fonctionner ensemble quatre machines identiques n'est pas exactement pareil que concevoir un logiciel de communication ou protocole susceptible d'être utilisé entre des milliards de machines hétérogènes. Apporter du changement dans un système d'une telle ampleur est problématique: il n'est pas possible d'envisager une migration massive du jour au lendemain surtout si des équipements physiques sont concernés. Le changement ne peut être que graduel et via des mises à jour logicielles dans les hôtes d'extrémité. La peur d'un effondrement de l'Internet dû à la congestion comme à la fin des années 80 resurgit. Causés par une surabondance de trafic réseau sur des liens saturés, ces troubles ont mis en avant la nécessité d'introduire un mécanisme de contrôle de congestion dans les protocoles de transport. Si les nouvelles solutions introduites se comportent de façon égoïste quand elles partagent une ressource commune (un lien), alors cette peur est fondée. Il est donc nécessaire de fournir des moyens de vérifier si une solution donnée possède les propriétés adéquates avant de l'introduire dans un système partagé à très large échelle.

SSL/TLS, un protocole de sécurité datant de 1995, est devenu aujourd'hui une brique essentielle pour la sécurité des communications, depuis les sites de commerce en ligne ou les réseaux sociaux jusqu'aux réseaux privés virtuels (VPN), en passant par la protection des protocoles de messagerie électronique, et de nombreux autres protocoles. Ces dernières années, SSL/TLS a été l'objet de toutes les attentions, menant à la découverte de nombreuses failles de sécurité et à des améliorations du protocole. Dans cette thèse, nous commençons par explorer l'écosystème SSL/TLS sur Internet en énumérant les serveurs HTTPS sur l'espace IPv4; nous proposons pour cela des méthodologies de collecte et d'analyse permettant d'obtenir des résultats reproductibles et comparables entre différentes campagnes de mesure. Au-delà de ces observations, nous nous sommes intéressés en détail à deux aspects essentiels de la sécurité TLS: comment parer les attaques sur le Record Protocol, et comment implémenter des parsers sûrs et efficaces. Finalement, en se basant sur les nombreuses failles d'implémentation qui ont affecté presque toutes les piles TLS ces dernières années, nous tirons quelques enseignements concernant les difficultés liées à l'écriture d'une bibliothèque TLS de confiance / SSL/TLS, a 20-year old security protocol, has become a major component securing network communications, from HTTPS e-commerce and social network sites to Virtual Private Networks, from e-mail protocols to virtually every possible protocol. In the recent years, SSL/TLS has received a lot of attentions, leading to the discovery of many security vulnerabilities, and to protocol improvements. In this thesis, we first explore the SSL/TLS ecosystem at large using IPv4 HTTPS scans, while proposing collection and analysis methodologies to obtain reproducible and comparable results across different measurement campaigns. Beyond these observations, we focused on two key aspects of TLS security: how to mitigate Record Protocol attacks, and how to write safe and efficient parsers. Finally, building on the numerous implementation flaws in almost all TLS stacks in the last years, we propose some thoughts about the challenges in writing a secure TLS library

Titre de l'écran-titre (visionné le 17 avril 2023) / L'insuffisance cardiaque (IC) est un syndrome chronique où les personnes peuvent présenter des symptômes tels que la dyspnée et la fatigue (Jaarsma et al., 2021; McDonagh et al., 2022). La pratique des autosoins est requise notamment pour contribuer à stabiliser les symptômes, pour éviter des épisodes de décompensation et pour augmenter la qualité de vie (Jaarsma et al., 2021). Les autosoins sont définis par Riegel et al. comme étant « un processus de maintien de la santé grâce à des pratiques de promotion favorisant la santé et des pratiques de gestion de la maladie » (2012, p. 195, traduction libre). En plus de l'IC, 41 % de ces personnes sont atteintes d'un trouble neurocognitif (TNC) (Yap et al., 2022). En raison de l'effet combiné de l'IC et du TNC, la pratique des autosoins se veut plus difficile (Riegel et al., 2012). Ces personnes peuvent donc avoir besoin d'aide, et un suivi infirmier adapté à leurs besoins peut devenir nécessaire. Or, peu d'études publiées présentent les composantes d'interventions d'un suivi infirmier adapté à ces personnes (Hickman et al., 2020; Lovell et al., 2019). Aussi, les interventions sont peu explicitées, ce qui rend difficile leur transposition dans la pratique et au sein d'un groupe de personnes aux besoins diversifiés (Hickman et al. (2020). Pour ces raisons, la présente étude avait comme but d'élaborer un suivi infirmier permettant à des personnes atteintes d'IC et d'un TNC léger de pratiquer au quotidien des autosoins complexes requis par leur condition chronique. Les autosoins sont complexes en raison de la quantité (Kessing et al., 2019) et de l'implication de différents processus cognitifs (Riegel et al., 2012; Riegel et Dickson, 2008). La vision des soins infirmiers proposée par le modèle d'adaptation de Roy (2009) a servi d'assise à cette étude. Les postulats du modèle suggèrent de mettre à profit les capacités et les forces d'une personne malgré des capacités cognitives légèrement atténuées et des difficultés évidentes dans la pratique des autosoins, tout en soulignant la possibilité d'agir afin de favoriser un processus d'adaptation optimal. Pour ce faire, la méthode proposée par Sidani et Braden (2011) a été employée afin de développer un protocole d'interventions infirmières pour des personnes atteintes d'IC et d'un TNC léger. Les 4 phases suivantes ont été consacrées à l'élaboration du protocole, soit la compréhension du problème (phase 1), l'identification et l'élaboration des interventions appropriées (phase 2), le développement du protocole d'interventions infirmières (phase 3), ainsi que la conduite d'un projet pilote. Ce dernier a permis de raffiner le protocole d'interventions; d'évaluer son acceptabilité, sa faisabilité, de même que les capacités des indicateurs de résultats sélectionnés à saisir les changements de l'application du protocole d'interventions infirmières (phase 4). Des entrevues avec des personnes aux prises avec l'IC et un TNC, et des professionnels de la santé, appuyées par les résultats d'études empiriques et le recours à des théories en mesure d'expliquer les résultats obtenus, ont permis de cibler des besoins et des interventions. L'analyse des données expérientielles, empiriques et théoriques des deux premières phases a donné le moyen d'élaborer le protocole d'interventions infirmières, et le projet pilote a permis d'en raffiner le contenu. Les phases de la méthode de Sidani et Braden (2011) ont mis en lumière des éléments importants devant être intégrés dans un suivi infirmier auprès de la population atteinte d'IC et d'un TNC. Les résultats de cette étude suggèrent qu'un suivi infirmier régulier, à domicile et à long terme, est à privilégier. Les résultats ont également fait valoir que l'enseignement doit s'étendre au-delà des recommandations standards, que les opérations cognitives liées à la pratique des autosoins doivent être soutenues et, surtout, que la pratique des autosoins doit être contextualisée dans la vie quotidienne de la personne. Les résultats ont fait valoir comment la présence d'un proche s'avère indispensable à la pratique des autosoins. Au final, le projet pilote a permis de compléter la phase d'élaboration du protocole d'interventions infirmières en plus de montrer qu'il est acceptable et faisable pour soutenir la pratique des autosoins des personnes atteintes d'IC et d'un TNC. / Heart failure is a chronic condition which could cause symptoms such as dyspnea and fatigue (Jaarsma et al., 2021). The person with heart failure (HF) can help stabilize symptoms, avoid decompensation, and enhance quality of life by managing his or her chronic disease, particularly through self-care (Jaarsma et al., 2021). Self- care is defined as « a process of maintaining health through heath promoting practices and managing illness » (Riegel et al., 2012, p.195). However, the practice of self-care is influenced by mild cognitive impairment (MCI) common in heart failure patients, affecting 41 % of that population (Yap et al., 2022). HF associated with MCI can make self-care practice more difficult (Riegel et al., 2012). Thus, these people may need assistance, and a nursing follow-up adapted to their needs may become necessary. However, few published studies present the intervention components of a nursing follow-up adapted to these people (Hickman et al., 2020; Lovell et al., 2019). Also, in those studies, the interventions are poorly explained, which makes it difficult to transpose them into practice and to a group of people with diverse needs (Hickman et al., 2020). For these reasons, the aim of the present study was to develop a nursing follow-up that would allow people with HF and MCI to practice the complex self-care required by their chronic condition on a daily basis. The vision of nursing care proposed by Roy's (2009) adaptation model served as the basis for this study. The model's postulates suggest building on a person's abilities and strengths despite slightly impaired cognitive abilities and obvious difficulties in practicing self-care, while emphasizing the possibility of taking actions to promote an optimal adaptation process. To this end, the method proposed by Sidani and Braden (2011) was used to develop a nursing follow-up protocol for people with HF and MCI. The following 4 phases are devoted to the development of the nursing interventions protocol: understanding the problem (phase 1), identifying and developing appropriate interventions (phase 2), developing the intervention protocol (phase 3), as well as conducting a pilot project to refine the protocol; assess its acceptability, feasibility and outcome indicator capabilities; and capture changes during the implementation of the nursing interventions protocol (phase 4). Interviews with people with HF and MCI, and health professionals, supported by empirical research findings and the use of theories to explain the findings, were used to target needs and interventions. Analysis of the experiential, empirical and theoretical data from the first two phases led to the development of the nursing interventions protocol, and the pilot project helped to refine its content. The phases of Sidani and Braden's (2011) method highlighted important elements that should be incorporated into a nursing follow-up for population with HF and MCI. The results of this study suggest that regular, home- based, long-term follow-up is preferred. The results also suggested that teaching should extend beyond standard recommendations, that cognitive operations related to self-care practice should be supported, and, most importantly, that self-care practice should be contextualized in the person's daily life. The results underline how the presence of a relative is indispensable for the practice of self-care. In the end, the pilot project completed the nursing interventions protocol development phase and showed that it is acceptable and feasible to support the practice of self-care for people with HF and MCI.

<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