請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/87731完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 陳偉松 | zh_TW |
| dc.contributor.advisor | Tony Tan | en |
| dc.contributor.author | 陳翰霆 | zh_TW |
| dc.contributor.author | Han-Ting Chen | en |
| dc.date.accessioned | 2023-07-19T16:10:13Z | - |
| dc.date.available | 2023-11-09 | - |
| dc.date.copyright | 2023-07-19 | - |
| dc.date.issued | 2023 | - |
| dc.date.submitted | 2023-06-17 | - |
| dc.identifier.citation | [1] D. J. Bernstein and B.-Y. Yang. Fast constant-time gcd computation and modular in version. 2019(3):340–398, 2019. https://tches.iacr.org/index.php/TCHES/article/view/8298.
[2] p. c. Daniel J. Bernstein and P. Wuille. safegcd-bounds. https://github.com/sipa/safegcd-bounds, 2021. [3] W. Decker, G.-M. Greuel, G. Pfister, and H. Schönemann. SINGULAR 4-3-0 — A computer algebra system for polynomial computations. http://www.singular.uni-kl.de, 2022. [4] Y.-F. Fu, J. Liu, X. Shi, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. Signed cryptographic program verification with typed cryptoline. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS ’19, page 1591–1606, New York, NY, USA, 2019. Association for Computing Machinery. [5] P. L. Montgomery. Modular multiplication without trial division. Mathematics of Computation, 44:519–521, 1985. [6] A. Niemetz, M. Preiner, and A. Biere. Boolector 2.0. J. Satisf. Boolean Model. Comput., 9(1):53–58, 2014. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/87731 | - |
| dc.description.abstract | 我們使用形式驗證工具 Cryptoline 驗證兩個利用 Bernstein-Yang 演算法的模反元素程式，其中一個是目前以模數為 2^255-19 最快的 x86 實作。本論文提供了驗證此程式所用到的驗證細節與技巧。我們利用形式化方法驗證了此程式的正確性，也展現了一個形式驗證在證明密碼學系統的可信度上的應用。 | zh_TW |
| dc.description.abstract | 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. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2023-07-19T16:10:13Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2023-07-19T16:10:13Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | Verification Letter from the Oral Examination Committee i
Acknowledgements iii 摘要 v Abstract vii Contents ix List of Figures xiii List of Tables xv Denotation xix Chapter 1 Introduction 1 Chapter 2 Preliminary 3 2.1 Modular Inverse Algorithms . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Original Bernstein-Yang Algorithm . . . . . . . . . . . . . . . . . . 4 2.2.1 Definition of 2-adic division steps . . . . . . . . . . . . . . . . . . 4 2.2.2 Iterations of 2-adic division steps . . . . . . . . . . . . . . . . . . . 5 2.2.3 Fast computation of iterations of 2-adic division steps . . . . . . . . 8 2.2.4 Fast modular inversion computation . . . . . . . . . . . . . . . . . 9 2.3 Improved Bernstein-Yang Algorithm . . . . . . . . . . . . . . . . . 11 Chapter 3 Introduction to Cryptoline 13 3.1 Why Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2 What is CRYPTOLINE . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.1 Property . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2.2 The structure of a CRYPTOLINE program . . . . . . . . . . . . . . . 18 3.2.3 CRYPTOLINE instructions . . . . . . . . . . . . . . . . . . . . . . . 19 3.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.3.1 Examples of modeling . . . . . . . . . . . . . . . . . . . . . . . . 23 3.3.2 CRYPTOLINE tricks . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.3.3 Verify an assembly program . . . . . . . . . . . . . . . . . . . . . 31 Chapter 4 Verifying a Simple Implementation 33 4.1 x86 25519 Implementation . . . . . . . . . . . . . . . . . . . . . . . 34 4.1.1 C implementation of fpinv25519.c . . . . . . . . . . . . . . . . . 34 4.2 Verifiy Simple Subroutines . . . . . . . . . . . . . . . . . . . . . . . 39 4.2.1 Verify modular addition . . . . . . . . . . . . . . . . . . . . . . . . 39 4.2.2 Verify conditional modular negation . . . . . . . . . . . . . . . . . 40 4.2.3 Verify signed multiplication with addition . . . . . . . . . . . . . . 40 4.2.4 Verify modular multiplication . . . . . . . . . . . . . . . . . . . . . 41 4.2.5 Verify signed multi-limb multiplication with addition . . . . . . . . 41 4.3 Verify 62 divstep iterations . . . . . . . . . . . . . . . . . . . . . . . 43 4.3.1 Pseudo code of the subroutine . . . . . . . . . . . . . . . . . . . . 43 4.3.2 Verify 1 divstep iteration . . . . . . . . . . . . . . . . . . . . . . . 44 4.3.3 Model the subroutine . . . . . . . . . . . . . . . . . . . . . . . . . 49 4.3.4 Verify signed multi-limb multiplication and shift . . . . . . . . . . . 51 4.3.5 Completeness of verification of the subroutine . . . . . . . . . . . . 52 4.4 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Chapter 5 Verifying a Fast Vectorized Implementation 55 5.1 Vectorized x86 25519 Implementation . . . . . . . . . . . . . . . . . 56 5.1.1 Outline of the assembly code . . . . . . . . . . . . . . . . . . . . . 57 5.2 Verify 20 divstep iterations . . . . . . . . . . . . . . . . . . . . . . . 62 5.2.1 An alternative definition of divstep . . . . . . . . . . . . . . . . . . 63 5.2.2 Verify each divstep iteration . . . . . . . . . . . . . . . . . . . . . 64 5.3 Verify vectorized update . . . . . . . . . . . . . . . . . . . . . . . . 67 5.3.1 Pseudo code of the subroutine . . . . . . . . . . . . . . . . . . . . 67 5.3.2 Computing in parallel . . . . . . . . . . . . . . . . . . . . . . . . . 71 5.3.3 Computing with Montgomery multiplication . . . . . . . . . . . . . 72 5.3.4 Verify signed shift right computed with unsigned shift right . . . . . 74 5.3.5 Use a proof from Coq . . . . . . . . . . . . . . . . . . . . . . . . . 75 5.3.6 Reduce the output range . . . . . . . . . . . . . . . . . . . . . . . . 76 5.4 Verify radix 2^30 number multiplication with reduction . . . . . . . . 78 5.5 Verify simple subroutines . . . . . . . . . . . . . . . . . . . . . . . 80 5.6 Interleaving instructions . . . . . . . . . . . . . . . . . . . . . . . . 82 5.7 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 Chapter 6 Concluding Remarks 85 6.1 Time Consumption . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 6.2 The Verified Results . . . . . . . . . . . . . . . . . . . . . . . . . . 86 References 87 Appendix A — Proof 89 A.1 Proof about arithmetic precision . . . . . . . . . . . . . . . . . . . . 89 Appendix B — Table 91 B.1 Verification Time of the Simple Implementation . . . . . . . . . . . 91 B.2 Verification time of the Fast Vectorized Implementation . . . . . . . 92 | - |
| dc.language.iso | en | - |
| dc.subject | 形式驗證 | zh_TW |
| dc.subject | Curve25519 | zh_TW |
| dc.subject | 密碼學實作 | zh_TW |
| dc.subject | 輾轉相除法 | zh_TW |
| dc.subject | 模反元素 | zh_TW |
| dc.subject | 模型檢測 | zh_TW |
| dc.subject | formal verification | en |
| dc.subject | model checking | en |
| dc.subject | modular inversion | en |
| dc.subject | gcd | en |
| dc.subject | cryptographic programs | en |
| dc.subject | Curve25519 | en |
| dc.title | 快速常數時間模反元素演算法程式之形式驗證 | zh_TW |
| dc.title | Formal Verification of Fast Constant Time Modular Inverse Algorithm Implementations | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 111-2 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.coadvisor | 王柏堯 | zh_TW |
| dc.contributor.coadvisor | Bow-Yaw Wang | en |
| dc.contributor.oralexamcommittee | 楊柏因;黃鐘揚 | zh_TW |
| dc.contributor.oralexamcommittee | Bo-Yin Yang;Chung-Yang Huang | en |
| dc.subject.keyword | 形式驗證,模型檢測,模反元素,輾轉相除法,密碼學實作,Curve25519, | zh_TW |
| dc.subject.keyword | formal verification,model checking,modular inversion,gcd,cryptographic programs,Curve25519, | en |
| dc.relation.page | 92 | - |
| dc.identifier.doi | 10.6342/NTU202300852 | - |
| dc.rights.note | 同意授權(全球公開) | - |
| dc.date.accepted | 2023-06-17 | - |
| dc.contributor.author-college | 電機資訊學院 | - |
| dc.contributor.author-dept | 資訊工程學系 | - |
| 顯示於系所單位： | 資訊工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-111-2.pdf | 887.57 kB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。