The paper presents an inductive approach to verifying cryptographic protocols, using inductive definitions and the theorem prover Isabelle/HOL. The method is based on ordinary predicate calculus and can handle infinite-state systems. Protocols are defined as sets of traces, where a trace is a list of communication events. The attacker is modeled using inductively defined operators: *parts* for returning all components of a set of messages, *analz* for decrypting past traffic, and *synth* for forging messages. Properties are proved by induction on traces, with each case considering a possible state of the system. The approach is applied to three protocols: Otway-Rees (shared-key encryption), Needham-Schroeder (public-key encryption), and a recursive protocol. The paper discusses the modeling of protocols, standard rules, induction, regularity lemmas, secrecy theorems, and finding attacks. The inductive definitions and proof techniques are tailored to Isabelle/HOL, and the paper provides detailed examples of how these are implemented and used to prove properties of the protocols.The paper presents an inductive approach to verifying cryptographic protocols, using inductive definitions and the theorem prover Isabelle/HOL. The method is based on ordinary predicate calculus and can handle infinite-state systems. Protocols are defined as sets of traces, where a trace is a list of communication events. The attacker is modeled using inductively defined operators: *parts* for returning all components of a set of messages, *analz* for decrypting past traffic, and *synth* for forging messages. Properties are proved by induction on traces, with each case considering a possible state of the system. The approach is applied to three protocols: Otway-Rees (shared-key encryption), Needham-Schroeder (public-key encryption), and a recursive protocol. The paper discusses the modeling of protocols, standard rules, induction, regularity lemmas, secrecy theorems, and finding attacks. The inductive definitions and proof techniques are tailored to Isabelle/HOL, and the paper provides detailed examples of how these are implemented and used to prove properties of the protocols.