請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/87731
標題: | 快速常數時間模反元素演算法程式之形式驗證 Formal Verification of Fast Constant Time Modular Inverse Algorithm Implementations |
作者: | 陳翰霆 Han-Ting Chen |
指導教授: | 陳偉松 Tony Tan |
關鍵字: | 形式驗證,模型檢測,模反元素,輾轉相除法,密碼學實作,Curve25519, formal verification,model checking,modular inversion,gcd,cryptographic programs,Curve25519, |
出版年 : | 2023 |
學位: | 碩士 |
摘要: | 我們使用形式驗證工具 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. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/87731 |
DOI: | 10.6342/NTU202300852 |
全文授權: | 同意授權(全球公開) |
顯示於系所單位: | 資訊工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-111-2.pdf | 887.57 kB | Adobe PDF | 檢視/開啟 |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。