## The Inductive Approach to Verifying Cryptographic ProtocolsAbstract: "Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state systems. Proofs are generated using Isabelle/HOL. The human effort required to analyze a protocol can be as little as a week or two, yielding a proof script that takes a few minutes to run. Protocols are inductively defined as sets of traces. A trace is a list of communication events, perhaps comprising many interleaved protocol runs. Protocol descriptions incorporate attacks and accidental losses. The model spy knows some private keys and can forge messages using components decrypted from previous traffic. Three protocols are analyzed below: Otway-Rees (which uses shared-key encryption), Needham-Schroeder (which uses public-key encryption), and a recursive protocol [9] (which is of variable length). One can prove that event ev always precedes event ev ́or that property P holds provided X remains secret. Properties can be proved from the viewpoint of the various principals: say, if A receives a final message from B then the session key it conveys is good." |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Common terms and phrases

add the event analz and synth analz H analz spies evs bad agents BAN logic Belief logics certificates components Crypt KX Crypt(shrK cryptographic protocols datatype decryption defined encrypted messages event Says evs2 evs4 evsl Fake form Crypt(pubK form Says Formal verification forwarding lemma fraudulent messages fresh nonce honest agent inductive definition INonce Isabelle Isabelle/HOL Kab}Ka key compromise theorem key Kcs key secrecy theorem long-term keys message Crypt(pubK model checking Nb}Kb Needham-Schroeder Nonce NB Oops message otway Otway-Rees protocol parts({X parts(spies evs Possibility Properties private keys proof script protocol descriptions protocol runs protocol steps proved by induction Proving Guarantees public keys recursive authentication protocol recursive protocol regularity lemma remains secret replay attack respond evs rewrite rules Roger Needham Says B A sending server session key compromise session key Kab session key secrecy set evs set evs3 shrK simplify specify subgoal Symbolic evaluation synth H trivial uncompromised unicity