## Security Theorems via Model Theory

 Joshua Guttman (Worcester Polytechnic Institute)

 A model-theoretic approach can establish security theorems for cryptographic protocols. Formulas expressing authentication and non-disclosure properties of protocols have a special form. They are quantified implications for all xs . (phi implies for some ys . psi). 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 phi is the antecedent of a security goal, then there is a skeleton A_phi such that, for every skeleton B, phi is satisfied in B iff there is a homomorphism from A_phi to B. (2) A protocol enforces for all xs . (phi implies for some ys . psi) iff every realized homomorphic image of A_phi satisfies psi. Hence, to verify a security goal, one can use the Cryptographic Protocol Shapes Analyzer CPSA (TACAS, 2007) to identify minimal realized skeletons, or "shapes," that are homomorphic images of A_phi. If psi holds in each of these shapes, then the goal holds.

In Sibylle Fröschle and Daniele Gorla: Proceedings 16th International Workshop on Expressiveness in Concurrency (EXPRESS 2009), Bologna, Italy, 5th September 2009, Electronic Proceedings in Theoretical Computer Science 8, pp. 51–65.
Published: 17th November 2009.

 ArXived at: http://dx.doi.org/10.4204/EPTCS.8.5 bibtex PDF

 Comments and questions to: eptcs@eptcs.org For website issues: webmaster@eptcs.org