该论文提出了一种名为Owl的新框架，用于安全协议的组合验证。现有的计算安全协议验证工具要么缺乏模块化，要么缺乏自动化。Owl通过新颖地使用信息流类型和细化类型来实现加密安全的证明。该框架允许对安全协议进行基于类型的模块化描述，其中不相交的子协议可以被独立编程并通过自动化类型检查自动证明安全。作者为Owl提供了形式化的安全证明，基于一个核心语言，该语言支持对称和非对称密码原语、Diffie-Hellman操作以及通过随机预言机进行哈希。他们还实现了Owl的类型检查器，以及一个将协议提取到Rust的原型机制，并在14个案例研究上进行了评估，包括简化版的SSH密钥交换和Kerberos。实验结果表明，Owl能够有效地验证真实世界协议的简化版本，同时提供模块化和自动化。