Inductive Proofs
Approach: like proofs of program correctness
- Induction to prove “loop invariant”
State-transition model, objective is security invariant
General-purpose specification/verification system support
- Kemmerer, using Ina Jo and ITP [Kem89] (the first)
- Paulson, using Isabelle [Paul98] (the new wave)
- Dutertre and Schneider, using PVS [DS97]
- Bolignano, using Coq [Bol97]
Can also be done manually [Sch98, THG98]
- Contributed to better understanding of invariants
- Much more complex than belief logic proofs
Full guarantee of correctness (with respect to model)
- Proofs include confidentiality