Any organization, public or private, has to set up electronic services, for internal or external needs. These services have to guarantee a high level of security, either for protecting exchanged information, for authenticating the involved actors, or for guarantying the quality and correction of those services. Securing communications is in general provided by cryptographic protocols, but to prove that those protocols really achieve the required security properties is often very difficult. Some methods based on automated reasoning are defined to try to get those proofs, or to show some failures.