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