Có những giao thức hiện đại (hậu Thế chiến II) và nổi tiếng đã được chứng minh là an toàn (trong bất kỳ mô hình nào: dựa trên trò chơi, UC...) nhưng bằng chứng của chúng là sai và có thể dẫn đến các cuộc tấn công trong thế giới thực?

Lưu ý rằng:

• Tôi không thực sự lo lắng về các cuộc tấn công vào chính các giả định toán học (dường như là trọng tâm của chủ đề nàyvà không thể được coi là sai lầm trong bằng chứng: chúng "chỉ" là những giả định đáng tiếc). Nhưng tất nhiên, tôi muốn nghe về các giao thức được tuyên bố là an toàn ngay khi giả định X là đúng, trong khi thực tế chúng bị hỏng mặc dù X không bị hỏng.
• Theo "tấn công trong thế giới thực", tôi thích các cuộc tấn công phá vỡ các giao thức được sử dụng trong thực tế bởi người dùng cuối không chuyên, nhưng tôi cũng ổn với các giao thức nổi tiếng hầu hết được biết đến và sử dụng trong thế giới học thuật.

Lý tưởng nhất là tôi muốn tìm hiểu xem liệu "lỗi" trong bằng chứng có thực sự là một lỗi hay có khả năng được tạo ra có chủ đích (cửa sau của NSA...).

CHỈNH SỬA

Bạn cũng có thể nói chính xác, bất cứ khi nào có thể, nếu cuộc tấn công là do lỗi trong chính bằng chứng hoặc nếu mô hình bảo mật không được chọn phù hợp?

Có lẽ "Các cuộc tấn công phục hồi bản rõ chống lại SSH"đủ tư cách?

Tại thời điểm này, một số độc giả có thể thắc mắc làm cách nào chúng tôi có thể tấn công một biến thể của SSH đã được chứng minh là an toàn trong [1]. Lý do cơ bản là, trong khi các tác giả của [1] nhận ra rằng hoạt động giải mã trong SSH không phải là âatomicâ và có thể thất bại theo nhiều cách khác nhau, mô hình bảo mật của họ không phân biệt giữa các chế độ thất bại khác nhau khi báo cáo lỗi đối thủ. Hơn nữa, mô hình của họ không tính đến thực tế là lượng dữ liệu cần thiết để hoàn thành hoạt động giải mã được xác định bởi chính dữ liệu phải được giải mã (trường độ dài). Thật không may, có vẻ như việc triển khai mật mã trong thế giới thực phức tạp hơn các mô hình bảo mật hiện tại cho SSH handle.

Sau đó xem "Một loạt các bộ mật mã SSH" để theo dõi.

Có lẽ chúng ta có thể tính đến tiêu chuẩn quốc tế đầu tiên về chữ ký số, ISO/IEC 9796:1991, đã chỉ định chữ ký RSA và Rabin bằng cách sử dụng phần đệm dự phòng của thông báo để ký. An ninh đã được chứng minh bởi một sau đó cơ sở lý luận nhà nước-the-nghệ thuật, xuất bản năm thủ tục tố tụng của Eurocrypt 1990. Điều đó nêu rõ các thuộc tính của phần đệm chữ ký của tiêu chuẩn cần thiết để bảo mật mặc dù thuộc tính nhân của hàm RSA thô $x\mapsto x^d\bmod n$, Thích:

• Việc thay đổi hoặc bổ sung các yếu tố đại diện không dẫn đến các yếu tố khác.
• Tích tự nhiên của bất kỳ phần tử đại diện nào với bất kỳ hằng số nào khác 1 không phải là phần tử đại diện.

Những thuộc tính này là đúng. Nhưng chúng không tạo thành một bằng chứng bảo mật theo nghĩa hiện đại của điều đó. Họ chỉ chứng minh sự bất khả thi của một số các cuộc tấn công, chứ không phải là của không tí nào tấn công.

Và nó đã được tìm thấy¹ vào năm 1999, một phương pháp tính toán rẻ tiền thể hiện các loại thông báo lớn sao cho chữ ký của một thông báo được tìm thấy bằng cách gửi một thông báo khác (đôi khi là ba lần đầu tiên) cho chữ ký RSA; hoặc khóa bí mật được tìm thấy (một sự cố hoàn toàn) bằng cách gửi hai thông báo để lấy chữ ký của Rabin. Tiêu chuẩn đã được rút lại một năm sau đó.

Mặc dù tiêu chuẩn đó đang được sử dụng trong thực tế, cuộc tấn công chưa bao giờ thoái hóa thành khai thác theo như tôi biết, bởi vì các ứng dụng không cho phép lấy chữ ký của ngay cả một vài thông báo đáp ứng các ràng buộc chính xác.

Một ví dụ tương tự là ISO/IEC 9796-2:1997 chữ ký (nhưng nó đi kèm với yêu cầu bảo mật ít hơn). Nó bị phá vỡ bởi một cuộc tấn công: Jean-Sébastien Coron, David Naccache, Mehdi Tibouchi, Ralf-Philipp Weinmann's Phân tích mật mã thực tế của chữ ký ISO 9796-2 và EMV, Trong Tạp chí Mật mã học (2015), và trước đó trong kỷ yếu của Crypto 2009. Sơ đồ này được sử dụng rộng rãi trong Thẻ thông minh ngân hàng, với các tham số cho phép tính toán khả thi vài trăm nghìn tin nhắn sao cho, Nên một kẻ thù quản lý để có được chữ ký của tất cả trừ một người, điều này cho phép tìm thấy chữ ký của tin nhắn cuối cùng. Nhưng nó không thể suy thoái để khai thác thực tế.

¹ Tài liệu tham khảo về các cuộc tấn công là Don Coppersmith, Jean-Sébastien Coron, François Grieu, Shai Halevi, Charanjit Jutla, David Naccache, Julien P. Stern: Phân tích mật mã của ISO/IEC 9796-1, Trong Tạp chí Mật mã học (2007). Nó tập hợp lại các cuộc tấn công trước đó:

• Chiến lược giả mạo chữ ký mới áp dụng cho ISO 9796â1/2, ECASHâ¢, PKCS#1 V2.0, ANSI X9.31, SSL-3.02, đóng góp của chuyên gia ISO/IEC JTC1/SC27 (1999) đã chỉ ra đường tấn công, đường dẫn này hóa ra không áp dụng trực tiếp cho tiêu chuẩn do chi tiết một bit.
• ISO 9796-1 và chiến lược giả mạo mới (dự thảo làm việc) cải thiện chiến lược đó để xử lý toàn bộ tiêu chuẩn, nhưng yêu cầu nhiều thông báo được chọn.
• Một cuộc tấn công bằng tin nhắn được chọn vào lược đồ chữ ký ISO/IEC 9796-1 (trang trình bày) sử dụng một chiến lược khác hoạt động với ít thư và giúp việc tìm kiếm chúng không tốn kém.

Mới đây, WPA2 được phát hiện dễ bị tấn công Cài đặt lại khóa, mặc dù bắt tay 4 bước WPA2 đã được chứng minh là an toàn.

• Các cuộc tấn công cài đặt lại khóa: Buộc sử dụng lại Nonce trong WPA bởi Mathy Vanhoef và Frank Piessens

Từ trang web của họ

Bắt tay 4 bước đã được chứng minh về mặt toán học là an toàn. Làm thế nào là cuộc tấn công của bạn có thể?

Câu trả lời ngắn gọn là bằng chứng chính thức không đảm bảo rằng khóa chỉ được cài đặt một lần. Thay vào đó, nó chỉ đảm bảo rằng khóa đã đàm phán vẫn được giữ bí mật và các thông điệp bắt tay không thể bị giả mạo.

Câu trả lời dài hơn được đề cập trong phần giới thiệu bài báo nghiên cứu của chúng tôi: các cuộc tấn công của chúng tôi không vi phạm các thuộc tính bảo mật đã được chứng minh trong phân tích chính thức về bắt tay 4 bước. Đặc biệt, những bằng chứng này nêu rõ rằng khóa mã hóa đã thương lượng vẫn ở chế độ riêng tư và danh tính của cả máy khách và Điểm truy cập (AP) đã được xác nhận. Các cuộc tấn công của chúng tôi không làm rò rỉ khóa mã hóa. Ngoài ra, mặc dù các khung dữ liệu thông thường có thể bị giả mạo nếu sử dụng TKIP hoặc GCMP, nhưng kẻ tấn công không thể giả mạo thông báo bắt tay và do đó không thể mạo danh ứng dụng khách hoặc AP trong quá trình bắt tay. Do đó, các thuộc tính đã được chứng minh trong phân tích chính thức của bắt tay 4 bước vẫn đúng. Tuy nhiên, vấn đề là các bằng chứng không mô hình cài đặt khóa. Nói cách khác, các mô hình chính thức không xác định khi nào nên cài đặt khóa thương lượng. Trong thực tế, điều này có nghĩa là cùng một khóa có thể được cài đặt nhiều lần, do đó đặt lại các nonce và bộ đếm phát lại được sử dụng bởi giao thức mã hóa (ví dụ: bởi WPA-TKIP hoặc AES-CCMP).

Các Clipper Chip với mật mã cá cờ bạc

Đây có thể là kết quả treo thấp hơn bạn dự định, vì "Vector tấn công trong thế giới thực" có thể không hữu ích lắm để tấn công, vì chỉ có AT&T TSD-3600-E là thiết bị đã được biết là đã thực hiện điều này cho việc này và hầu hết các thiết bị khác dường như chỉ được mua bởi Bộ Tư pháp Hoa Kỳ. Điều này nói rằng, nó có thể giúp xây dựng nhận xét của @ Kevin về cách các kênh bên phổ biến hơn để trở thành vectơ tấn công cho các thuật toán đã nói, với lý do nổi tiếng nhất là nó không còn được sử dụng nữa.

Clipper Chip và Trường Truy cập Thực thi Pháp luật (LEAF)

LEAF được dự định là một cách cho phép chính phủ đọc thông tin cần thiết để có thể xác định khóa mã hóa và có thể giải mã tin nhắn khi họ có lệnh làm như vậy.

Điều này có 2 vấn đề lớn sau đó được phát hiện:

1.) Matt Blaze, vào năm 1994, phát hiện ra rằng có thể sử dụng thực tế là Hệ thống LEAF yêu cầu hàm băm 16 bit cho khóa mã hóa để xác minh rằng đó là một thông báo hợp lệ để mã hóa (Sao cho nó có thể được giải mã), có thể dùng vũ lực trong khoảng 30-50 phút tổng kiểm tra 16 bit mới cho một khóa mã hóa khác với khóa được sử dụng để mã hóa tin nhắn, bỏ qua bước "Có thể giải mã nếu cần" một cách hiệu quả .

2.) Yair Frankel và Moti Yung vào năm 1995 đã phát hiện ra rằng có thể sử dụng một Thiết bị có khả năng LEAF để tạo xác thực được đính kèm cho các tin nhắn được mã hóa trên thiết bị khác, do đó bỏ qua bước "Có thể giải mã nếu cần" trong thời gian thực.

Cuối cùng, những vấn đề này rất có thể dẫn đến việc không sử dụng phương pháp này, với chính phủ Hoa Kỳ là khách hàng lớn nhất đáng chú ý nhất của AT&T TSD-3600-E. Kết quả là tôi không biết có bao nhiêu trong số này đã thực sự được sử dụng, vì theo báo cáo, hầu hết các hộp đều chưa được mở. Điều này khiến chúng ta liên quan đến mật mã Skipjack thực tế.

cá ngừ vằn

Theo tôi hiểu, đây là mã hóa đã được Clipper Chip sử dụng sao cho, nếu không có LEAF hợp lệ đó từ các giá trị băm ở trên, sẽ được bảo đảm chống lại việc ai đó giải mã nội dung trong tin nhắn.

Điều này khó chứng minh rằng nó đã được chứng minh là an toàn, vì ban đầu, nó đã được phân loại, nhưng... Các nhà nghiên cứu hàn lâm đã được mời đến để đánh giá Skipjack và phát hiện ra rằng "Vì vậy, không có rủi ro đáng kể nào về việc SKIPJACK sẽ bị phá vỡ bằng cách tìm kiếm toàn diện trong 30-40 năm tới."

Ngày 25 tháng 6 năm 1998, khi Skipjack được giải mật, Eli Biham và Adi Shamir đã phát hiện ra điều đó khi Skipjack giảm xuống còn 16 thay vì 32 vòng, nó có thể bị phá vỡ với một vectơ tấn công được phát hiện vào thời điểm đó. Sau đó vào năm 1999, với Alex Biryukov, họ đã có thể kéo dài nó lên 31 trên 32 vòng.

Rõ ràng, kể từ năm 2009, sự đột phá hoàn toàn của tất cả 32 vòng vẫn chưa bị phá vỡ hoàn toàn, nhưng những điều này dường như chỉ ra rằng bằng chứng ban đầu có thể đã sai, vì có vẻ như 31 vòng đầu tiên của Skipjack 32 vòng chủ yếu dựa vào sự phân loại của thuật toán tại thời điểm đó.

Như @Kevin đã nói trong nhận xét của anh ấy cho câu hỏi trên, chủ yếu các kênh phụ sẽ là cách phá vỡ nó - và trong trường hợp này, Chip Clipper và chính giao thức LEAF của nó đã chứng tỏ là liên kết yếu hơn - phá vỡ giao thức sẽ có đã được sử dụng để giải mã các tin nhắn được mã hóa cơ bản khi được bảo hành.

Vào năm 2019, một lỗ hổng làm giả đã được phát hiện trong Zcash [xem đây].

Trước khi được khắc phục, kẻ tấn công có thể đã tạo Zcash giả mà không bị phát hiện!

Với mức vốn hóa thị trường hiện tại là 1,7 tỷ đô la, có vẻ như Zcash, ít nhất là ngày nay, được áp dụng rộng rãi ngoài một số người dùng chuyên gia. Lỗ hổng bắt nguồn từ một lỗ hổng mật mã tinh vi trong [BCTV14] bài báo mô tả cấu trúc zk-SNARK được sử dụng trong lần ra mắt ban đầu của Zcash. Lỗ hổng này rất tinh vi, đến nỗi nó đã trốn tránh nhiều năm phân tích của các chuyên gia mật mã. Ngoài ra, một số công trình tiếp theo của các nhà nghiên cứu nổi tiếng cũng mắc phải lỗi tương tự.

Điều quan trọng là [BCTV14] xây dựng không có bằng chứng bảo mật chuyên dụng, như đã lưu ý trong [Parno15], và chủ yếu dựa vào [PGHR13] bằng chứng bảo mật và sự giống nhau giữa hai sơ đồ. Nhóm Công ty Zcash đã cố gắng viết bằng chứng bảo mật trong [BGG17], nhưng nó không phát hiện ra lỗ hổng này. Zcash đã kể từ đó nâng cấp lên một hệ thống chứng minh mới [Groth16] có nhiều bằng chứng độc lập và phân tích tốt hơn đáng kể.

Đối với phần lớn các thuật toán mật mã hiện đại, không có bằng chứng toán học nghiêm ngặt nào chứng minh rằng chúng an toàn. Thông thường, khi một bằng chứng như vậy được xuất bản hoặc thảo luận, nó dựa trên giả định mà chỉ đơn thuần được tin là đúng. Nếu những giả định này không đúng, bằng chứng sẽ sụp đổ ngay cả khi không có sai lầm nào trong đó. Ví dụ: tính bảo mật của triple-DES dựa trên giả định rằng DES thông thường là an toàn (mặc dù với kích thước khóa không đủ để ngăn chặn các cuộc tấn công vũ phu). Nếu một lỗ hổng nghiêm trọng được phát hiện trong DES, thì nó cũng có khả năng ảnh hưởng đến bảo mật của 3DES.

Loại giả định thứ hai trong bằng chứng bảo mật xuất phát từ thực tế là họ đang cố gắng chứng minh một tiêu cực. Vì vậy, thay vì chứng minh rằng một thuật toán không thể bị phá vỡ, các nghiên cứu đánh giá khả năng bảo mật của thuật toán đó. các cuộc tấn công đã biết. Nếu một thuật toán đã được biết đến rộng rãi trong vài thập kỷ, thì nó được cho là "đã được chứng minh trong thực tế", trên thực tế, đây là một giả định rằng không có cuộc tấn công mới nào có thể được thiết kế để chống lại nó.

Hai điểm trên là bổ sung cho những sai lầm tầm thường trong logic của chứng minh.

Vì vậy, tùy thuộc vào mức độ bằng chứng mà bạn cho là đầy đủ, bạn có thể nói rằng không ai trong số các giao thức nổi tiếng trong thế giới thực đã từng được chứng minh là an toàn hoặc những giao thức bị bẻ khóa sau này đã được "chứng minh" là an toàn tại một số điểm (nếu không thì chúng đã không được sử dụng), nhưng bằng chứng không có giá trị.