Proved generation of implementations from computationally secure protocol specifications
Proved generation of implementations from computationally secure protocol specifications
复制标题
经过验证的计算安全协议规范的实现生成
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
B. Blanchet
中科院分区：
文献类型：
--
作者：
David Cadé;B. Blanchet
为了获得实现的安全协议证明是安全的计算模型，我们以前实现了一个编译器，该编译器需要一个规范的协议在输入语言的计算协议验证器CryptoVerif和翻译成OCaml实现。然而，到目前为止，这个编译器还没有被证明是正确的，所以我们对生成的实现没有真实的保证。在本文中，我们填补了这一空白。我们证明，该编译器保留了CryptoVerif证明的安全属性：如果对手有概率p破坏生成的代码中的安全属性，那么存在一个对手，打破属性具有相同的概率p的CryptoVerif规范。因此，如果协议规范在计算模型中被CryptoVerif证明是安全的，那么生成的实现也是安全的。
In order to obtain implementations of security protocols proved secure in the computational model, we have previously implemented a compiler that takes a specification of the protocol in the input language of the computational protocol verifier CryptoVerif and translates it into an OCaml implementation. However, until now, this compiler was not proved correct, so we did not have real guarantees on the generated implementation. In this paper, we fill this gap. We prove that this compiler preserves the security properties proved by CryptoVerif: if an adversary has probability p of breaking a security property in the generated code, then there exists an adversary that breaks the property with the same probability p in the CryptoVerif specification. Therefore, if the protocol specification is proved secure in the computational model by CryptoVerif, then the generated implementation is also secure.