本论文针对 EMV 非接触式支付系统中存在的中继攻击（relay attack）问题展开研究。中继攻击允许攻击者在持卡人与读卡器之间转发消息，从而在用户不知情的情况下完成支付，例如通过无线方式窃取资金。论文首先评估了现有的防护措施：Apple Pay 要求用户指纹或 Face ID 授权；Mastercard 和 Visa 则提出了基于时间或加密的协议来阻止中继。作者发现，在交通支付模式下，可以利用中继绕过 Apple Pay 的锁屏，从已锁定的 iPhone 向任意 EMV 读卡器非法支付任意金额，无需用户授权。此外，Visa 提出的中继对抗措施可被 root 后的智能手机绕过。对于 Mastercard 的防护，作者指出其时间限制在 ISO 14443 协议层实施比在 EMV 协议层更可靠。基于这些发现，论文提出了一种新的中继抵抗协议 L1RP（Layer 1 Relay Protection），并利用 Tamarin 证明器对手机支付（含或不含用户认证）的不同模式进行建模，形式化验证了 Apple 和 Visa 建议（Samsung 采用）的解决方案，并证明 L1RP 能够有效抵御中继攻击。该研究为改进非接触式支付安全提供了重要理论和实践依据。

现有程序验证器能够证明安全协议实现的高级属性，但由于需要大量人工努力，难以扩展到大型代码库。针对这一挑战，本文提出了一种名为Diodon的新方法。Diodon通过将代码库分割为协议实现（核心）和其余部分（应用程序）来解决扩展性问题。这种分割允许对安全关键的核心应用强大的半自动验证技术，同时通过全自动静态分析确保应用程序不能破坏为核心证明的安全属性，从而将验证扩展到整个代码库。静态分析通过证明I/O独立性来实现，即应用程序内的I/O操作与核心的安全相关数据（如密钥）无关，并且应用程序满足核心的要求。作者首先通过证明可以安全地允许应用程序执行独立于安全协议的I/O操作，其次证明手动验证和静态分析能够可靠地组合，从而证明了Diodon的正确性。评估在两个案例上进行：一个签名的Diffie-Hellman密钥交换实现，以及一个大的（10万+行代码）生产级Go代码库，该代码库实现了一个密钥交换协议。通过使用自动激活程序验证器Gobra验证约1%代码的核心，在不到3人月内获得了机密性和注记一致性保证。该方法为大型安全协议实现的可扩展验证提供了一种新途径。

本文提出Pepper，一种高带宽匿名广播协议，针对全局敌手提供加密发送者匿名性。Pepper基于双服务器DC-net架构，但引入三项关键创新：1）使用可验证分布式点函数的自包含匿名注册子协议，无需外部拨号服务；2）通过分布式多点函数支持批量消息，允许每个发送者每个epoch发送多条消息且只需单次审计；3）基于秘密共享证明的轻量级访问控制机制。与现有系统相比，Pepper显著提升了大规模数据传输的吞吐量。实现表明，Pepper达到毫秒级注册审计，可高效扩展至数千通道，有效消息速率比最先进方案高1.2至20倍。此外，Pepper设计注重实际部署，能与Tor和联邦社交网络自然兼容。该研究主要贡献在于突破了DC-net在带宽和可扩展性上的瓶颈，并提供了实用的匿名广播方案。