The security of ICT systems poses a number of challenges related not only to the computational complexity of cryptographic models, but also to the complexity of the systems to secure. Indeed, the development and implementation of these latter might involve a wealth of techniques, including software and network engineering, as well as distributed and multi-agent computational models. 

In this broad direction, the approach based on the specification and verification of security properties by means of logic based-languages aims at automating a number of validation tasks by replacing test-based approaches, code analysis, and building large attack databases with formal methods, such as model checking techniques. The literature on the subject is growing rapidly.

Recently, in [Belardinelli et al., 2019] we proposed a novel approach to the verification of electronic voting protocols based on logics for strategies. More specifically, our approach is based on the Alternating-time Temporal Logic ATL, under the assumption of imperfect information to account for the restricted knowledge of agents in cryptographic contexts.
We developed notions of alternating bisimulation with the aim of reducing the state-space of models, in order to obtain smaller model checking instances. 
In particular, we applied this approach to the verification of properties of anonymity and coercion-freeness in the case of an electronic voting protocol without cryptography - the ThreeBallot system, thus showcasing the feasibility of this PhD project.

This PhD project is meant to develop further the research line initiated in [Belardinelli et al., 2019] in order to develop tools and techniques for the verification of security and voting protocols by using formal methods, also in the presence of cryptography.

Advantages. The main advantages of the proposed methodology over related approaches, including process algebras and rewriting techniques, can be summarised as follows:

1. A rich logic-based language to express relevant properties such as anonymity, authentication, coercion freeness, etc.

2. A clear semantic separation between the strategic aspects of security protocols and the epistemic aspects pertaining to the agents' knowledge and observations.

3. The possibility to adapt well-known techniques in the area of formal methods for system's verification, including bisimulations, multi-valued abstractions, Galois connections, thus allowing reductions in the state-space of the model checking instance at hand.

Challenges. While leveraging on (1), (2), and (3) above, the PhD project will also have to tackle the following two challenges:

4. The complexity of modelling cryptographic aspects within commonly-used, logic-based, specification languages.

5. A significant catch-up with existing methods based on process algebras and rewriting techniques, which are nowadays the most popular methodology in the verification of security protocols.

Contribution. The main objectives of this PhD project consist in the application of logics for strategic reasoning to the analysis and verification of security and voting protocols. The main contributions of the project can be summarised as follows:

1. To extend standard logics for strategic reasoning, such as ATL, to account for the cryptographic aspects of security protocols.

2. To develop verification techniques for security properties, also using (bi)simulations and abstractions to reduce the systems' state-space.

3. To develop an ATL-based model checking tool for the verification of security and voting protocols.

4. To apply this tool to check for vulnerabilities pertaining to safety and security in a vast number of voting protocols.


[Belardinelli et al., 2019] F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, M. Knapik: Bisimulations for Verifying Strategic
Abilities with an Application to ThreeBallot. Information & Computation. To appear.