Các chứng minh hình thức cho hai ứng cử viên của mật mã hậu lượng tử

Bài viết dưới đây trình bày kết quả đánh giá về tính đúng đắn của mô tả thuật toán, cũng như cài đặt của nó dưới góc nhìn chứng minh hình thức cho hai trong số các thuật toán lọt vào vòng 3 của quá trình chuẩn hóa thuật toán mật mã hậu lượng tử của NIST.

GIỚI THIỆU

Quá trình chuẩn hóa mật mã sau lượng tử của NIST hiện đang ở giai đoạn thứ ba, có 7 ứng viên chính thức lọt vào vòng chung kết thứ ba và 8 ứng viên dự bị đang được xem xét để tiêu chuẩn hóa. NIST đã tổ chức trực tuyến Hội nghị Tiêu chuẩn hóa Mật mã Hậu lượng tử lần thứ ba vào ngày 7-9 tháng 6/2021 để thảo luận về các khía cạnh khác nhau của những ứng cử viên này và thu được những phản hồi có giá trị cho các lựa chọn cuối cùng. Mỗi nhóm mà đã đệ trình các thuật toán trong số 15 thuật toán lọt vào vòng chung kết được mời đưa ra một bản cập nhật ngắn về thuật toán của họ. Tất nhiên, trong hội nghị cũng còn một số báo cáo khác [1]. Bài viết này sẽ trình bày về tình trạng chứng minh hình thức của hai ứng cử viên, đó là Kyber và Saber.

KYBER VÀ SABER

Kyber là cơ chế bọc gói khóa (Key Encapsulation Mechanism - KEM) được chứng minh có độ an toàn IND-CCA2 dựa trên độ khó của việc giải bài toán learning-with-errors (LWE) trên lưới mô-đun. Bản đệ trình liệt kê ba bộ tham số khác nhau nhằm vào các mức an toàn khác nhau. Cụ thể, Kyber-512 hướng đến độ an toàn tương đương với AES-128, Kyber-768 hướng tới độ an toàn tương đương với AES-192 và Kyber-1024 hướng tới độ an toàn tương đương với AES-256.

Đối với những người dùng quan tâm đến việc sử dụng Kyber, có những khuyến cáo sau:

Sử dụng Kyber nên theo chế độ lai ghép, kết hợp với độ an toàn “tiền lượng tử” đã được thiết lập; ví dụ như kết hợp với Diffie-Hellman đường cong Elliptic.
Nên sử dụng bộ tham số Kyber-768, theo một phân tích rất thận trọng - đạt được nhiều hơn độ an toàn 128 bit chống lại tất cả các tấn công cổ điển và lượng tử đã biết. Saber là cơ chế bọc gói khóa an toàn được chứng minh có độ an toàn IND-CCA2 dựa trên độ khó của của bài toán learning-with-rounding (LWR) trên mô-đun. LWR là một biến thể của LWE. Saber cung cấp ba cấp độ bảo mật: LightSaber có mức bảo mật hậu lượng tử tương tự như AES-128, Saber có mức bảo mật hậu lượng tử tương tự như AES-192 và FireSaber có mức bảo mật hậu lượng tử tương tự như AES-256.

Kyber và Saber là hai ứng cử viện nặng ký cho mật mã hậu lượng tử. Những thông tin khá chi tiết về hai thuật toán này được đăng tải tại các trang web https://pq-crystals.org/kyber/ và https://www.esat.kuleuven.be/cosic/pqcrypto/saber/. Hai thuật toán này đã thu hút được sự quan tâm lớn của cộng đồng mật mã, có rất nhiều công trình nghiên cứu về hai thuật toán này. Trên trang web của Hiệp hội quốc tế những nhà nghiên cứu mật mã (eprint.iacr.org), chỉ tính riêng trong năm 2021 (cho tới ngày 9/11/2021) đã có 12 bài báo viết về Kyber (các bài số 1364, 1311, 1307, 1222, 1189, 986, 956, 874, 563, 561, 483 và 193) và có 8 bài viết về Saber (các bài số 1452, 1364, 1202, 995, 986, 902, 193 và 079).

HAI CÔNG CỤ DÙNG CHO CHỨNG MINH HÌNH THỨC

Chứng minh hình thức (formal verification)

Trước đây, các thuộc tính an toàn của các lược đồ mật mã đã được xác nhận bằng các chứng minh độ an toàn viết tay. Tuy nhiên, sự đổi mới và phát triển trong lĩnh vực mật mã đã dẫn đến sự gia tăng đáng kể trong độ phức tạp của các lược đồ mật mã. Do đó, các chứng minh độ an toàn viết tay về cơ bản trở nên rất khó khăn để được thực hiện một cách chuẩn xác. Trên thực tế, tồn tại nhiều trường hợp chứng minh độ an toàn, mặc dù chúng đã được xem xét kỹ lưỡng và được coi là chuẩn xác, nhưng thực tế lại bị lỗi. Thậm chí tệ hơn, trong một số trường hợp, lược đồ mật mã tương ứng cũng được phát hiện là không an toàn [2]. Những trường hợp này minh chứng rõ ràng tầm quan trọng và tính khó khăn của việc xây dựng một cách đúng đắn một lược đồ mật mã và chứng minh độ an toàn của nó.

Ngoài mối quan tâm ở trên, ngay cả khi một lược đồ mật mã được xác nhận độ an toàn của nó là hoàn toàn chính xác thì các lỗi cài đặt vẫn có thể làm mất hiệu lực của các thuộc tính và bảo đảm bất kỳ của lược đồ. Kết quả là, mặc dù lược đồ hoàn toàn mạnh ở mức thiết kế, nhưng không có độ an toàn nào có thể được đảm bảo. Tương tự như quan tâm trước, tồn tại nhiều ví dụ về cài đặt bị lỗi của các hệ thống mật mã mạnh dẫn tới các tổn thương độ an toàn [3]. Điều này cho thấy tầm quan trọng của việc cài đặt mật mã một cách hợp lý và an toàn.

Để khắc phục một phần các vấn đề nói trên, lĩnh vực mật mã có sự hỗ trợ của máy tính đã được sử dụng. Lĩnh vực nghiên cứu này tìm cách phát triển các tiếp cận khác nhau để đưa ra các thuật toán mật mã sử dụng máy tính có thể xác nhận và đảm bảo tính an toàn nhằm khẳng định tính chuẩn xác, hiệu quả và độ an toàn khi sử dụng hỗ trợ từ máy tính. Việc sử dụng máy tính theo cách này làm giảm đáng kể độ phức tạp của lao động thủ công trong việc chứng minh độ an toàn và tính chuẩn xác của một lược đồ và các cài đặt của nó, đồng thời cung cấp mức độ chặt chẽ cao một cách nhất quán. Điều này cho phép thu được mức tin cậy cao hơn về độ an toàn, tính chuẩn xác của một lược đồ mật mã và các cài đặt của nó.

Quá trình chứng minh hình thức tổng quát

Sự phát triển gần đây trong lĩnh vực mật mã có sự hỗ trợ của máy tính xác nhận rằng một quy trình xác nhận hình thức tổng quát có thể được áp dụng cho các hệ thống mật mã trong thế giới thực [4]. Đặc biệt, khi đã cho đặc tả của lược đồ và chứng minh độ an toàn (viết tay), quá trình này cho phép người ta xác nhận một cách hình thức bất kỳ lược đồ nào và các cài đặt của nó. Ngoài ra, quy trình không phụ thuộc vào bất kỳ công cụ cụ thể nào, miễn là chúng cho phép thực hiện nhiệm vụ xác nhận mong muốn. Tuy nhiên, việc lựa chọn công cụ có thể ảnh hưởng đáng kể đến độ khó của quá trình. V í dụ, tùy thuộc vào các thuộc tính được xác nhận hoặc kiểu chứng minh được sử dụng. Quá trình diễn ra được tóm tắt như sau. Đầu tiên, người ta hình thức hóa đặc tả của lược đồ, các thuộc tính độ an toàn.

Sau đó, lược đồ đã được chỉ ra sẽ được chứng minh là sở hữu các thuộc tính an toàn mong muốn. Sau đó, cài đặt của lược đồ có thể được kiểm tra là chuẩn xác về mặt chức năng đối với đặc tả của lược đồ. Do đó, cài đặt được chỉ ra là tương ứng với một đặc tả, đặc tả này đã được xác nhận sở hữu một số thuộc tính mong muốn nhất định, ngụ ý cài đặt cũng sở hữu các thuộc tính này. Cuối cùng, tùy thuộc vào các công cụ có sẵn và được sử dụng, một số thuộc tính khác của cài đặt có thể được xác nhận. Ví dụ về các thuộc tính như vậy là tính an toàn bộ nhớ và có thời gian chạy không đổi.

EasyCrypt

EasyCrypt là một công cụ chủ yếu nhằm để chứng minh một cách hình thức các thuộc tính an toàn của các cấu trúc mật mã [5]. Để đạt được mục đích này, công cụ áp dụng cách tiếp cận dựa trên mã lệnh cho độ an toàn chứng minh được. Nghĩa là, các thuộc tính độ an toàn và các giả thiết khó được mô hình hóa như các chương trình xác suất. Hơn nữa, logic bao quanh bậc cao hơn của công cụ, thư viện tiêu chuẩn và các cơ chế được tích hợp sẵn cho phép suy luận toán học mở rộng, các kiểu chứng minh khác nhau (ví dụ, chơi trò chơi và dựa trên mô phỏng) và xây dựng mô-đun của hệ thống mật mã.

Mặc dù được áp dụng thuận tiện hơn ở mức thiết kế, EasyCrypt có thể được sử dụng ở cả mức cài đặt. Đặc biệt là với sự phát triển của khung như Jasmin, việc sử dụng EasyCrypt để xác nhận tính đúng đắn về mặt chức năng và thuộc tính thời gian chạy không đổi của các cài đặt cụ thể được thực hiện ít phức tạp hơn đáng kể.

Jasmin

Jasmin là một khung được thiết kế cho cài đặt mật mã tốc độ cao và tin cậy cao [6]. Khung bao gồm ngôn ngữ lập trình, trình biên dịch và một số công cụ để xác nhận (một phần) tự động các thuộc tính chương trình mong muốn. Đặc biệt, các công cụ của khung hỗ trợ nhà phát triển chứng minh một cách hình thức một cài đặt Jasmin là an toàn về bộ nhớ, thời gian chạy không đổi và đúng chức năng. Ở đây, trái với công cụ để đảm bảo an toàn về bộ nhớ, các công cụ cho tính đúng đắn của chức năng và thời gian không đổi không hoàn toàn tự động. Do đó, việc xác nhận các thuộc tính này vẫn đòi hỏi một số lao động thủ công, mặc dù công sức này là tối thiểu đối với thuộc tính thời gian chạy không đổi. Cụ thể, khi đã cho một cài đặt Jasmin, các công cụ này tạo ra mã EasyCrypt nhằm xác nhận thuộc tính tương ứng của chúng. Sau đó, mã lệnh này có thể được sử dụng để xác nhận thực sự thuộc tính được xem xét trong EasyCrypt.

CHỨNG MINH HÌNH THỨC CHO HAI DỰ TUYỂN MẬT MÃ HẬU LƯỢNG TỬ CỦA NIST

Bài thuyết trình [1] đã trình bày tiến trình của hai dự án xác nhận hình thức của các thí sinh lọt vào vòng chung kết cuộc thi PQC: một cho Kyber và một cho Saber. Mục tiêu cuối cùng của cả hai dự án là giống hệt nhau và có 2 mặt; cụ thể, cả hai dự án đều nhằm mục đích: (1) xác nhận một cách hình thức độ an toàn IND-CCA2 cho đặc tả của cơ chế bọc khóa; (2) xác nhận một cách hình thức tính đúng đắn về mặt chức năng, thuộc tính an toàn về bộ nhớ và thời gian chạy không đổi của một cài đặt mẫu và một cài đặt tối ưu của cơ chế bọc khóa. Với mục đích này, cả hai dự án đều sử dụng EasyCrypt và Jasmin.

Tại thời điểm 6/2021, tiến độ của cả hai dự án như sau. Đối với cả Kyber và Saber, một cài đặt mẫu và một cài đặt tối ưu đã được xây dựng trong Jasmin. Ngoài ra, dự án Kyber đã xác minh một cách hình thức thuộc tính IND-CPA và cận với độ chuẩn xác (1 - d) của đặc tả mã hóa khóa công khai, tính đúng đắn về chức năng và tính an toàn về bộ nhớ của cài đặt mẫu cũng như tính an toàn về bộ nhớ của cài đặt tối ưu hóa. Dự án Saber đã xác nhận một cách hình thức thuộc tính IND-CPA của lược đồ mã hóa khóa công khai và tính an toàn về bộ nhớ của cả hai cách cài đặt.

Mặc dù có vẻ không may là việc phân tích xem xét các đối thủ lượng tử vẫn chưa thể thực hiện được trong EasyCrypt, nhưng xác nhận hình thức trong thiết lập cổ điển đã cung cấp cái nhìn sâu sắc có giá trị về các lược đồ này và các thuộc tính của chúng. Nhưng trong công trình gần đây, Unruh đã xác nhận một cách hình thức độ an toàn hậu lượng tử của phép biến đổi Fujisaki-Okamoto trong công cụ qRHL [7]. Do đó, việc xác nhận các tính chất của các lược đồ Kyber và Saber trong thiết lập cổ điển cũng làm tăng độ tin tưởng vào tính đúng đắn và độ an toàn của các lược đồ này khi xem xét các đối thủ lượng tử.

TÀI LIỆU THAM KHẢO

1. Manuel Barbosa, Andreas Hülsing, Matthias Meijers and Peter Schwabe, Formal Verifcation of Post-Quantum Cryptography, https://csrc.nist.gov/CSRC/ media/ Events/third-pqc-standardization-conference/documents/ accepted-papers/meijers-formal-verification-pqc2021.pdf

2. N. Koblitz and A. Menezes, “Critical perspectives on provable security: Fifteen years of “another look” papers.” Cryptology ePrint Archive, Report 2019/1336, 2019. https://eprint.iacr.org/2019/1336.

3. D. Lazar, H. Chen, X. Wang, and N. Zeldovich, “Why does cryptographic software fail? a case study and open problems”, in Proceedings of 5th Asia-Pacifc Workshop on Systems, APSys ’14, (New York, NY, USA), Association for Computing Machinery, 2014.

4. M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, K. Liao, and B. Parno, “Sok: Computer-aided cryptography.” Cryptology ePrint Archive, Report 2019/1393, 2019. https://eprint.iacr.org/2019/1393.

5. G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt, and P.-Y. Strub, EasyCrypt: A Tutorial, pp. 146– 166. Cham: Springer International Publishing, 2014.

6. J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire, V. Laporte, T. Oliveira, H. Pacheco, B. Schmidt, and P.-Y. Strub, “Jasmin: High-assurance and highspeed cryptography,” in Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17, (New York, NY, USA), p. 1807–1823, Association for Computing Machinery, 2017.

7. D. Unruh, “Post-quantum verifcation of FujisakiOkamoto,” in Advances in Cryptology – ASIACRYPT 2020 (S. Moriai and H. Wang, eds.), (Cham), pp. 321– 352, Springer International Publishing, 2020.