The rise of the Internet and the ubiquity of electronic devices have changed our daily life. Nowadays, almost all the services have a digital counterpart (e.g. electronic voting, messaging, electronic commerce). Unfortunately, this digitalization of the world comes with tremendous risks for our security and privacy. The risks are even more important on digital systems compared to non-digital ones since a security flaw can lead to large scale frauds even with limited ressources. To secure these applications, various cryptographic protocols have been deployed (e.g., TLS, Verified-by-Visa, Signal's secure messaging protocol, and Bitcoin's blockchains). However, these protocols sometimes contain security flaws which can be exploited with important socio-economic consequences (e.g. linkable French electronic passport, flaws in TLS). In fact, the design and analysis of security protocols is notoriously difficult since it requires to consider any possible malicious adversary interacting with the protocol. Formal methods have been shown successful in proving protocols and finding flaws. For example while formalizing the voting protocol Helios in a symbolic model, Cortier and Smyth have identified a flaw in the protocol which allows an adversary to compromise the vote-privacy of a given voter. However manually proving the security of cryptographic protocols is hard and error-prone. Hence, a large variety of automated verification tools have been developed to prove or find attacks on protocols. These tools differ in their scope, degree of automation and attacker models. Despite the large number of automated verification tools, several cryptographic protocols still represent a real challenge for these tools and reveal their limitations. This is particularly the case for stateful protocols, i.e., protocols that require participants to remember information over different sessions, and protocols that rely on cryptographic primitives with complex algebraic properties (e.g., blind signatures, exclusive-or). To cope with these limits, each tool focuses on different classes of protocols depending on the primitives, the security properties, etc. Moreover, the tools cannot interact with each other as they evolve in their own model with specific assumptions. Thus, even though it is already challenging to choose the best suited tool amongst the plethora of existing ones for a given protocol, it is also impossible to prove a protocol relying on different verifiers even when different parts of the protocol could be handled by different tools. The aim of this project is to get the best of all these tools, meaning, on the one hand, to improve the theory and implementations of each individual tool towards the strengths of the others and, on the other hand, build bridges that allow the cooperations of the methods/tools. We will focus in this project on the tools CryptoVerif, EasyCrypt, Scary, ProVerif, Tamarin, AKiSs and APTE. (As France is one of the most advanced countries in the development of such tools, most of these tools are French, but some are international: EasyCrypt, Tamarin.) In order to validate the results obtained in this project, we will apply our results to several case studies such as the Authentication and Key Agreement protocol from the telecommunication networks, the Scytl and Helios voting protocols, and the low entropy authentication protocols 3D-Secure. These protocols have been chosen to cover many challenges that the current tools are facing.