Security protocols aims at securing communications over untrusted networks such as Internet. Their design is notoriously error-prone, with flaws discovered years later. Formal methods have been successful in reasoning about the security of protocols and detect attacks. Automatic tools have been designed and applied to many protocols, from academic ones to deployed protocols such as SSL or Kerberos. In these lectures, we explain how security protocols can be modeled in symbolic models such as Horn clauses (a fragment of first-order logic) or applied-pi calculus (a process algebra). We describe and discuss decision techniques to automatically verify properties such as authentication or confidentiality.