Automated Game-Theoretic Verification of Security Systems

Research output: Contribution to conferencePaperResearchpeer-review

50 Downloads (Pure)

Abstract

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
Publication statusAccepted/In press - 2019
Event16th International Conference on Quantitative Evaluation of SysTems - Glasgow, United Kingdom
Duration: 10 Sep 201912 Sep 2019

Conference

Conference16th International Conference on Quantitative Evaluation of SysTems
Abbreviated titleQEST 2019
CountryUnited Kingdom
CityGlasgow
Period10/09/1912/09/19

Fingerprint

Security systems
Temporal logic
Markov processes
Telecommunication networks
Costs
Communication systems
Network protocols
Communication

Cite this

Mu, C. (Accepted/In press). Automated Game-Theoretic Verification of Security Systems. Paper presented at 16th International Conference on Quantitative Evaluation of SysTems , Glasgow, United Kingdom.
Mu, Chunyan. / Automated Game-Theoretic Verification of Security Systems. Paper presented at 16th International Conference on Quantitative Evaluation of SysTems , Glasgow, United Kingdom.
@conference{0c49e7ca5bcb4f09ab7048e6c71f5422,
title = "Automated Game-Theoretic Verification of Security Systems",
abstract = "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 offeredand 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.",
author = "Chunyan Mu",
year = "2019",
language = "English",
note = "16th International Conference on Quantitative Evaluation of SysTems , QEST 2019 ; Conference date: 10-09-2019 Through 12-09-2019",

}

Mu, C 2019, 'Automated Game-Theoretic Verification of Security Systems' Paper presented at 16th International Conference on Quantitative Evaluation of SysTems , Glasgow, United Kingdom, 10/09/19 - 12/09/19, .

Automated Game-Theoretic Verification of Security Systems. / Mu, Chunyan.

2019. Paper presented at 16th International Conference on Quantitative Evaluation of SysTems , Glasgow, United Kingdom.

Research output: Contribution to conferencePaperResearchpeer-review

TY - CONF

T1 - Automated Game-Theoretic Verification of Security Systems

AU - Mu, Chunyan

PY - 2019

Y1 - 2019

N2 - 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 offeredand 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.

AB - 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 offeredand 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.

M3 - Paper

ER -

Mu C. Automated Game-Theoretic Verification of Security Systems. 2019. Paper presented at 16th International Conference on Quantitative Evaluation of SysTems , Glasgow, United Kingdom.