面向物联网中克隆节点攻击检测方案的形式化建模、分析与验证
密码学与安全
2021-08-24 v1
摘要
在克隆节点攻击中，攻击者试图物理捕获设备以收集敏感信息，从而实施各种内部攻击。从上述观点出发，已有多种用于检测物联网网络中克隆节点攻击的解决方案被提出。这些解决方案专注于特定的系统设计、过程和特征集，并基于少数性能要求作为底层系统架构的高层抽象。然而，现有提出的解决方案中常常忽略了关键特性，如形式化分析、建模和验证，而这些特性旨在验证系统的正确性和鲁棒性，以确保不存在有问题的场景或异常。本文对我们先前提出的物联网克隆节点攻击检测方案进行了形式化分析、建模和验证。首先，我们使用高级Petri网（HLPNs）对该方案的架构组件进行建模，然后根据其指定功能进行映射。其次，我们使用Z规约语言定义并分析了该方案的行为属性。此外，我们使用可满足性模理论库（SMT-Lib）和Z3求解器来验证和演示该方案的整体功能。最后，除了建模和分析之外，本工作还采用了着色Petri网（CPNs），它将Petri网与高级编程语言相结合，使其更适合大规模系统建模。为了在CPN中执行模拟，我们使用了定时和非定时模型，其中定时模型用于评估性能，非定时模型用于验证逻辑有效性。
引用
@article{arxiv.2108.09931,
title = {Towards a Formal Modelling, Analysis, and Verification of a Clone Node Attack Detection Scheme in the Internet of Things},
author = {Khizar Hameed and Saurabh Garg and Muhammad Bilal Amin and Byeong Kang},
journal= {arXiv preprint arXiv:2108.09931},
year = {2021}
}