¿¿¿¿¿¿Pre¿t a¿ Voter provides a practical approach to end-to-end verifiable elections with a simple, familiar voter-experience. It assures a high degree of transparency while preserving secrecy of the ballot. Assurance arises from the auditability of the election itself, rather than the need to place trust in the system components. The original idea has undergone several revisions and enhancements since its inception in 2004, driven by the identification of threats, the availability of improved cryptographic primitives, and the desire to make the scheme as flexible as possible. This paper presents the key elements of the approach and describes the evolution of the design and their suitability in various contexts. We also describe the voter experience, and the security properties that the schemes provide.

This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder (1978) public key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs.

Security properties such as confidentiality and authenticity\ud may be considered in terms of the flow of\ud messages within a network. To the extent that this\ud characterisation is justified, the use of a process algebra\ud such as Communicating Sequential Processes (CSP)\ud seems appropriate to describe and analyse them. This\ud paper explores ways in which security properties may\ud be described as CSP specifications, how security mechanisms\ud may be captured, and how particular protocols\ud designed to provide these properties may be analysed\ud within the CSP framework. The paper is concerned\ud with the theoretical basis for such analysis. A sketch\ud verification of a simple example is carried out as an\ud illustration.