08-Inductive Method.pdf

1Protocol Verification by the Inductive Method John Mitchell CS 259 Analysis Techniques Crypto Protocol Analysis Formal Models Computational Models Modal Logics Model Checking Inductive Proofs Dolev-Yao (perfect cryptography) Random oracle Probabilistic process calculi Probabilistic I/O automata … Finite processes, finite attacker Process Calculi … Finite processes, infinite attacker Spi-calculusBAN logic Recall: protocol state space
Participant + attacker actions define a state transition graph
A path in the graph is a trace of the protocol
Graph can be ? Finite if we limit number of agents, size of message, etc. ? Infinite otherwise ... ... Analysis using theorem proving
Correctness instead of bugs ? Use higher-order logic to reason about possible protocol executions
No finite bounds ? Any number of interleaved runs ? Algebraic theory of messages ? No restrictions on attacker
Mechanized proofs ? Automated tools can fill in parts of proofs ? Proof checking can prevent errors in reasoning [Paulson] Inductive proofs
Define set of traces ? Given protocol, a trace is one possible sequence of events, including attacks
Prove correctness by induction ? For every state in every trace, no security condition fails – Works for safety properties only ? Proof by induction on the length of trace Two forms of induction
Usual form for ?n∈Nat. P(n) ? Base case: P(0) ? Induction step: P(x) ? P(x+1) ? Conclusion: ?n∈Nat. P(n)
Minimial counterexample form ? Assume: ?x [ ?P(x) ∧ ?yx. P(y) ] ? Prove: contraction ? Conclusion: ?n∈Nat. P(n) Both equivalent to “the natural numbers are well-ordered” 2Use second form
Given set of traces ? Choose shortest sequence to bad state ? Assume all steps before that OK ? Derive contradiction – Consider all possible steps All states are good Bad state Sample Protocol Goals
Authenticity: who sent it? ? Fails if A receives message from B but thinks it is from C
Integrity: has it been altered? ? Fails if A receives message from