An Extension of CryptoPAi to the Formal Analysis of E-voting Protocols

Abstract

CryptoPAi is a hybrid operational-epistemic framework for specification and analysis of security protocols with genuine support for cryptographic constructs. This framework includes a process algebraic formalism for the operational specification and an epistemic extension of modal mu-calculus with past for the property specification. In this paper, we extend CryptoPAi framework with more cryptographic constructs. The main practical motivation for this work came from the domain of e-voting protocols and then we investigate the applicability of the extended framework in this domain. The framework provides explicit support for cryptographic constructs, which is among the most essential ingredients of security and e-voting protocols. Some more advanced cryptographic constructs are provided to allow specifying the behavior of<br />more protocols in our process language and then verifying properties expressed in our logic with both temporal and epistemic operators.We apply our extended framework to the FOO e-voting protocol. We also promote the prototype model-checker of the framework in the Maude rewriting logic tool and apply it to model-check some specified properties on their corresponding models.