车载自组织网络将无线通信技术与现代汽车技术相结合,实现了车辆之间、车辆与道路基础设施之间的实时通信,能够有效提升道路交通安全和运输效率,为驾驶者提供更良好的驾驶体验。然而,无线通信的开放性导致车辆面临来自外部的各种威胁,带来的安全问题严重影响了车联网应用的落地。安全协议是解决以上问题的有效方法,然而目前已经存在的大量安全协议被证实存在各种安全漏洞,而且一些安全协议在实现过程中,可能会引入一些新的问题,所以如何对协议程序的执行逻辑进行安全性的检验逐渐成为了人们关注的重点之一。本文针对典型车联网通信协议交互逻辑的安全性问题进行了研究,主要研究成果如下:首先,搭建了面向典型车联网通信协议的交互环境。使用业界主流的大规模网络仿真软件平台对典型车联网通信协议的交互过程进行了模拟,并设计了一种面向车联网通信协议的程序交互方案,能够利用车联网通信协议中各个协议端交互的消息数据来构造新的数据包,有效减少了学习端构造数据包的复杂度。其次,研究了面向多端的状态机学习优化算法。车联网协议往往存在多个通信实体,而传统的状态机学习算法只能面向单端目标,针对这个问题提出了一种面向多端的状态机学习方法,能够同时针对多个协议端的状态机进行学习。其次,为了解决传统一致性测试算法需要与目标协议端进行大量交互的问题,提出了基于最短路径的测试序列优化算法,并在此基础上使用贪心策略算法进一步优化,实验结果表明,在针对目标协议进行学习的过程中,所提出的方法相对于传统的一致性测试算法平均减少了30%的重置次数和24%的交互次数。再次,研究了面向协议状态机的自动化安全验证方法。针对学习得到的状态机模型,制定了一系列转换规则,实现了状态机模型到形式化描述语言的自动转换,并使用形式化验证工具对转换后的协议流程进行了安全性验证。最后,在本文研究成果的基础上,设计并实现了车联网通信协议交互逻辑安全验证系统。经过对系统的程序交互模块、模型学习模块和安全验证模块三部分的功能性测试,结果证明系统能够有效验证目标车联网通信协议交互逻辑的安全性。