STV: Socio-Technical Verification of Information Security and Trust in Voting Systems

The STV project is a collaboration between researchers from Institute of Computer Science, Polish Academy of Sciences, The Luxembourg University, and Polish-Japanese Academy of Information Technology. It is funded by NCBiR (Narodowe Centrum Badań i Rozwoju, Poland) and FNR (Fonds National de la Recherche, Luxembourg).

The project aims to develop new concepts and tools for specification, analysis, and assessment of information security properties. The focus is on voting procedures and protocols, and in particular on their essential features like confidentiality, coercion-resistance, and voter-verifiability. The developed concepts and tools will be applied to other domains where information security is important. The same holds for the new protocols, designed to support security requirements in the social context.

Learn More

Funded by

The Team

Prof. Peter Y. A. Ryan, co-PI

The leader of the Luxembourgish part of the project. Key areas: information security, in particular coercion-resistant and voter-verifiable voting protocols.
Personal website

Prof. Wojciech Jamroga, co-PI

The leader of the Polish part of the project. Key areas: logical methods for specification and verification of multi-agent systems, as well as game-theoretic models of MAS.
Personal website

Prof. Wojciech Penczek

Key areas: models of distributed systems, multi-agent systems, modelling of knowledge and belief, temporal logics, automated verification, planning, and model checking of concurrent systems.
Personal website

Michał Knapik, PhD, research associate (postdoc)

Key areas: model checking for temporal and strategic logics; formal methods for multi-agent systems.
Personal website

Gabriele Lenzini, PhD

Key areas: modelling, analysis and design of secure and trustworthy systems, analysis of security in socio-technical systems.
Personal website

Damian Kurpiewski, MSc, PhD student

Key areas: modelling and analysis of complex systems, algorithms for model-checking, tool development.
Personal website

Teofil Sidoruk, MSc, PhD student

Key areas: state space reduction methods, model checking of multi-agent systems.

Yan Kim, MSc, PhD student

Key areas: modelling and analysis of voting protocols.

Prof. Marek Bednarczyk

Key areas: algorithms for parallel computation and automated search.

Tadeusz Puźniakowski, PhD

Key areas: algorithms for parallel computation and automated search.
Personal website

Łukasz Mikulski, PhD

Key areas: reduction methods, model-checking algorithms, optimization methods.

Witold Pazderski, MSc, PhD student

Key areas: tool development.

Peter Roenne, PhD

Key areas: cryptography and design of e-voting protocols.

David Mestel, PhD

Key areas: information security, quantified information flow.

Associated Researchers

Łukasz Maśko, PhD

Masoud Tabatabaei, PhD

Publications and Software

Publications

Software

StraTegic Verifier (STV)
STV is a prototype tool aimed at verification of strategic abilities in multi-agent systems, and synthesis of strategies that guarantee a given temporal goal.

MsATL
MsATL is a prototype tool for deciding the satisfiability of Alternating-time Temporal Logic (ATL) with imperfect information. MsATL combines SAT Modulo Monotonic Theories solvers with existing ATL model checkers: MCMAS and STV. The tool can deal with various semantics of ATL, including perfect and imperfect information, and can handle additional practical requirements. MsATL can be applied for synthesis of games that conform to a given specification, with the synthesised game often being minimal.