借助新兴的互联车辆（CV）技术，车对车（V2V）和车对基础设施（V2I）的无线通信使车辆能够与其他实体实时交换重要的安全和移动信息。2016年9月，美国运输部（USDOT）在纽约，怀俄明州和坦帕市的三个地点启动了CV试点计划，以刺激早期CV技术的部署并在现实世界中测试CV安全应用。截至2018年秋季，该计划已进入第三阶段，该阶段至少需要18个月的时间才能进行长期运行和关键绩效评估。
虽然CV技术可以极大地有益于运输的机动性和安全性，但是这种大大提高的连通性不可避免地会增加车辆和运输基础设施的攻击面。例如，如果CV通信协议栈不够安全，则攻击者会直接对道路上的驾驶员造成安全隐患。因此，必须尽早了解CV网络堆栈中的潜在安全漏洞，以便可以在大规模攻击之前主动解决这些漏洞。为此，必须从研究CV网络堆栈中潜在的设计安全漏洞入手，因为此类漏洞的发现和防御解决方案通常都可以影响其相应实现实例的安全性。现有的用于分析车辆专用网络（VANET，Vehicular Ad-Hoc Network）或CV安全性的工作通常受到以下三个限制：
（L1）：缺乏系统的方法，只能依靠人工检查来识别潜在的威胁，这些威胁既不充分也不高效。在这些工作中，很难使已识别威胁的风险评估自动化。例如ETSI的威胁分析方法，该方法要依靠人工对威胁的风险进行定性排名。同样，手动地描述了自动车辆（例如，具有V2X通信功能的协作式自动车辆）中的威胁，也仅能说明定性风险。
（L2）：对高层协议（即IEEE 1609协议和CV应用程序）可用性的威胁，可以阻止合法协议参与者访问网络中的关键服务。尽管USDOT和协议设计者已经采用了安全机制来保护CV网络通信的完整性和机密性，但协议栈仍可能会遇到可用性问题。例如下图所示，如果可能导致安全威胁的传入数据包无法通过验证，则会在不触发任何警告的情况下将其丢弃，并且应用程序将无法处理任何传入数据包。
（L3）：先前的工作主要针对前几代协议，或者是在IEEE 1609协议系列的标准化之前进行的，因此在最新的CV网络堆栈设计中不存在一些已发现的漏洞。
本文在（1）IEEE 1609协议家族的最新版本和（2）协同自适应巡航控制（CACC，Cooperative Adaptive Cruise Control）应用程序中执行了严格的安全分析，以自动发现可用性或DoS（拒绝服务）漏洞。为了解决L1（即手动分析）的问题，将分析公式化为模型检查问题，并设计一个新颖的攻击CVAnalyzer，该工具利用（1）通用模型检查器（MC，general model checker）和（2）概率模型检查器（PMC，probabilistic model checker）自动进行攻击显示和攻击评估，任何一个现有模型检查器都无法实现本研究的分析目标。MC可用于攻击发现[；同时，由于易处理性原因，PMC（例如PRISM）在发现漏洞方面的支持有限，并且主要侧重于定量属性验证。因此，利用MC和PMC分别验证与可用性相关的属性和定量属性。
为了解决L2（即没有可用性威胁分析）的问题，定义了安全属性以涵盖与可用性相关的属性（例如，“所有CV设备最终应学习未知证书”）和定量属性（例如，“处理下一个数据包的预期时间延迟是多少？”）。通过验证这些属性不仅可以识别潜在的漏洞，还可以了解相应的安全后果。
为了解决L3，检查了CV网络协议的最新规范和一个复杂的CV应用程序（即CACC）。对于前者，专注于新添加的CV特定功能（例如P2PCD，Peer-to-Peer Certificate Distribution）；对于后者，选择了两个编队管理协议PMP（VENTOS和PLEXE），它们被研究人员，实践者和开发人员广泛使用。
选择研究PMP是因为（1）重要性很高，因为它可以直接控制车辆并因此影响安全性，并且（2）对系统验证的要求很高，因为它涉及多个车辆之间的分布式协作，手动操作很难有效地进行分析。将CV协议抽象为多个有限状态机（FSM，fifinite state machine）。在抽象模型中，每个FSM代表协议参与者，并且所有参与者都通过敌手控制的公共信道相互通信。这种抽象模型忽略了底层实现细节，很适合发现设计缺陷。
通过设计，CVAnalyzer不会触发任何误报，目的是确保稳健性。也就是说，如果进行告警那么一定正确，但是无法检测到所有违规行为。分析由协议参与者的数量来参数化，给定特定数量的协议参与者和一组属性，模型检查可确保详尽枚举所有可到达的状态。因此，模型检查器还应该具有完整性，即，如果模型检查器没有报告任何属性违规，则证明该模型是正确的。但是由于无法确定参数化的系统验证问题，无法实现稳健性和完整性，并且无法枚举所有可能的协议参与者。在这种情况下本文遵循了针对健全性而不是完整性的传统方法。
在模型检查中，模型大小（即可达状态的总数）随状态变量的数量和协议参与者的数量呈指数增长。为了缓解将模型检查应用于复杂网络协议时的状态爆炸问题，提出了一种抽象方法，该方法减少了不必要的状态变量并将大数据域合并为较小的等效数据域。
CV通信能力：在本研究中，假设攻击者可以在自己的车辆或其他车辆上破坏车载设备单元（OBU，On-Board Unit）。这种假设是合理的，因为先前的工作已经表明车载系统可能会受到物理或远程损害。在这种情况下，攻击者可以通过受感染的CV设备将恶意数据包发送到其他车辆。所有恶意数据包都应遵守协议规范，值得注意的是，攻击者被允许将恶意数据包单播到特定车辆（请参阅IEEE 1609.3，5.5.1子条款）。
被动监控：攻击者可以在无线适配器的混杂模式下被动窃听并捕获其无线通信范围内的所有网络流量。
密码学操作：假设CV协议中使用的加密操作（例如签名，验证和哈希）是安全的。因此，攻击者无法伪造用于数据包身份验证的数字签名，但可以使用安装在受损车辆中的有效证书对输出数据包进行签名。攻击者仍然可以（1）通过嗅探CV网络流量来被动地收集有效证书，并且（2）构造未由受信任的锚节点签名的本地证书。
在本节中首先介绍如何构造模型中的每个组件，包括敌手模型和每个协议状态机。然后描述如何减少状态空间，并记录如何实现CVAnalyzer。
A. 模型构建
如上图所示，模型由环境和协议状态机（P）组成，由网络和计时器事件驱动。通常，环境管理协议状态机生成的数据包/时间事件。它向协议状态机传递触发的事件（例如，分组接收，超时）。为攻击者控制的通信环境为循环定义了三个顺序步骤：
1.Retrieve：如果此类事件可用，则环境会选择许多不同的数据包/时间事件之一。
2.Process：协议状态机处理事件。
3.PostProcess：处理给定事件后，协议状态机要么发送新数据包，添加新计时器并取消现有计时器。环境需要更新其内部状态，并跟踪新添加的事件。
威胁模型假定攻击者具有通信和窃听能力，因此为攻击者增加了一个发送和接收任意数据包的步骤：
4.Attack：攻击者能够监视环境中的所有数据包。如果需要，她可以向环境中注入任意数据包，从而允许协议状态机处理所有可能的数据包事件。为网络建模构造了通信通道:
其中chi,j是从Pi到Pj的FIFO队列。在这种情况下，数据包的发送和接收被抽象为chi,j的入队和出队操作。注意不考虑网络因素来发现漏洞，例如网络延迟和数据包丢失，因为有损和错误的网络会削弱攻击的能力并增加模型的复杂性。将攻击者置于她的最佳位置可以帮助发现所有潜在的攻击。另一方面，要对计时器建模，不跟踪绝对时间而只关心事件的时间顺序，这是对分布式系统进行模型检查的常见做法。为了推进进度，如果没有活动事件传递到协议状态机，则所有计时器将同时倒计时。
协议状态机：所有协议参与者（Pi，i∈[1，n]）都是相同的；因此，它们每个都可以表示为同一有限状态机（FSM）。然后模型M可以定义为并发系统，其中包括一个敌手控制环境C和n个等价过程Pi：
在分析中抽象了CV网络堆栈中的高层协议：（1）在网络服务和消息子层中定义的通信模型，（2）安全服务，以及（3）PMP。遵循它们的规范或代码库来定义数据包和计时器处理程序，这些处理程序在处理环境传递的数据包和超时的同时更新Pi的内部状态。模型除了安全服务中证书吊销的处理程序，因为它依赖于像SCMS这样的外部公钥基础结构（PKI）吊销证书，这超出了网络堆栈本身的范围。
对于安全服务，首先将密码图形结构抽象化，假设CV协议中的密码操作是安全的。然后对数据包类型和数据包头数据进行建模，这是内部安全机制所需的。在CV网络中，每个协议参与者都将具有一批唯一的终端实体证书（也称为签名证书）。为了触发所有内部安全机制，对于证书配置，假设每一批签名证书的颁发者都互不相同，并且在传输过程中附加有数据包。
概率：网络协议涉及许多并发事件（例如，分组传输），导致状态机中的并发转换。在建立概率模型时，开发了离散时间马尔可夫链（DTMC）模型，该模型将统一概率分配给源自相同状态的并发状态转换。
状态减少：如下图，现在通过一个具体的例子展示如何抽象化模型以减少状态。为了便于说明使用源自N4的简化示例，目标是减少不必要的状态以获得抽象模型。另外要确保在抽象模型中找到的反例在原始模型中是有效的。
在示例中开发了一种简化的协议，其中该模型根据事件（第9-13行）更新计时器，其中函数h(x)抽象化P2PCD中的哈希截断操作。假设没有攻击者，事件范围是[0,X-1]，其中X<M≤N。环境中的攻击者可以触发所有可能的事件[0,N-1]。对于给定事件，如果h(event)等于i，则将初始化timer[i]（第10行）。对于其他不匹配的计时器，如果未初始化timer[i]（None），则计时器将（1）保持不变；如果已初始化，则（2）倒计时，或者（3）到期时设置为未初始化。为了捕获攻击者的行为，对于上图中的每个下一步，在EventRange中随机选择一个值作为下一个事件（第8行）。值得注意的是，[X,N-1]中的事件由攻击者触发，并且可以导致所有计时器的初始化。最后，要查找反例，指定一个活动属性（第14-16行），如果所有计时器都已初始化，则该计时器最终应终止。
显然，模型的状态空间取决于N和M，它们可以任意大。例如，P2PCD中的定时器索引范围将是[0,2^24-1]（即M＝ 2^24）。事件的数量N可以是2^256。不幸的是，模型检查器无法处理如此大的状态空间。
通过分析模型，不需要跟踪所有timer[i]，因为当没有攻击者出现时，该协议仅更新一小组计时器。如前所述，在没有攻击者的情况下，事件的范围是[0,X-1];因此，该模型仅更新timer[i]，其中i∈[0,X-1]。通常，协议实例并不关心其他计时器是否最终会过期。因此，除了将TimerIndexRange减小为[0,X-1]，还派生了一个弱化性质：
另一方面，观察到许多事件在计时器上触发相同的更新。例如，event=0和event=M都导致timer[0]的初始化。因此，决定保留一小部分EventRange。首先将EventRange划分为几个等效类：
其中EventRangei中的每个事件都会在timer[i]上触发相同的更新。然后，对于每个等效类EventRangei，选择一个值EventRangei = {i}，以便可以在计时器上触发所有更新。在这种情况下将EventRange减小为[0,M-1]。但是，在此范围内，攻击者仅触发[X,M-1]中的事件，这意味着攻击者无法在计时器上触发所有更新。因此将[X,M-1]设置为[X,2M-1]，以便攻击者本身可以触发所有计时器的初始化。最后导出一个映射函数：
对于[0,2M-1]中的每个x’，总能在[0，N-1]中找到至少一个x，使得x‘ = f(x)。换句话说，对于抽象模型中每个已识别的示例，总是可以通过在event上应用反函数f^(-1)来在原始模型中找到至少一个对应的反示例。
通过将上述两种策略结合在一起，可以成功减少示例的状态空间，并确保没有错误的属性冲突。特别是将TimerIndexRange和EventRange分别减小为[0，X X1]和[0,2X-1]。
B. 模型检查
使用通用模型检查器的目的是发现漏洞。给定模型M和安全属性，一旦模型违反属性，通用MC将生成一个反例，导致违反的执行跟踪。形式上，模型可以定义为由状态S的有限集合，初始状态I⊆S，过渡关系T⊆S×S以及从状态到原子集的有限集合L的标记函数L：S→2^(AP)。上表总结了分析P2PCD和PMP的高级属性。对于每个属性，首先对ϕi进行细化以获得新属性ϕi‘，使得ϕi⇒ϕi’和¬ϕi‘⇒¬ϕi。例如，对ϕ1的改进将是至少一个CV设备在观察到未知证书后最终应广播学习请求。使用MC查找违规属性。通过分析反例，可以制定攻击程序并分析确定攻击的根本原因，这对缓解设计很有帮助。最后修补模型，以确保常规MC以后不会生成相同类型的违规。
PMC的目的是避免进行手动风险评估，并且不会丢弃一般MC中已发现的漏洞。它有助于评估暴露的漏洞的严重性，从而使协议设计者可以优先考虑解决方案的设计。与一般的MC不同，PMC为每个状态转换T分配概率：S×S→[0,1]，使得∀s∈S：Σs’∈S|T(s，s‘)=1。因为分配了统一的概率到并发状态转移，对于Succs = {s’∈S | T(s，s‘)> 0}中s的所有可达后继状态，s与任何s0之间的转移概率为1/(| Succs |) 。转移矩阵可以从转移概率中得出。因此，PMC可以计算从初始状态转换为任何目标状态的可能性。如果可以正式确定成功攻击的状态，那么PMC可以帮助提高攻击成功率。除可能性外，PMC还可以为状态转换分配“time”成本，该成本可用于量化与时间相关的属性。利用PMC来量化不确定性攻击N1-4的严重性，N1-4被定义为每次尝试不一定都能成功的攻击。观察到只有将恶意数据包恰好在攻击时间窗口内传递到受害车辆，P2PCD攻击才能成功。但是，攻击者无法精确推断时间窗口的开始和结束，而只能粗略地预测开始时间。因此使用PMC根据成功率和时间延迟来量化其严重性。
C. 实施
按照所提出的方法要实例化CVAnalyzer，使用TLC作为通用模型检查器，因为它可以快速构建模型，选择PRISM 作为的概率模型检查器。作为模型检查的第一步，手动提取IEEE 1609协议家族和PMP的抽象模型。抽象模型包括两辆（即n = 2）合法车辆和一辆恶意车辆（即攻击者）。然后，需要使用TLC和PRISM所使用的建模语言来实现具体模型。由于PLEXE支持的操作是VENTOS的子集，因此将它们合并为一个模型。
在本节中详细描述P2PCD中的4种DoS攻击，VENTOS和PLEXE中的15种攻击（下表）。然后分析确定的攻击的安全隐患，并对那些不确定性攻击的数据包处理的成功率和平均时间延迟进行量化。
A. P2PCD漏洞
总而言之，CVAnalyzer发现了4种新的DoS攻击，它们可能损害CV网络的可用性。所有4个漏洞都来自P2PCD ，如下图。受害车辆在不知道必要的证书的情况下无法验证传入的数据包。因此，CV网络堆栈无法将数据传递到应用程序层。此外讨论了造成这些漏洞的根本原因并评估了它们的安全后果。
在以下描述中，两个CV设备，Vehicle 1（V1）和Vehicle 2（V2）每100毫秒广播一次SPDU。但是，V2无法验证V1发送的数据包，因为V2不知道V1使用的签名证书ee1的颁发者ca1。因此，V2想学习未知证书ca1。对于下面介绍的每种攻击，V1首先向V2发送触发SPDU。在没有攻击者的正常情况下，V2在接收到触发SPDU之后，初始化P2PCD学习过程并将学习请求信息附加到下一个传出SPDU中。V1将在收到学习请求后构造并发送学习响应。
1）响应静默攻击（Response Mute Attack）
N1可以阻止对等CV设备发送学习响应。该攻击利用了对学习响应的可选验证以及P2PCD的限制机制，该机制将响应数量限制为单个请求。攻击者通过发送多个恶意学习响应来有意与V1进行交互，以确保V1的响应计数器超过响应阈值。结果，V1选择不发送学习响应，并且V2无法学习未知证书ca1。
假设：为了成功进行此攻击，攻击者需要知道响应阈值的准确值。例如，BSM的响应阈值为3。假设V1不要求对传入的学习响应进行验证，这与当前的协议规范一致。此外，假设攻击者具有足够的计算能力来有效构建可能导致部分哈希碰撞（例如，低阶3字节碰撞low-order 3 bytes collision）的学习响应。
攻击步骤：上图详细说明了攻击步骤。V1首先向V2发送触发SPDU。V2不是立即发送学习请求，而是将未知证书ca1的HashedId8值存储在队列中（参见IEEE 1609.2，D.4.2.1.1）。V2在其下一个传出SPDU的学习请求字段中附加ca1的HashedId3值。在P2PCD中，HashedId8和HashedId3分别表示证书的低阶8字节和3字节哈希。收到学习请求后，V1开始准备学习响应。基于限制机制，V1初始化请求的证书的响应退避计时器和响应计数器。
但是，攻击者可以观察到触发SPDU和学习请求，因此可以确定V2要从V1学习未知证书。攻击者因此自由地构造了多个学习响应，其中有效载荷中第一个证书的HashedId3值与未知证书ca1相匹配。攻击者随后将这些恶意数据包发送出去，以使V1的响应计数器饱和（即，使其不低于响应阈值）。在接收到恶意学习响应后，V1错误地更新了其响应计数器（通过IEEE 1609.2中定义的AddCertificate原语）。当响应退避计时器到期时，V1检查响应计数器是否小于或等于响应阈值。显然，基于响应计数器的当前状态，V1决定此时放弃响应。
2）请求静默攻击（Request Mute Attack）
N2和N3都可以阻止CV设备发送学习请求。与N1相似，N2利用哈希碰撞问题。N3利用单播功能，并向恶意SPDU注入与V2打算发送的学习请求字段相同的学习请求字段（即cashed的HashedId3值）。结果V2可以观察到恶意学习请求，并决定不发送自己的学习请求。由于V1未收到任何学习请求，因此V2无法学习未知证书ca1。
假设：为了成功发起此攻击，唯一的要求是攻击者需要知道受害者车辆V2的MAC地址。这是合理的，因为攻击者可以监视网络中的所有流量。因此，它可以从V2发送的数据包中观察V2的MAC地址。
攻击步骤：如下图所示，V2在从V1接收到触发SPDU后初始化P2PCD。V2将未知证书ca1的HashedId8值存储在队列中。同时，由于攻击者可以观察到触发SPDU，因此她构造了一个恶意学习请求，其中学习请求字段m.lr等于未知证书ca1的HashedId3值。在P2PCD中，收到学习请求后，V2删除队列中任何匹配的HashedId8条目。因此，V2删除队列中未知证书h8（ca1）的条目，其中h8是获取输入的低阶八字节哈希的函数。随着队列变空，V2决定不在下一个传出SPDU中附加学习请求信息。因此，V2无法学习正确的未知证书。
3）麻木攻击（Numb Attack）
首先，与N3一样，此攻击利用单播功能，并向恶意SPDU注入与V2打算发送的学习请求字段相同的学习请求字段（即，HashedId3值约为ca1）。这导致了与N3相同的结果，其中V2选择不发送学习请求，因此无法学习未知证书。然后，由于请求活动计时器（例如reqActiveTimer），V2仍然认为动态中应该有Bean活动请求。因此，在接收下一个触发SPDU时，V2选择不将未知证书ca1的HashedId8值添加到队列中，并继续等待学习响应。
攻击步骤：如上图所示，此攻击类似于N3，但攻击者具有不同的攻击目标，即试图阻止受害车辆V2记录未知证书。由于V1每100毫秒广播一次BSM，因此V2将在几毫秒内再次接收到触发SPDU。此时，V2仍无法验证传入的数据包。但是，由于请求活动计时器已在上一轮通信中初始化，并且该计时器通常设置为250 ms，因此V2认为仍存在活动中的学习请求。因此，V2不会在队列中添加任何内容，这意味着它不会在下一个传出SPDU中附加任何学习请求信息。在请求活动计时器到期之前，V2无法从此恶意状态中恢复。
4）评估
只有攻击者将恶意数据包恰好在攻击时间窗口内发送给受害车辆，N1-4才能成功。但是，攻击者的一个挑战是她不能精确确定攻击时间窗口的开始或结束，而只能大致估计时间窗口。因此通过使用CVAnalyzer中的概率模型检查器来量化成功发起攻击的概率。
上表总结了量化结果。由于N3和N4使用相同类型的数据包攻击受害车辆，并且它们的攻击时间窗口相同，因此将这两种攻击合并在一起，并根据攻击数据包的类型来量化概率结果。
对于N1，成功率为99.47％。在实验中将响应阈值设置为3。要成功发起一种攻击，攻击者至少要发送4个恶意学习响应，而其余攻击仅需要发送一个恶意数据包。这就是为什么N1的成功率略低于其他三种攻击的原因。对于N2-4，成功率为99.99％。如果V2能够在接收到恶意数据包之前发送学习请求，则攻击者将失败。但是根据结果，这不太可能发生。
为了更深入地了解网络因素将如何影响成功率，利用数据包丢失来演示PMC的功能。上图显示，N1的成功率下降的幅度远大于其他三种攻击，因为N1的攻击者需要成功发送至少4个恶意数据包才能确保成功。由于N2-4以相同的攻击时间窗口为目标，因此它们具有相同的成功率。对于N1-4，一旦受害者车辆进入其通讯范围，攻击者应立即发起攻击。丢包率（PLR）和两个CV设备之间的距离呈正相关，在高速公路环境中，如果两个CV设备相距450m，则PLR约为42％，其中450m是最长的通信距离。重点分析了当受害车辆进入攻击者的通信范围时的成功率，这对于攻击者而言是最坏的情况（PLR：42％）。虽然丢包会降低攻击成功率，但也会影响正常包的传输，导致关键CV安全包的丢失。
B. PMP漏洞
CVAnalyzer在VENTOS 和PLEXE的PMP中识别出15种攻击。在已识别的漏洞中，A1-4与可用性问题并不直接相关，而是其他攻击的基础。尽管本文分析的PMP是学术原型，但主要贡献是验证方法，该方法可普遍应用于未来的PMP协议。
在以下描述中，V1和V2仍代表车辆。V1是前行车辆，而V2通常是跟随者。它们的相对位置因情况而异。
1）拆分触发式攻击（Split Trigger Attacks）
A3和A4都可以在任何位置触发拆分行动。在不牺牲自己的速度稳定性的情况下，在A3中，攻击者可以进一步导致高效率的车辆进入和离开队伍，这会降低效率和安全性。
攻击步骤：在A3中，攻击者首先与V1合并为恶意跟随者。然后，V2将MERGE_REQ发送到V1并加入队伍。这时，攻击者有意将错误的编号为2的LEAVE_REQ发送给V1，其中深度编号表示车辆为V2。因此，V1错误地在V2的位置启动了拆分操作。切分过程之后，V2从攻击者那里接收信标消息，并再次与前队伍并。通过反复触发V2的合并和拆分操作，攻击者降低了V2的速度稳定性。
2）PMP阻止攻击（PMP Block Attacks）
这是VENTOS和PLEXE当前PMP设计中最常见的漏洞（A5-14）类型，它会误导受害车辆保持繁忙状态。在这里仅描述A7。
攻击步骤：在A7中，攻击者首先通过A2加入队伍，其目的是阻止拆分行动。通常，只有领航者可以发起拆分行动，但跟随者不能。攻击者可以利用A3和A4误导领航者以将SPLIT_REQ发送给任何指定的成员。在A7中，攻击者从V1接收到SPLIT_REQ，但选择不回复SPLIT_ACCEPT。因此，领航者将继续等待分开的答复。此时，如果攻击者之前的V2接近目的地并想离开队伍，则V1将无法处理离开请求或管理拆分过程为V2创建空间。如果车辆前后没有足够的空间，则V2直接更改车道是很危险的。
3）不一致攻击（Inconsistency Attack）
此攻击旨在为受害跟随者分配一个错误的深度编号，该深度编号与队伍成员列表中的索引不一致。拆分行动中使用了队伍的深度，因此深度数不一致会导致拆分行动失败，并且领航者/跟随者离开机动。攻击步骤。在此攻击中，攻击者首先以追随者身份加入V1的队伍。然后，攻击者放慢速度，在自己和V1之间创建较大的差距（例如100m）。
此时，V2更改其车道并在V1之后行驶。V2从V1接收信标消息，并将MERGE_REQ发送到V1。与V1合并后，V1通过将V2的ID附加到队伍成员列表来更新其本地状态，指示V2的实际队伍深度为2。但是，V2仅从前车V1接收深度为0的信标消息；因此，V2错误地将其深度设置为1。这时，攻击者将LEAVE_REQ发送到V1。由于V1认为攻击者是中间追随者，而V2则认为攻击者在后面，因此它将SPLIT_REQ发送到V2以便为攻击者创建后方空间。在VENTOS中，观察到CHANGE_PL不会显示绝对深度，但会携带深度信息的相对变化，因为领航者可以方便地向所有跟随者发送一个CHANGE_PL而不是多个不同的CHANGE_PL。在拆分操作期间，V2从V1接收CHANGE_PL，深度变化为-2。在本地更新深度信息时，V2的PMP会为无效的新深度引发错误：1-2 =-1，这可能会损害PMP的可用性，并终止拆分行动。
A. 安全影响
通过设计，CV安全应用程序有望提高人身安全性。但是实验结果表明，P2PCD攻击可以完全消除CV应用程序的优势（例如，前向碰撞警告（FCW）），这违反了CV应用程序的最初目标。
追尾碰撞场景w/FCW：首先设置了一个后端碰撞场景，并演示了具有V2V安全应用程序前撞警告（FCW）的车辆可以避免事故（下图a）。追尾碰撞场景包括前车（V1）和后车（V2），其初始参数在上表中。FCW提醒驾驶员，以避免撞到道路上其他车辆的尾端。遵循Cohda SDK中的FCW设计，以主动监控两辆车之间的距离。一旦距离小于安全距离，FCW将警告驾驶员。由于FCW不能直接控制车辆，因此在收到FCW警告后，要求模拟车辆保持安全速度。值得注意的是，利用无碰撞的Krauss汽车跟随模型来计算安全距离和安全速度。
在模拟过程中，两辆车都在同一车道上行驶。通过交换BSM，它们可以监视彼此的速度，位置和加速度。两辆车之间的初始距离为30m，小于当时的安全距离，从而触发FCW。在开始模拟10s后，V1突然以最大减速度（即5m /s^2）停止。上图a显示，在10s之前由于FCW，V2保持到领先车辆的距离不断增加。因此，领先车辆突然减速后，V2有足够的空间安全地减速。
遭到攻击的w/FCW车辆：攻击者在路边发起P2PCD攻击，旨在引起交通事故，导致上图b中所示的追尾碰撞。在仿真开始时，这两种车辆都会启动P2PCD来交换证书，以便他们可以验证和处理后续的BSM，但是P2PCD攻击阻止了他们学习证书，这意味着它们无法从对等车辆中处理任何BSM。在仿真过程中，观察到FCW从未触发，因此V2加速到最大速度并跟随V1。在10 s时，V1开始以最大减速度（5m/s^2）减速。由于两辆车彼此之间距离太近（即54m），并且V2的最大减速度为2m/s^2，因此V2最终碰撞到V1的后端。
B. 交通效率影响
通过设计，CACC旨在提高流量吞吐量并改善流量稳定性。但是，即使不牺牲自己的速度稳定性，A3和A4也会干扰交通流的稳定性，这违反了CACC的设计目标。依次将V1，攻击者和V2放在同一条车道上，并按照A3的攻击步骤运行仿真100秒钟。上图展示了受害V2的速度曲线。在正常情况下（图a），所有车辆最终将达到20m/s的稳定速度；在大约27秒的时间开始发动攻击后，将V2速度的标准差提高了43％，从而进一步干扰了随后的交通。
C. CVAnalyzer性能
上表列出了CVAnalyzer的运行性能，在具有四个2.60GHz（8核）CPU和128G内存的服务器上运行CVAnalyzer。CVAnalyzer首先浏览所有可达状态，然后验证给定属性。值得注意的是，在不应用状态减少的情况下，这两个模型检查任务将花费很长时间来探索可达状态。结果突出了减少状态的重要性和有效性。
基于前几节的讨论，在协议设计中提出了解决方案：
1.验证所有学习响应的权限；
2.增加证书中颁发者字段和SPDU中学习请求字段的截断哈希大小；
3.禁止单播学习请求；
4.将发送者身份与CV证书绑定；
5.在本地或远程跟踪队伍配置数据；
6.设计并集成错误恢复机制。
在本文中，介绍了自动进行Dos漏洞分析的CVAnalyzer。CVAnalyzer成功地在P2PCD中检测到4种新的DoS攻击，在PMP中成功检测到15种攻击；此外还构建了实用的漏洞利用程序，并在真实的测试平台上进行了验证。已经向IEEE 1609工作组报告了4种P2PCD攻击并得到了确认。最后讨论了造成这些漏洞的根本原因，并提出了有效的缓解措施。
- 结尾 - 精彩推荐 【技术分享】针对以太坊Dapp攻击事件的全面评估 Zigator：分析Zigbee智能家居的安全性 【技术分享】IoT环境中针对用户隐私的新型多阶段隐私攻击 戳“阅读原文”查看更多内容 原文始发于微信公众号（安全客）：【技术分享】CVAnalyzer：自动发现互联车辆协议中的拒绝服务漏洞
