School of Software, East China Jiaotong University, Nanchang 330013, China.
Comput Intell Neurosci. 2022 Aug 23;2022:2420590. doi: 10.1155/2022/2420590. eCollection 2022.
The verification of security protocols is an important basis for network security. Now, some security protocols add timestamps to messages to defend against replay attacks by network intruders. Therefore, verifying the security properties of protocols with timestamps is of great significance to ensure network security. However, previous formal analysis method of such protocols often extracted timestamps into random numbers in order to simplify the model before modeling and verification, which probably cause time-dependent security properties that are ignored. To solve this problem, a method for verifying security protocols with timestamps using model checking technique is proposed in this paper. To preserve the time-dependent properties of the protocol, Promela (process meta language) is utilized to define global clock representing the protocol system time, timer representing message transmission time, and the clock function representing the passage of time; in addition, a mechanism for checking timestamps in messages is built using Promela. To mitigate state space explosion in model checking, we propose a vulnerable channel priority method of using Promela to build intruder model. We take the famous WMF protocol as an example by modeling it with Promela and verifying it with model checker SPIN (Simple Promela Interpreter), and we have successfully found two attacks in the protocol. The results of our work can make some security schemes based on WMF protocol used in the Internet of things or other fields get security alerts. The results also show that our method is effective, and it can provide a direction for the analysis of other security protocols with timestamp in many fields.
安全协议的验证是网络安全的重要基础。现在，一些安全协议会向消息中添加时间戳，以防止网络入侵者的重播攻击。因此，验证具有时间戳的协议的安全属性对于确保网络安全具有重要意义。然而，以前针对此类协议的正式分析方法通常会将时间戳提取为随机数，以便在建模和验证之前简化模型，这可能会忽略与时间相关的安全属性。为了解决这个问题，本文提出了一种使用模型检查技术验证带时间戳的安全协议的方法。为了保留协议的时间相关属性，使用 Promela（进程元语言）定义表示协议系统时间的全局时钟、表示消息传输时间的计时器以及表示时间流逝的时钟函数；此外，使用 Promela 构建了检查消息中时间戳的机制。为了缓解模型检查中的状态空间爆炸问题，我们提出了一种使用 Promela 构建入侵模型的脆弱通道优先级方法。我们使用 Promela 对著名的 WMF 协议进行建模，并使用模型检查器 SPIN（Simple Promela Interpreter）对其进行验证，成功地在协议中发现了两个攻击。我们工作的结果可以使基于 WMF 协议的一些安全方案在物联网或其他领域得到安全警报。结果还表明，我们的方法是有效的，它可以为许多领域中带有时间戳的其他安全协议的分析提供方向。
