Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol

被引:6
作者
Belardinelli, Francesco [1 ,2 ]
Condurache, Rodica [3 ]
Dima, Catalin [3 ]
Jamroga, Wojciech [4 ]
Knapik, Michal [4 ]
机构
[1] Imperial Coll London, London, England
[2] Univ Evry, Nice, France
[3] Univ Paris Est Creteil, LACL, Creteil, France
[4] Polish Acad Sci, Inst Comp Sci, Warsaw, Poland
关键词
Alternating-time Temporal Logic; Bisimulations; Voting protocols; Formal verification; MODEL CHECKING; SYSTEMS; VERIFICATION; UNCERTAINTY; ANONYMITY; LOGIC;
D O I
10.1016/j.ic.2020.104552
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL* for both the objective and subjective variants of the state-based semantics with imperfect information, which are commonly used in the modeling and verification of multi-agent systems. Furthermore, we apply the theoretical result to the verification of coercion-resistance in the ThreeBallot voting system, a voting protocol that does not use cryptography. In particular, we show that natural simplifications of an initial model of the protocol are in fact bisimulations of the original model, and therefore satisfy the same ATL* properties, including coercion-resistance. These simplifications allow the model-checking tool MCMAS to terminate on models with a larger number of voters and candidates, compared with the initial model. (C) 2020 Elsevier Inc. All rights reserved.
引用
收藏
页数:24
相关论文
共 74 条
  • [51] Jamroga W., 2015, Logical Methods for Specification and Verification of Multi-Agent Systems
  • [52] Jamroga W., 2006, EUMAS 06, P14
  • [53] Model Checking the SELENE E-Voting Protocol in Multi-agent Logics
    Jamroga, Wojciech
    Knapik, Michal
    Kurpiewski, Damian
    [J]. ELECTRONIC VOTING, 2018, 11143 : 100 - 116
  • [54] Jamroga W, 2017, AAMAS'17: PROCEEDINGS OF THE 16TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS, P1241
  • [55] Juels Ari, 2005, WPES '05, P61, DOI DOI 10.1145/1102199.1102213
  • [56] Kacprzak M, 2008, FUND INFORM, V85, P313
  • [57] Augmenting ATL with strategy contexts
    Laroussinie, Francois
    Markey, Nicolas
    [J]. INFORMATION AND COMPUTATION, 2015, 245 : 98 - 123
  • [58] Lomuscio A., 2006, 5 INT JOINT C AUT AG, P548
  • [59] Lomuscio A, 2016, AAMAS'16: PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, P662
  • [60] Melissen M., 2013, THESIS