Automated Game-Theoretic Verification of Security Systems

Chunyan Mu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

260 Downloads (Pure)


Security-sensitive computerised communication systems are of increasing importance, however checking that they function correctly can be non-trivial. We propose automated verification techniques for the formal analysis of quantitative properties of such systems. Since communication networks typically require the collaboration of their participants to work effectively, we adopt a game-theoretic approach. Utility functions for each player, such as the degree of security offered
and the communication costs incurred, are formally specified using quantitative temporal logics. Then, building upon probabilistic verification techniques for parametric Markov chains, we develop methods to identify Nash equilibria representing stable strategies for the participants. We implement our methods as an extension of the PRISM model checker, and illustrate their applicability by studying anonymity-cost trade-offs in the Crowds anonymity protocol.
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems. QEST 2019
EditorsD Parker, V Wolf
ISBN (Electronic)9783030302818
ISBN (Print)9783030302801
Publication statusPublished - 4 Sept 2019
Event16th International Conference on Quantitative Evaluation of SysTems - Glasgow, United Kingdom
Duration: 10 Sept 201912 Sept 2019

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference16th International Conference on Quantitative Evaluation of SysTems
Abbreviated titleQEST 2019
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Automated Game-Theoretic Verification of Security Systems'. Together they form a unique fingerprint.

Cite this