该论文针对证书透明化（Certificate Transparency, CT）这一已被所有主流浏览器支持的 TLS 证书生态机制，重新梳理其安全目标并给出严格的形式化分析。CT 的设计初衷是降低对证书颁发机构（CA）的信任依赖：所有 CA 必须把签发的证书写入公开日志，并由第三方监控方对日志的合规性与一致性进行检查。整个体系涉及 CA、日志运营方（logger）、监控方（monitor）以及终端用户客户端四个角色，彼此之间存在复杂的校验关系，因此很难精确说明 CT 究竟如何在引入复杂基础设施的代价下消除信任假设。作者指出，此前在 Dolev-Yao 符号模型与计算模型下的分析都只使用了高度简化的模型，并且其安全定义是为 CA 量身定制的，抓取到的其实是设计特性而非真正要保证的目标属性。本文主张把「可问责性（accountability）」确立为 CT 的核心目标，并在 Dolev-Yao 模型中展开系统性分析：先从传统 PKI 出发，逐层过渡到 CT，再进一步分析针对 SCT 审计（SCT Auditing）与 Gossiping 的扩展提案。分析结论表明，朴素 CT 方案在「日志诚实」的假设下才能提供可问责性，即它仍依赖一个诚实日志；SCT 审计扩展可以消除这一假设，而 Gossiping 扩展则无法消除该假设。该工作为理解 CT 及其扩展的真实信任边界提供了更精确的密码协议层面依据。

该论文针对企业级 X.509 证书资产管理中的优先级排序难题提出解决方案。大型组织往往持有数百万张证书，虽然有基于 CA/Browser Forum 基线要求、NIST IR 8547/SP 800-57 及密码强度标准构建的确定性合规检查工具，能精确定位违规项并指导修复，但把所有证书都跑一遍完整确定性分析在运维上不可行。为此作者设计了 X-amine509，一个两级分诊（triage）系统：第一阶段用机器学习模型快速预测每张证书的风险水平并排序，第二阶段只把排名最高、风险最大的证书送入完整的确定性分析，从而在保证关键缺陷不漏检的前提下大幅降低计算开销。风险评分被量化为一个复合分值，由 177 项缺陷检查项汇总而成，并按安全严重性划分为四个等级，从密码学层面的彻底攻破一直覆盖到轻微合规偏差。作者从财富 500 强、.gov 和 .edu 域名采集了 1,027,714 张证书，用该评分体系逐一打分。在 201,976 张留出测试集上，最佳模型 Extra Trees 取得 R²=0.993、MAE=2.26；决策树模型在单机上达到每秒 370 万张证书的推理速度，R²=0.986。排序质量验证了分诊价值：聚合 NDCG 超过 0.997，严重性等级分类准确率 99.76%，对关键等级缺陷的召回率达 98.90%。十三个月后作者又采集 571,374 张证书测试模型随时间推移的耐久性，Extra Trees 与决策树仍保持 MAE 低于 6.8、R² 至少 0.915、聚合 NDCG 高于 0.988、严重性等级准确率至少 99.52%、关键等级召回率至少 97.03%，说明模型未因证书生态演进显著退化。特征重要性分析指出，有效期长度、Extended Key Usage 配置、负序列号编码和自签名状态是最强的风险预测因子，为分诊阶段提供了粗粒度可解释性。

X.509 公钥基础设施（PKI）是广泛使用的可扩展且灵活的身份认证机制，但其标准文本由自然语言编写，存在设计复杂、歧义和欠规定（under-specification）等问题，导致实现者难以完全遵循标准。实际中，很多 X.509 实现库因不符合标准而出现缺陷，进而可能使依赖应用遭受冒充攻击或互操作性问题。本文旨在通过重新工程化（re-engineering）并形式化 X.509 标准中一个广泛使用的片段，并基于此开发一个高可信实现来缓解上述问题。作者的核心思路是将语法要求与语义要求解耦。对于语法要求，他们发现属性文法（attribute grammar）的一个受限片段足以形式化 X.509 的语法结构。对于语义要求，作者使用无量词一阶逻辑（Quantifier-Free First-Order Logic, QFFOL）来精确描述最常用 X.509 功能上的语义约束。有趣的是，使用 QFFOL 所得到的规范是可执行的（executable specification），并且可以由 SMT 求解器高效地执行检查。作者利用这些洞见开发了一个名为 CERES 的高可信 X.509 实现。他们使用 200 万条真实证书链和 200 万条合成证书链，将 CERES 与 mbedTLS、OpenSSL 和 GnuTLS 三个主流库进行了对比实验。结果表明，CERES 能够正确拒绝格式错误和无效的证书，而主流库中存在的相关的非合规缺陷则被暴露出来。该工作为使用形式化方法重新工程化自然语言标准提供了可行范例，也为提升 X.509 生态的整体安全性提供了一条建设性路径。本文适合 PKI/证书安全研究人员、标准制定者以及负责实现或审计 TLS/X.509 库的软件工程师阅读。

该论文针对协作式车辆队列（vehicle platooning）中的安全问题展开研究。协作式队列通过车辆间的物理感知与V2V（车对车）消息交换来协调加速、制动和转向，能显著提升高速公路安全性、燃油效率和交通流量。然而，V2V消息的真实性和完整性对行车安全至关重要，现有V2V/V2X标准虽然引入了PKI（公钥基础设施）来提供密码学认证，但PKI无法将车辆的数字化身份与其物理状态（如位置、速度等）绑定。因此，一个拥有合法密码学凭证的车辆可以在远程位置对队列造成影响，即所谓的'远程注入攻击'或'身份-物理状态脱节'问题。为此，作者提出了一种名为PoF（Proof-of-Following，跟随证明）的新机制。PoF的核心思想是让车辆向队列证明其确实在物理上跟随前车，而非仅仅拥有有效证书。该机制通过结合物理感知数据（如雷达、摄像头测距）与V2V消息中的动态状态信息（如位置、速度、加速度）来生成不可伪造的证明，使队列中的其他成员能够验证某辆车是否真正处于队列中的宣称位置。论文可能还设计了具体的协议流程、密码学构造（如承诺方案、签名聚合等）以及安全分析，并通过仿真或实验验证了PoF在抵抗远程攻击、保持低通信开销和高验证效率方面的有效性。主要贡献包括：提出身份-物理绑定缺失这一关键漏洞的解决方案；设计可证明安全且轻量级的验证协议；评估其在不同攻击模型下的鲁棒性。适合智能交通系统安全研究员、V2X标准制定者、汽车安全工程师及关注物理层与密码层融合的学者阅读。

标准5G认证与密钥协商（5G-AKA）仅验证存储在通用用户身份模块（USIM）上的订阅凭证，而不验证持有该凭证的物理设备或其启动状态。在战术5G部署中，用户设备可能被捕获、篡改、重新投入使用，或与移植的订阅凭证一同使用，这一安全缺口尤为严重。本文提出名为“Battlefield 5G”的预认证框架，面向5G独立组网，在标准注册流程被接受之前，结合双X.509设备证书检查和基于可信平台模块（TPM）的启动证明。其设计在5G基站（gNB）上设置外层证书挑战，在5G核心网中的接入与移动性管理功能（AMF）上设置独立的内层证书挑战，并由核心网侧的证明代理验证TPM的平台配置寄存器（PCR）引用。通过在gNB侧实现无线资源控制（RRC）转发门，并在AMF侧实现保存-重放机制，多轮证书与证明挑战-响应交换可插入注册流程，而无需修改任何3GPP非接入层（NAS）消息结构或新增NAS消息类型。作者基于B210通用软件无线电外设（USRP）测试平台，扩展了srsRAN、srsUE和Open5GS，并在UE中集成硬件TPM 2.0。原型阻止了SIM移植、伪造证书、固件篡改和重放攻击。在六次试验中，Battlefield 5G将平均入网时延从1886毫秒增加至2260毫秒，额外引入373.4毫秒的预认证开销，同时保留了标准的5G-AKA、安全模式和PDU会话流程。该研究为战术或高安全要求环境中的5G设备提供了一种实用的增强认证机制，并为未来标准演进提供了参考。

随着新太空时代的发展，近地轨道上由独立实体运营的卫星数量激增，这带来了更丰富的空间服务需求，但也要求安全、近实时的协调。高效的太空资产认证对于下一代任务至关重要。传统依赖地面的公钥基础设施（PKI）存在延迟和操作瓶颈，限制了在动态太空环境中的可扩展性和可用性。本文提出了基于太空的PKI架构设计，将证书管理和验证从地面基础设施转移到太空，减少对地面站的依赖，同时实现互操作性和跨实体协作。文中介绍了两种部署方案：一是空间-地面集成PKI，配备在轨验证权威机构；二是完全自主的基于太空的PKI，实现在太空签发和验证。文章分析了在多运营商环境中部署的权衡，包括可扩展性、可用性、安全性、成本和操作复杂性。此外，提供了基础延迟分析以说明在轨信任管理的性能影响。该研究为未来安全空间通信提供了重要的技术路线，适合太空安全工程师、PKI设计人员和卫星通信研究者阅读。