Abstract
| Language | Undefined |
|---|---|
| Title of host publication | Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015) |
| Editors | Sriram Sankaranarayanan, Enrico Vicario |
| Place of Publication | Zurich |
| Publisher | Springer International Publishing |
| Pages | 156-171 |
| Number of pages | 16 |
| ISBN (Print) | 978-3-319-22974-4 |
| DOIs | |
| State | Published - Sep 2015 |
| Event | 13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015 - Universidad Complutense de Madrid, Madrid, Spain Duration: 2 Sep 2015 → 4 Sep 2015 Conference number: 13 http://formats2015.unifi.it/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer International Publishing |
| Volume | 9268 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015 |
|---|---|
| Abbreviated title | FORMATS |
| Country | Spain |
| City | Madrid |
| Period | 2/09/15 → 4/09/15 |
| Internet address |
Keywords
- EC Grant Agreement nr.: FP7/318003
- EWI-25869
- FMT-MC: MODEL CHECKING
- EC Grant Agreement nr.: FP7/2007-2013
- Model Checking
- IR-97025
- Socio-technical security
- Case Studies
- Attack Tree
- Attacker Profile
- METIS-312524
- Uppaal Cora
Cite this
}
Quantitative Attack Tree Analysis via Priced Timed Automata. / Kumar, Rajesh; Ruijters, Enno Jozef Johannes; Stoelinga, Mariëlle Ida Antoinette.
Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015). ed. / Sriram Sankaranarayanan; Enrico Vicario. Zurich : Springer International Publishing, 2015. p. 156-171 (Lecture Notes in Computer Science; Vol. 9268).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
TY - GEN
T1 - Quantitative Attack Tree Analysis via Priced Timed Automata
AU - Kumar,Rajesh
AU - Ruijters,Enno Jozef Johannes
AU - Stoelinga,Mariëlle Ida Antoinette
N1 - Foreground = 80%; Type of activity = Conference; Main leader = UT; Type of audience = scientific community, industry; Size of audience = 50; Countries addressed = International;
PY - 2015/9
Y1 - 2015/9
N2 - The success of a security attack crucially depends on the resources available to an attacker: time, budget, skill level, and risk appetite. Insight in these dependencies and the most vulnerable system parts is key to providing effective counter measures. This paper considers attack trees, one of the most prominent security formalisms for threat analysis. We provide an effective way to compute the resources needed for a successful attack, as well as the associated attack paths. These paths provide the optimal ways, from the perspective of the attacker, to attack the system, and provide a ranking of the most vulnerable system parts. By exploiting the priced timed automaton model checker Uppaal CORA, we realize important advantages over earlier attack tree analysis methods: we can handle more complex gates, temporal dependencies between attack steps, shared subtrees, and realistic, multi-parametric cost structures. Furthermore, due to its compositionality, our approach is flexible and easy to extend. We illustrate our approach with several standard case studies from the literature, showing that our method agrees with existing analyses of these cases, and can incorporate additional data, leading to more informative results.
AB - The success of a security attack crucially depends on the resources available to an attacker: time, budget, skill level, and risk appetite. Insight in these dependencies and the most vulnerable system parts is key to providing effective counter measures. This paper considers attack trees, one of the most prominent security formalisms for threat analysis. We provide an effective way to compute the resources needed for a successful attack, as well as the associated attack paths. These paths provide the optimal ways, from the perspective of the attacker, to attack the system, and provide a ranking of the most vulnerable system parts. By exploiting the priced timed automaton model checker Uppaal CORA, we realize important advantages over earlier attack tree analysis methods: we can handle more complex gates, temporal dependencies between attack steps, shared subtrees, and realistic, multi-parametric cost structures. Furthermore, due to its compositionality, our approach is flexible and easy to extend. We illustrate our approach with several standard case studies from the literature, showing that our method agrees with existing analyses of these cases, and can incorporate additional data, leading to more informative results.
KW - EC Grant Agreement nr.: FP7/318003
KW - EWI-25869
KW - FMT-MC: MODEL CHECKING
KW - EC Grant Agreement nr.: FP7/2007-2013
KW - Model Checking
KW - IR-97025
KW - Socio-technical security
KW - Case Studies
KW - Attack Tree
KW - Attacker Profile
KW - METIS-312524
KW - Uppaal Cora
U2 - 10.1007/978-3-319-22975-1_11
DO - 10.1007/978-3-319-22975-1_11
M3 - Conference contribution
SN - 978-3-319-22974-4
T3 - Lecture Notes in Computer Science
SP - 156
EP - 171
BT - Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015)
PB - Springer International Publishing
CY - Zurich
ER -