Meta-CLF 2

2018

Carsten Schürmann: A framework for studying vote secrecy in elections, World Congress on Political Science, Panel Electoral integrity and the Quest for Secret Voting as part of the General Session on Electoral Integrity (GS05), Brisbane, Australia, July 2018.
In this draft paper, we study the role of vote secrecy in elections. Besides election integrity, vote secrecy is the second defining characteristics of genuine and credible elections. Modern vote casting methods, including internet voting and optical ballot scanners are game changers in terms of understanding and guaranteeing vote secrecy. This is because the concerns of election integrity can no longer be cleanly separated from vote secrecy, as it used to be the case for pen-and-paper election in controlled environments. Many modern election methods resolve this tension by regarding election integrity as more important than vote secrecy. Universal verifiable systems for example, are designed with election integrity in mind; but a universal verifiable election technology may break vote secrecy. To study this phenomenon in a bit more in detail, we present in this draft paper a framework and demonstrate it using three election methods, pen-and-paper voting, internet voting, and optical scan voting.
Carsten Schürmann: Rounding considered harmful, Third International Joint Conference on Electronic Voting (E-Vote-ID'18), Bregenz, Austria, October 2018.
Party-list proportional representation methods aim to allocate seats proportionally to the votes cast for each party. In general, exact proportionality is not possible as it would require a fractional allocation of seats. Therefore several methods have been devised to compute seat allocations that differ in the way they try to achieve proportionality. Examples of such methods include the d’Hondt and Sainte-Laguë methods that allocate seats according to fractional values. These methods are used in many countries. Numerically, these fractions appear harmless, however they are not. Computers do not work with infinite precision floating point numbers, implementations tend to round the fractions to several digits, which can, with a certain probability, lead to incorrect seat allocations.
Alessandro Bruni, Thorvald Sahl Jørgensen, Theis Grønbech Petersen, and Carsten Schürmann: Formal verification of ephemeral Diffie-Hellman over COSE (EDHOC), 4th International Conference on Security Standardisation Research (SSR’18), Darmstadt, Germany, November 2018.
Ephemeral Diffie-Hellman over COSE (EDHOC) is an authentication protocol that aims to replace TLS for resource constrained Internet of Things (IoT) devices using a selection of lightweight ciphers and formats. It is inspired by the newest Internet Draft of TLS 1.3 and includes reduced round-trip modes. Unlike TLS 1.3, EDHOC is designed from scratch, and does not have to support legacy versions of the protocol. As the protocol is neither well-known nor has been used in practice it has not been scrutinized to the extent it should be. The objective of this paper is to verify security properties of the protocol, including integrity, secrecy, and perfect forward secrecy properties. We use ProVerif to analyze these properties formally. We describe violations of specific security properties for the reduced round-trip modes. The flaws were reported to the authors of the EDHOC protocol
Iliano Cervesato, Sharjeel Khan, Giselle Reis, and Dragiša Žunić: Formalization of Automated Trading Systems in a Concurrent Linear Framework, 2018 Joint Workshop on Linearity & TLLA, Oxford, UK, July, 2018.
We present a declarative and modular specification of an automated trading system (ATS) in the concurrent linear framework CLF. We implemented it in Celf, a CLF type checker which also supports executing CLF specifications. We outline the verification of a representative property of trading systems using generative grammars, an approach to reasoning about CLF specifications.
Carlos Olarte, Valeria de Paiva, Elaine Pimentel, and Giselle Reis: Benchmarking Linear Logic Translations, 2018 Joint Workshop on Linearity & TLLA, Oxford, UK, July, 2018.
Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we seek to start a discussion of benchmarks for Girard's linear logic and some of its variants. For some quick bootstrapping of the collection of problems, we use translations of the collection of Kleene’s intuitionistic theorems in the traditional monograph Introduction to Metamathematics. We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using linear logic based provers with focusing.

2017

Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Carsten Schürmann: An Introduction to Voting Rule Verification, In Ulle Endriss (editor), Trends in Computational Social Choice, Cambridge University Press, October, 2017.
Social choice functions (or more specifically voting rules) form the backbone of modern democracies. They are often expressed as algorithms palatable for machine implementation and execution, and simultaneously they control the transfer of power from the people to a government. Social choice functions vary in complexity and exhibit different behaviors and properties. For scientists, they are perfect objects of study, in particular, to predict the way they behave, to understand corner cases, or to check that they comply with the law. Conversely, for agents (or voters) the functions’ behavior and which properties they satisfy or Violate often hard to discern and difficult to understand.
Stefan Patachi and Carsten Schürmann: Eos — a universal verifiable and coercion resistant voting protocol, Proceedings on the International Conference on Electronic Voting (E-Vote-ID'17) Bregenz, Austria, October 2017.
We present the voting protocol Eos that is based on a conditional linkable ring signatures scheme. Voters are organized in rings allowing them to sign votes anonymously. Voters may assume multiple pseudo identities, one of which is legitimate. We use the others to signal coercion to the Election Authority. Eos uses two mixing phases with the goal to break the connection between the voter and vote, not to preserve vote privacy (which is given already) but to guarantee coercion resistance by making it (nearly) impossible for a coercer to follow their vote through the bulletin board. Eos is universally verifiable.
Alessandro Bruni, Eva Drewsen, and Carsten Schürmann: A mechanized proof of Selene receipt freeness and privacy, Proceedings on the International Conference on Electronic Voting (E-Vote-ID'17) Bregenz, Austria, October 2017.
Selene is a novel voting protocol that supports individual verifiability, Vote-Privacy and Receipt-Freeness. The scheme provides tracker numbers that allow voters to retrieve their votes from a public bulletin board and a commitment scheme that allows them to hide their vote from a potential coercer. So far, however, Selene was never studied formally. The Selene protocol was neither completely formalized, nor were the correctness proofs for Vote-Privacy and Receipt-Freeness. In this paper, we give a formal model for a simplified version of Selene in the symbolic model, along with a machine-checked proof of Vote-Privacy and Receipt-Freeness. All proofs are checked with the Tamarin theorem prover.
Alessandro Bruni, Rosario Giustolisi, and Carsten Schürmann: Automated Analysis of Accountability, Proceedings of 20th International Information Security Conference (ISC 2017), Ho Chi Minh City, Vietnam, November, 2017.
A recent trend in the construction of security protocols such as voting and certificate management systems is to make principals accountable for their actions. Whenever some principals deviate from the protocol’s prescription and cause the failure of a goal of the system, accountability ensures that the system can detect the misbehaving parties who caused that failure. Accountability is an intuitively stronger property than verifiability as the latter only rests on the possibility of detecting the failure of a goal. A plethora of accountability and verifiability definitions have been proposed in the literature. Those definitions are either very specific to the protocols in question, hence not applicable in other scenarios, or too general and widely applicable but requiring complicated and hard to follow manual proofs. In this paper, we advance formal definitions of verifiability and accountability that are amenable to automated verification. Our definitions are general enough to be applied to different classes of protocols and different automated security verification tools. Furthermore, we point out formally the relation between verifiability and accountability. We validate our definitions with the automatic verification of three protocols: a secure exam protocol, Google’s Certificate Transparency, and an improved version of Bingo Voting. We find through automated verification that all three protocols satisfy verifiability while only the first two protocols meet accountability.
Bruno Xavier, Carlos Olarte, Giselle Reis and Vivek Nigam: Mechanizing Linear Logic in Coq, 12th Workshop on Logical and Semantic Frameworks with Applications (LFSA 2017), Brasília, Brazil, September 2017.
Linear logic has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks and models for concurrency. Linear logic's cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. Cut-elimination guarantees that linear logic is consistent and has the so-called sub-formula property. Focusing is a discipline for proof search that was introduced to reduce the search space, but has proved to have more value, as it allows one to specify the shapes of proofs available. This paper formalizes linear logic in Coq and mechanizes the proof of cut-elimination and the completeness of focusing. Moreover, the implemented logic is used to encode an object logic, such as in a linear logical framework, and prove adequacy.
Dragiša Žunić and Pierre Lescanne: A congruence relation for restructuring classical terms, 18th Italian Conference on Theoretical Computer Science (ICTCS 2017), Naples, Italy, September 2017.
We present a congruence relation on sequent-style classical proofs which identifies proofs up to trivial rule permutation. The study is performed in the framework of *X calculus which provides a Curry- Howard correspondence for classical logic (with explicit structural rules) ensuring that proofs can be seen as terms and proof transformation as computation. Congruence equations provide an explicit account for classifying proofs (terms) which are syntactically different but essentially the same. We are able to prove that there is always a representative of a congruence class which enables computation at the top level.
Dragiša Žunić: Standard classical logic as protocol for process communication, 6th Conference on Logic and Applications (LAP 2017), Dubrovnik, Croatia, September 2017.
We propose a process calculus for classical logic with explicit structural rules. Rather than going though linear logic we use a standard classical logic formalized in the sequent calculus. In this ongoing research, we illustrate that classical logic has potential to naturally serve as protocol for concurrent process communication.

2016

Peter Brottveit Bock, Alessandro Bruni, Agata Murawska, and Carsten Schürmann: Representing Session Types, Dale Miller's Festschrift (Dale-Fest 2016), Paris, France, December 2016.
In this paper we propose a logical foundation of processes and their focused normal forms. We use a linear meta-language based on substructural operational semantics to describe focused forms of processes, and compare them to standard π-calculus processes with their respective operational semantics. The overall goal of this research is to understand how to reason about processes, multi-party communication and global types, and how to mechanize properties such as deadlock freeness and liveness. We are also interested in establishing the limitations of this approach.
Carsten Schürmann: A Risk-Limiting Audit In Denmark: A Pilot, International Joint Conference on Electronic Voting (E-VOTE-ID 2016), Bregenz, Austria, October 2016.
The theory of risk-limiting audits is well-understood, at least mathematically. Such audits serve to create confidence in the reported election outcome by checking the evidence created during the election. When election officials introduce election technologies into the voting process, it is best to do this after the appropriate auditing framework has been implemented. In this paper, we describe our experiences with piloting a risk-limiting audit of a referendum that was held in Denmark on December 3, 2015. At the time of the publication of this paper, Denmark’s election law did not permit electronic voting technologies to be used during voting allowing us to study auditing in isolation. Our findings are that (1) risk-limiting audits also apply to paper and pencil elections; (2) election officials usually support risk-limiting audits even if no voting technologies are used because these audits can improve the efficiency of the manual count; (3) that practical and organizational challenges must be overcome to keep audits repeatable, in particular it must be possible to identify individual ballots repeatedly and reliably; (4) it is possible to arrange an audit for the result of an earlier stage in a count during a later stage, for example, an audit of the rough count results fine count; and (5) that whenever the electronic voting technologies are considered, auditing should be considered as part of feasibility study.
Dragiša Žunić and Pierre Lescanne: Asterix calculus — classical computation in detail, 5th Conference on Logic and Applications (LAP 2016), Dubrovnik, Croatia, September 2016.
We present Asterix calculus, built from names instead of variables. Asterix is designed to stand in computational correspondence with classical logic represented in the sequent calculus. More precisely, in the sequent system G1, featuring explicit structural rules weakening and contraction.
Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler: Coherence Generalises Duality: a logical explanation of multiparty session types, 27th International Conference on Concurrency Theory (CONCUR2016), Québec City, Canada, August 2016.
Wadler introduced Classical Processes (CP), a calculus based on a propositions-as-types correspondence between propositions of classical linear logic and session types. Carbone et al. introduced Multiparty Classical Processes, a calculus that generalises CP to multiparty session types, by replacing the duality of classical linear logic (relating two types) with a more general notion of coherence (relating an arbitrary number of types). This paper introduces variants of CP and MCP, plus a new intermediate calculus of Globally-governed Classical Processes (GCP). We show a tight relation between these three calculi, giving semantics-preserving translations from GCP to CP and from MCP to GCP. The translation from GCP to CP interprets a coherence proof as an arbiter process that mediates communications in a session, while MCP adds annotations that permit processes to communicate directly without centralised control.
Sebastian Mödersheim and Alessandro Bruni: AIF-omega: Set-Based Protocol Abstraction with Countable Families, 5th International Conference on Principles of Security and Trust (POST 2016), Eindhoven, The Netherlands, April 2016.
Abstraction based approaches like ProVerif are very efficient in protocol verification, but have a limitation in dealing with stateful protocols. A number of extensions have been proposed to allow for a limited amount of state information while not destroying the advantages of the abstraction method. However, the extensions proposed so far can only deal with a finite amount of state information. This can in many cases make it impossible to formulate a verification problem for an unbounded number of agents (and one has to rather specify a fixed set of agents). Our work shows how to overcome this limitation by abstracting state into countable families of sets. We can then formalize a problem with unbounded agents, where each agent maintains its own set of keys. Still, our method does not loose the benefits of the abstraction approach, in particular, it translates a verification problem to a set of first-order Horn clauses that can then be efficiently verified with tools like ProVerif.

Meta-CLF 2

Project Description

People

Collaborators

Past members

Outputs

Related Work