5 papers
Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
Ioana Boureanu, R. Ramanujam
Symbolic protocol verification models the network attacker as a Dolev--Yao (DY) intruder, which does everything its knowledge permits, whether or not it serves any purpose; real ad…
Decidability of Parameterised Dolev-Yao Secrecy
Ioana Boureanu, R. Ramanujam, Srinibas Swain
We study the verification of parameterised secrecy for cryptographic protocols in the Dolev-Yao model, where the number of protocol sessions is unbounded and treated as a parameter…
Program Semantics and a Verification Technique for Knowledge-Based Multi-Agent Systems
Francesco Belardinelli, Ioana Boureanu, Vadim Malvone +1
We give a relational and a weakest precondition semantics for "knowledge-based programs", i.e., programs that restrict observability of variables so as to richly express changes in…
Model Checking Strategic Abilities in Information-sharing Systems
Francesco Belardinelli, Ioana Boureanu, Catalin Dima +1
We introduce a subclass of concurrent game structures (CGS) with imperfect information in which agents are endowed with private data-sharing capabilities. Importantly, our CGSs are…
Model Checking ATL* on vCGS
Francesco Belardinelli, Catalin Dima, Ioana Boureanu +1
We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model…