<p>Ova teza se bavi &curren;-kvazilinearnim varijetetima grupoida. Pokazano je da postoji ta&middot;cno dvadeset osam idempotentnih &curren;-kvazilinearnih varijeteta grupoida, od kojih dvadeset &middot;sest varijeteta imaju kona&middot;cnu bazu i te baze su i navedene, dok preostala dva varijeteta imaju inherentno beskona&middot;cnu bazu. U tezi je opisano ured enje svih idempotentnih &curren;-kvazilinearnih varijeteta grupoida i nalazimo male grupoide koji generi&middot;su svaki od navedenih varijeteta. Na kraju je pokazano da postoji kontinum mnogo &curren;-kvazilinearnih variejeteta grupoida.</p> / <p>The topic of this thesis are &curren;-quasilinear varieties of groupoids.<br />We show that there exist exactly twenty-eight idempotent &curren;-quasilinear varieties of groupoids, twenty-six of which are &macr;nitely based (and we explicitly<br />give &macr;nite bases for each of them), while two are inherently non&macr;nitely based.<br />We describe the ordering of these twenty-eight idempotent &curren;-quasilinear varieties of groupoids and &macr;nd small generating algebras for each of them. In<br />the end we show that there exist continuum many &curren;-quasilinear varieties of<br />groupoids, not all of which are even locally &macr;nite.</p>

Le lambda-calcul est un formalisation de la notion de calcul. Dans cette thèse nous nous intéresserons à certaines variantes non déterministes, et nous nous pencherons plus particulièrement sur le cas probabiliste.L'étude du lambda-calcul probabiliste n'est pas nouvelle, mais les travaux précédents considéraient le comportement probabiliste comme un effet de bord. Notre objectif est de présenter ce calcul d'une manière plus équationnelle, en intégrant le comportement probabiliste à la réduction.Tout d'abord nous définissons une sémantique opérationnelle déterministe et contextuelle pour le lambda-calcul probabiliste en appel par nom. Afin de traduire la signification de la somme nous définissons une équivalence syntaxique dans notre calcul, dont nous démontrons qu'il ne déforme pas la réduction: considérer une réduction modulo équivalence revient à considérer simplement le résultat du calcul modulo équivalence. Nous prouvons également un résultat de standardisation.Dans ce cadre nous définissons une notion de théorie équationnelle pour le lambda-calcul probabiliste. Nous étendons certaines notions usuelles, et en particulier celle de bon sens. Cette dernière se formalise facilement dans un cadre déterministe mais est bien plus complexe dans le cas probabiliste.Pour finir nous prouvons une correspondance entre l'équivalence observationnelle, l'égalité des arbres de Böhm et la théorie cohérente sensée maximale. Nous définissons une notion d'arbres de Böhm probabilistes dont nous prouvons qu'elle forme un modèle. Nous démontrons ensuite un résultat de séparabilité disant que deux termes avec des arbres de Böhm distincts ne sont pas observationnellement équivalents. / The lambda-calculus is a way to formalize the notion of computation. In this thesis we will be interested in some of these variants introducing non deterministim, and we will focus mostly on a probabilistic calculus.The probabilistic lambda-calculus has been studied for some time, but the probabilistic behaviour has always been treated as a side effect. Our purpose is to give a more equational representation of this calculus, by handling the probabilities inside the reduction rather than as a side effect.To begin with we give a deterministic and contextual operational semantics for the call-by-name probabilistic lambda-calculus. To express the probabilistic behaviour of the sum we introduce a syntactic equivalence in our calculus, and we show it has little consequence on the calculus: reducing modulo equivalence amount to reducing and then looking at the result modulo equivalence. We also prove a standardization theorem.Then using this operational semantics we define a notion of equational theories for the probabilistic lambda-calculus. We extend some usual notions to this setting, and in particular the sensibility of a theory. This notion is quite simple in a deterministic setting but becomes more complicated when we have a probabilistic computation.Finally we prove a generalization of the equality between the observational equivalence, the Böhm tree equality and the maximal coherent sensible lambda-theory. We give a notion of probabilistic Böhm trees, and prove that this forms a model of the probabilistic lambda-calculus. Then we prove a separability result stating that two terms with different Böhm trees are separable, i.e. are not observationally equivalent.

Tesis por compendio / [ES] La herramienta criptográfica Maude-NPA es un verificador de modelos especializado para protocolos de seguridad criptográficos que tienen en cuenta las propiedades algebraicas de un sistema criptográfico. En la literatura, las propiedades criptográficas adicionales han descubierto debilidades de los protocolos de seguridad y, en otros casos, son parte de los supuestos de seguridad del protocolo para funcionar correctamente. Maude-NPA tiene una base teórica en la rewriting logic, la unificación ecuacional y el narrowing para realizar una búsqueda hacia atrás desde un patrón de estado inseguro para determinar si es alcanzable o no. Maude-NPA se puede utilizar para razonar sobre una amplia gama de propiedades criptográficas, incluida la cancelación del cifrado y descifrado, la exponenciación de Diffie-Hellman, el exclusive-or y algunas aproximaciones del cifrado homomórfico. En esta tesis consideramos nuevas propiedades criptográficas, ya sea como parte de protocolos de seguridad o para descubrir nuevos ataques. También hemos modelado diferentes familias de protocolos de seguridad, incluidos los Distance Bounding Protocols or Multi-party key agreement protocolos. Y hemos desarrollado nuevas técnicas de modelado para reducir el coste del análisis en protocolos con tiempo y espacio. Esta tesis contribuye de varias maneras al área de análisis de protocolos criptográficos y muchas de las contribuciones de esta tesis pueden ser útiles para otras herramientas de análisis criptográfico. / [CA] L'eina criptografica Maude-NPA es un verificador de models especialitzats per a protocols de seguretat criptogràfics que tenen en compte les propietats algebraiques d'un sistema criptogràfic. A la literatura, les propietats criptogràfiques addicionals han descobert debilitats dels protocols de seguretat i, en altres casos, formen part dels supòsits de seguretat del protocol per funcionar correctament. Maude-NPA te' una base teòrica a la rewriting lògic, la unificació' equacional i narrowing per realitzar una cerca cap enrere des d'un patró' d'estat insegur per determinar si es accessible o no. Maude-NPA es pot utilitzar per raonar sobre una amplia gamma de propietats criptogràfiques, inclosa la cancel·lació' del xifratge i desxifrat, l'exponenciacio' de Diffie-Hellman, el exclusive-or i algunes aproximacions del xifratge homomòrfic. En aquesta tesi, considerem noves propietats criptogràfiques, ja sigui com a part de protocols de seguretat o per descobrir nous atacs. Tambe' hem modelat diferents famílies de protocols de seguretat, inclosos els Distance Bounding Protocols o Multi-party key agreement protocols. I hem desenvolupat noves tècniques de modelització' de protocols per reduir el cost de l'analisi en protocols amb temps i espai. Aquesta tesi contribueix de diverses maneres a l’àrea de l’anàlisi de protocols criptogràfics i moltes de les contribucions d’aquesta tesi poden ser útils per a altres eines d’anàlisi criptogràfic. / [EN] The Maude-NPA crypto tool is a specialized model checker for cryptographic security protocols that take into account the algebraic properties of the cryptosystem. In the literature, additional crypto properties have uncovered weaknesses of security protocols and, in other cases, they are part of the protocol security assumptions in order to function properly. Maude-NPA has a theoretical basis on rewriting logic, equational unification, and narrowing to perform a backwards search from an insecure state pattern to determine whether or not it is reachable. Maude-NPA can be used to reason about a wide range of cryptographic properties, including cancellation of encryption and decryption, Diffie-Hellman exponentiation, exclusive-or, and some approximations of homomorphic encryption. In this thesis, we consider new cryptographic properties, either as part of security protocols or to discover new attacks. We have also modeled different families of security protocols, including Distance Bounding Protocols or Multi-party key agreement protocols. And we have developed new protocol modeling techniques to reduce the time and space analysis effort. This thesis contributes in several ways to the area of cryptographic protocol analysis and many of the contributions of this thesis can be useful for other crypto analysis tools. / This thesis would not have been possible without the funding of a set of research projects. The main contributions and derivative works of this thesis have been made in the context of the following projects: - Ministry of Economy and Business of Spain : Project LoBaSS Effective Solutions Based on Logic, Scientific Research under award number TIN2015-69175-C4-1-R, this project was focused on using powerful logic-based technologies to analyze safety-critical systems. - Air Force Office of Scientific Research of United States of America : Project Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA Scientific Research under award number FA9550-17-1-0286 - State Investigation Agency of Spain : Project FREETech: Formal Reasoning for Enabling and Emerging Technologies Scientific I+D-i Research under award number RTI2018-094403-B-C32 / Aparicio Sánchez, D. (2022). Modeling and Analysis of Advanced Cryptographic Primitives and Security Protocols in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/190915 / Compendio