Insecurity, going from terms to formulas

Reasoning about cryptographic protocols starts with a term algebra of communicated terms over which an appropriate logic is built, with variables designating terms. In logics of announcements, formulas are communicated, blurring the distinction between terms and formulas. Constructs such as zero knowledge proofs and certificates are akin to formulas, motivating a similar extension to reasoning about security protocols as well. However, the interaction between equality and the existential quantifier leads to interesting twists: witnesses for existential quantifiers may be unbounded, and obtaining small witness terms while maintaining equality proofs complicates the analysis considerably. In this talk we attempt to highlight the challenges in reasoning about insecurity when formulas are communicated. This work is joint with Vaishnavi Sundararajan and S P Suresh.