Abstract
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 language | English |
|---|---|
| Publication status | Accepted/In press - 2019 |
| Event | 16th International Conference on Quantitative Evaluation of SysTems - Glasgow, United Kingdom Duration: 10 Sep 2019 → 12 Sep 2019 |
Conference
| Conference | 16th International Conference on Quantitative Evaluation of SysTems |
|---|---|
| Abbreviated title | QEST 2019 |
| Country | United Kingdom |
| City | Glasgow |
| Period | 10/09/19 → 12/09/19 |
Fingerprint
Cite this
}
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 conference › Paper › Research › peer-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 -