Security theorems via model theory
Joshua D. Guttman · 2009
A model-theoretic approach can establish security theorems, which are formulas expressing authen-tication and non-disclosure properties of protocols. Security theorems have a special form, namely quantified implications ∀~x.(φ ⊃ ∃~y.ψ). Models (interpretations) for these formulas are skeletons, partially ordered structures consisting of a number of local protocol behaviors. Realized skeletons contain enough local sessions to explain all the behavior, when combined with some possible adversary behaviors. We show two results. (1) If φ is the antecedent of a security goal, then there is a skeleton Aφ such that, for every skeleton B, φ is satisfied in B iff there is a homomorphism from Aφ to B. (2) A protocol enforces ∀~x.(φ ⊃ ∃~y.ψ) iff every realized homomorphic image of Aφ satisfies ψ. Since the program CPSA finds the minimal realized skeletons, or “shapes, ” that are homomorphic images of Aφ, if ψ holds in each of these shapes, then the goal holds. 1