|
14:00 to 14:45, Seminar Hall Existential Assertions for Voting Protocols Vaishnavi Sundararajan Chennai Mathematical Institute. 03-04-17 Abstract Cryptographic protocols often involve certification, that is, agents sending each other certain facts about terms -- for example, an agent may wish to tell another that an encrypted secret was actually chosen from a particular set of values. In protocols based on the popular Dolev-Yao model, certification is often modelled via sequences of terms, or by introducing new cryptographic primitives to capture these statements. In a previous paper, we extended the Dolev-Yao model with ``assertions'', allowing agents to communicate both basic messages (terms) as well as statements about them (assertions). This separation of communications into two sorts was done with a view to simplifying the logical analysis of protocols. In this paper, we build on that work and add a few new constructs -- most importantly, existential abstraction -- to the assertion language, which allows us to translate common requirements in voting protocols into proof properties. We also give an equivalence-based definition of anonymity in this model, and prove anonymity for the FOO protocol. This is joint work with Prof R Ramanujam (IMSc) and Prof S P Suresh (CMI), and has been accepted for presentation at the 2nd Workshop on Advances in Secure Electronic Voting Schemes 2017.
|
