Our information society notably relies on secure information exchanges typically achieved by security protocols. Given, their ubiquitous and critical nature, we need guarantees that they meet their goals such as privacy properties. Ideally, those guarantees are established via formal methods providing mathematical frameworks to analyse security protocols. However, existing methods suffer from scalability and precision issues that the present thesis aims to address. First, to mitigate the scalability problem, we develop partial order reduction techniques enabling to dramatically reduce the search space to explore when analysing security protocols. Second, we solve a critical precision issue by adopting a privacy via sufficient conditions approach. We show that two well-designed and easily verifiable conditions always imply unlinkability and anonymity. We confirm the practical relevance of our contributions by implementing them and using them for analysing real-life security protocols, finding new attacks and establishing new proofs.