快速常數時間模反元素演算法程式之形式驗證

Abstract

我們使用形式驗證工具 Cryptoline 驗證兩個利用 Bernstein-Yang 演算法的模反元素程式，其中一個是目前以模數為 2^255-19 最快的 x86 實作。本論文提供了驗證此程式所用到的驗證細節與技巧。我們利用形式化方法驗證了此程式的正確性，也展現了一個形式驗證在證明密碼學系統的可信度上的應用。

In this thesis, we conducted formal verification using the Cryptoline tool on two x86 implementations of the Bernstein-Yang algorithm, both designed to operate in constant time. Notably, one of these implementations represents the current fastest constant time modular inversion implementation for prime modulus 2^255-19 on x86. Our study provides comprehensive details and verification techniques for verifying these assembly implementations. By formal methods, the correctness of these implementations is systematically demonstrated. The results of this study provide substantial evidence for the effectiveness of formal verification in ensuring the accuracy and reliability of cryptographic systems.