This chapter uses the applied π-calculus to model threats. The need to explicitly model sessions with both honest and compromised agents is justified via famous examples. Attacks are explained formally and the use of tools for automation is covered. To address the problem that adversaries can inject infinitely many inputs, the sequent calculus is introduced to calculate meaningful inputs. The operational semantics of the applied π-calculus is enhanced with constraints, defined using sequents and inequalities. The enhanced semantics is applied to calculate an attack on the secrecy of a nontrivial protocol. Cut elimination for the sequent calculus is introduced and its role in proving secrecy is illustrated on an example. Exercises apply the threat models and methods to further protocols.