| 摘 要: 针对车联网的攻击场景具有时空特性,以及现有攻击图在建模和分析方面存在的局限性,提出一种基于概率时空攻击图的车联网安全建模及分析方法。首先,构建了一种新的概率时空攻击图模型,建模具有时空特性的车联网攻击场景;其次,通过转换概率时空攻击图,运用模型检测技术,分析车联网系统对关键安全属性的可满足性。案例分析的结果表明,该方法不仅能有效建模车联网的攻击场景,而且还能确保100%检测出系统对关键安全属性的违反情况,为车联网的攻击场景建模和安全分析提供了一种新方法。 |
| 关键词: 车联网;攻击图;模型转换;概率时间自动机;模型检测 |
|
中图分类号: TP393
文献标识码: A
|
|
| Probabilistic Spatio-Temporal Attack Graph Security Analysis Method for the Internet of Vehicles |
|
CHEN Xinkai, XU Bingfeng
|
(School of Information Science and Technology, Nanjing Forestry University, Nanjing 210037, China)
nlxxchenxinkai@njfu.edu.cn; bingfengxu@njfu.edu.cn
|
| Abstract: In response to the spatio-temporal characteristics of attack scenarios in the Internet of Vehicles (IoV)and the limitations of existing attack graphs in modeling and analysis, this paper proposes a security modeling and analysis method for IoV based on probabilistic spatio-temporal attack graphs. Firstly, a novel probabilistic spatiotemporal attack graph model is constructed to characterize IoV attack scenarios with spatio-temporal features. Secondly,by transforming the probabilistic spatio-temporal attack graph and leveraging model checking technology, the satisfiability of critical security properties in IoV systems is analyzed. Case study results demonstrate that this method not only effectively models IoV attack scenarios but also ensures 100% detection of system violations against critical security properties, providing a novel approach for modeling and security analysis of IoV attack scenarios. |
| Keywords: Internet of Vehicles (IoV); attack graph; model transformation; probabilistic timed automata; model checking |
