Cryptographic protocols are an essential building block to secure online communications. Relying on cryptographic primitives, such as encryption and digital signatures, these protocols typically guarantee security properties such as confidentiality and authenticity of communications. These properties are for instance basic goals of TLS, the most widely deployed cryptographic protocol, underlying all https Internet connections. Many modern applications may also need to guarantee properties related to users' privacy: such properties include anonymity and unlinkability (users cannot be traced) properties. History has however shown that cryptographic protocols are very error-prone and attackers have been able to exploit design and implementation flaws. The difficulty of designing and deploying secure protocols comes from an inherent asymmetry in security: while a protocol designer needs to think about all possible attacks, an attacker only needs to find a single weakness. Even on rather simple protocols, it is difficult for a human to explore all possible cases in a security proof when we take into account an attacker that has control of the underlying communication network and can intercept, modify and insert messages, in addition to the concurrent nature of the protocols. This task is even more complicated when requiring strong security properties that hold, or guaranteeing at least a degraded form of security, when parts of the system under study have been compromised. Therefore, it is essential to design algorithms that are able to automate security proofs, or automatically detect attacks in protocols. This approach, where messages are represented as first-order terms, in a symbolic model, was pioneered by Dolev and Yao and has been extremely successful, e.g., when analyzing new, upcoming security standards such as TLS 1.3 or 5G. The goal of this project is the development of efficient algorithms and tools for automated verification of cryptographic protocols, that are able to comprehensively analyse detailed models of real-world protocols building on techniques from automated reasoning. Automated reasoning is the subfield of AI whose goal is the design of algorithms that enable computers to reason automatically, and these techniques underlie almost all modern verification tools. Current analysis tools for cryptographic protocols do however not scale well, or require to (over)simplify models, when applied on real-world, deployed cryptographic protocols. We aim at overcoming these limitations: we therefore design new, dedicated algorithms, include these algorithms in verification tools, and use the resulting tools for the security analyses of real-world cryptographic protocols. The resulting tools will have increased efficiency, better automation and a wider scope. These developments will be driven by and validated on three classes of protocols: e-voting protocols, protocols for mobile devices from the 5G standard, and protocols for modern messaging applications, in particular the NOISE protocol framework. Our research is driven by the development of verification tools and their application to real-life protocols. Developing efficient, usable tools requires to develop solid, theoretical foundations, on the one hand, and evaluation on real-life case studies, on the other hand, to understand their limitations in practice. Our project will therefore be structured around the development of several, complementary tools that are developed in the PESTO research team, headed by Steve Kremer. On a more technical side, the methods developed in the project include symbolical reasoning on partially ordered traces, new algorithms for efficient subsumption in first-order Horn clause resolution, the design of equational reasoning techniques to enable support of associative, commutative operators and heuristics for guiding the state exploration to favor termination.