|The security and trustworthiness of AI systems poses a number of challenges related to the complexity of the systems at hand. Indeed, the design and development of security features calls for a careful modelling of the reasoning and computational capabilities of the agents partaking in the system.|
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 has
been growing steadily.
Recently, in [Belardinelli et al., 2019] we proposed a novel approach to the verification of voting protocols based on logics for strategies. More specifically, our approach is based on Alternating-time Temporal Logic (ATL), under the assumption of imperfect information to model the restricted knowledge of agents typical in multi-agent systems (MAS). We applied this approach to the verification of properties of anonymity and coercion-freeness in the Three Ballot system, an electronic voting protocol without cryptography, thus showcasing the feasibility of this project.
This PhD project is meant to pursue further the research line initiated in [Belardinelli et al., 2019] in order to develop tools and techniques for the verification of security properties in multi-agent systems (MAS), including voting protocols, thus providing a formal certification of their trustworthiness.
The main advantages of the proposed methodology over related approaches, including process algebras and rewriting techniques, can be summarised as follows:
a. A rich AI-inspired language to express agent-centric properties such as anonymity, authentication, coercion-freeness.
b. A clear separation between the strategic aspects of security protocols, modelled as actions and transitions, and the epistemic aspects pertaining to the agents’ knowledge, modelled by observations.
c. The possibility to adapt well-known techniques in MAS verification, including bisimulations, multi-valued abstractions, Galois connections, thus allowing reductions in the state-space of the model checking instance at hand.
While leveraging on (a), (b), and (c) above, the PhD project will also have to tackle the following two challenges:
d. The complexity of modelling cryptographic aspects within commonly-used, logic-based, specification languages.
e. 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. This PhD project focus on the application of logics for strategic reasoning to the analysis and verification of security and trustworthiness in voting protocols. The main contributions of the project can be summarised as follows:
1. To extend the standard logics for strategic reasoning, including ATL, to account for the cryptographic aspects of security protocols.
2. To develop verification techniques for security properties, also leveraging on (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.
The research described in this PhD project is relevant for the key CDT areas of verification, conformance to norms, logic-based AI, and security and trustworthiness. [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, 2019.