Exploit for rollback_car_attack_proverif

## https://sploitus.com/exploit?id=KITPLOIT:TOOLS-GITHUB-THOMASARMEL-ROLLBACK_CAR_ATTACK_PROVERIF
# Rollback 攻击形式化验证

_ProVerif 对汽车遥控钥匙上 Rollback 攻击的概念验证（CVE-2022-37418、CVE-2022-36945 和 CVE-2022-37305），详见[1]_

* * *

## 免责声明

我与 [1] 的作者没有任何关联。感谢他们使其论文开放获取。

## ProVerif 安装

### 官方方式

要运行 ProVerif 形式化验证 PoC，请先按照官方网站上的说明安装 ProVerif。

### 预编译二进制

另外，我预编译了适用于 amd64 架构 Linux 的静态二进制文件，可在仓库的发布页面获取，同时还有适用于 Windows 的可执行文件。

请确保为下载的可执行文件添加执行权限：

root@kitploit:~
    
    
    chmod +x proverif_linux_amd64_static
    

## 用法

### 克隆仓库

root@kitploit:~
    
    
    git clone https://github.com/thomasarmel/rollback_car_attack_proverif.git
    cd rollback_car_attack_proverif/
    

### 在模型上运行验证

root@kitploit:~
    
    
    proverif model.pv
    

您应该会看到，打开车门并不意味着遥控钥匙已被按下，这意味着攻击者成功打开了车门：

![ProVerif 控制台上的攻击查询摘要](https://assets.kitploit.com/production/public/readmes/33502/dbe8798176c0ec354f5aec5f519da084549e644327716eb27b46aad9877be78b.png)

确切地说，这个查询意味着可以触发开启机制的次数大于按下遥控钥匙的次数。

#### 需要按下遥控钥匙

我们可以注意到，虽然查询

root@kitploit:~
    
    
    inj-event(car_open) ==> inj-event(fob_pressed)
    

返回 `false`，但 Proverif 会告诉我们，查询

root@kitploit:~
    
    
    event(car_open) ==> event(fob_pressed)
    

将会返回 `true`：

![inj-event\(car_open\) ==> inj-event\(fob_pressed\) 为 false，但 event\(car_open\) ==> event\(fob_pressed\) 为 true](https://assets.kitploit.com/production/public/readmes/33502/1e3ff931f2720a4a7f6fd829e61d5c198043672a691aea3708710a41fafe8b0b.png)

这意味着必须按下遥控钥匙才能打开车门，但车门可以被打开的次数可以大于遥控钥匙被按下的次数。

### 生成攻击图

#### Graphviz

为了生成轨迹 PDF，ProVerif 需要安装 graphviz 并将其添加到 PATH 环境变量。

在 Linux 上，你可以使用以下命令安装：

root@kitploit:~
    
    
    sudo apt update
    sudo apt install graphviz
    

在 Windows 上，你可以从 https://graphviz.org/download/ 下载安装程序。请确保将安装文件夹添加到 PATH 环境变量：

![在 Windows 上安装 Graphviz 时，将安装文件夹添加到 PATH 环境变量](https://assets.kitploit.com/production/public/readmes/33502/b9455b69034e0677a5985d7b4c5ad91e8399469ce3a68e4ca6d396b1df13fb5a.png)

#### 生成图

要生成详细描述攻击的图，请运行

root@kitploit:~
    
    
    proverif -graph . model.pv
    

现在打开生成的 PDF 文件，查看攻击者如何在不按下遥控钥匙的情况下触发车门打开：

![恶意打开车门时的攻击图](https://assets.kitploit.com/production/public/readmes/33502/42d557d5ba2da6455e7ac644379283bb9a577d5341213f817404f9e7dbe730cd.png)

## 参考文献

[1] _Csikor, Levente and Lim, Hoon Wei and Wong, Jun Wen and Ramesh, Soundarya and Parameswarath, Rohini Poolat and Chan, Mun Choon_ , **Rollback: A new time-agnostic replay attack against the automotive remote keyless entry systems** , ACM Transactions on Cyber-Physical Systems, 2024, https://doi.org/10.1145/3627827