ความปลอดภัยที่พิสูจน์ได้และการลดทอน

ความปลอดภัยที่พิสูจน์ได้แสดงให้เห็นว่าการทำลายระบบเข้ารหัสเป็นเรื่องยากพอๆ กับการแก้ปัญหาที่เชื่อว่าไม่สามารถแก้ไขได้ โดยการลดทอนอย่างชัดเจนจากปัญหาที่ถือว่ายากไปสู่การโจมตีใดๆ บนระบบนั้น

Definition

การลดทอนความปลอดภัยคือการพิสูจน์ที่แปลงคู่ต่อสู้ที่มีประสิทธิภาพใดๆ ที่ทำลายระบบเข้ารหัสให้เป็นอัลกอริทึมที่มีประสิทธิภาพที่แก้ปัญหาที่ถือว่ายาก ซึ่งแสดงให้เห็นว่าระบบนั้นปลอดภัยเว้นแต่ปัญหานั้นจะง่าย

Scope

หัวข้อนี้ครอบคลุมระเบียบวิธีที่อิงการลดทอนของการพิสูจน์ทางคริปโตกราฟี: โครงสร้างของการลดทอนความปลอดภัย, ความกระชับและความปลอดภัยที่เป็นรูปธรรม, รูปแบบการพิสูจน์ที่อิงเกมและการอิงการจำลอง, แบบจำลองออราเคิลสุ่มและแบบจำลองมาตรฐาน, และข้อจำกัดและข้อวิพากษ์วิจารณ์ของแนวทางนี้ นอกจากนี้ยังกล่าวถึงวิธีการระบุและโต้แย้งการรับประกันความปลอดภัย โดยไม่รวมถึงข้อสมมติฐานความยากเฉพาะเจาะจง และคำจำกัดความและแบบจำลองของคู่ต่อสู้ ซึ่งจะกล่าวถึงในหัวข้อที่เกี่ยวข้อง

Core questions

• การลดทอนแปลงการโจมตีบนระบบให้เป็นการแก้ปัญหาที่ยากได้อย่างไร?
• ความแตกต่างระหว่างการพิสูจน์ที่อิงเกมและการพิสูจน์ที่อิงการจำลองคืออะไร?
• 'ความกระชับ' ของการลดทอนมีความหมายอย่างไรต่อพารามิเตอร์ความปลอดภัยในโลกแห่งความเป็นจริง?
• แบบจำลองออราเคิลสุ่มและแบบจำลองมาตรฐานคืออะไร และเหตุใดแบบจำลองแรกจึงเป็นที่ถกเถียง?
• ข้อจำกัดและข้อผิดพลาดทั่วไปของการโต้แย้งความปลอดภัยที่พิสูจน์ได้คืออะไร?

Key concepts

• การลดทอนความปลอดภัย
• การพิสูจน์ที่อิงเกม
• การพิสูจน์ที่อิงการจำลอง
• การลดทอนแบบกระชับเทียบกับแบบหลวม
• ความปลอดภัยที่เป็นรูปธรรม
• แบบจำลองออราเคิลสุ่ม
• แบบจำลองมาตรฐาน
• ความได้เปรียบที่ไม่น้อยเกินไป
• ข้อสมมติฐานความยาก

Key theories

ระเบียบวิธีพิสูจน์แบบลดทอน

ในการพิสูจน์ว่าระบบมีความปลอดภัย จะสมมติว่ามีคู่ต่อสู้ที่ทำลายระบบนั้น และสร้างอัลกอริทึมที่แก้ปัญหาพื้นฐานที่ยาก โดยใช้คู่ต่อสู้เป็นรูทีนย่อย — ดังนั้นการโจมตีที่ประสบความสำเร็จจะขัดแย้งกับข้อสมมติฐานความยาก

แบบจำลองออราเคิลสุ่ม

ระบบที่มีประสิทธิภาพหลายระบบได้รับการพิสูจน์ว่าปลอดภัยโดยการทำให้ฟังก์ชันแฮชเป็นออราเคิลสุ่มอย่างแท้จริง แบบจำลองนี้ช่วยให้สามารถพิสูจน์การสร้างที่ใช้งานได้จริง แต่เป็นเชิงการคาดคะเน เนื่องจากไม่มีฟังก์ชันจริงใดเป็นออราเคิลสุ่ม

Mechanisms

ในการลดทอน ผู้พิสูจน์จะสมมติว่ามีคู่ต่อสู้สมมติที่ทำลายระบบด้วยความได้เปรียบที่ไม่น้อยเกินไป และสร้างตัวห่อหุ้มที่ฝังอินสแตนซ์ของปัญหาที่ยากลงในมุมมองของคู่ต่อสู้ เรียกใช้คู่ต่อสู้ และใช้ผลลัพธ์ของมันเพื่อแก้ปัญหา การพิสูจน์ที่อิงเกมจะดำเนินการผ่านลำดับของเกมที่ไม่สามารถแยกแยะได้จากระบบจริงไปสู่ระบบที่คู่ต่อสู้ไม่สามารถชนะได้อย่างชัดเจน ความกระชับของการลดทอน — ความได้เปรียบและเวลาทำงานที่สูญเสียไป — เป็นตัวกำหนดขนาดคีย์ที่จำเป็นสำหรับระดับความปลอดภัยเป้าหมาย

Clinical relevance

ความปลอดภัยที่พิสูจน์ได้เป็นมาตรฐานที่ระบบเข้ารหัสได้รับความไว้วางใจและการกำหนดมาตรฐาน: AES, SHA-3 ของ NIST และกระบวนการหลังควอนตัมให้ความสำคัญกับการพิสูจน์ความปลอดภัยอย่างมาก และโปรโตคอลเช่น TLS 1.3 ก็มาพร้อมกับการวิเคราะห์แบบลดทอนและที่ตรวจสอบด้วยเครื่องจักร การทำความเข้าใจการลดทอนช่วยให้ผู้ปฏิบัติงานสามารถตัดสินได้ว่าการอ้างสิทธิ์ความปลอดภัยรับประกันอะไรและไม่รับประกันอะไร และเลือกพารามิเตอร์ที่คำนึงถึงความกระชับของการลดทอน

Evidence & guidelines

แนวปฏิบัติสมัยใหม่นิยมการพิสูจน์ในแบบจำลองมาตรฐานเมื่อทำได้ และถือว่าการพิสูจน์แบบออราเคิลสุ่มเป็นหลักฐานเชิงการคาดคะเนที่แข็งแกร่งมากกว่าการรับประกันที่สมบูรณ์ กรอบงานที่ใช้เครื่องมือช่วย (EasyCrypt, CryptoVerif) ให้การพิสูจน์ที่ตรวจสอบด้วยเครื่องจักร การวิเคราะห์ความปลอดภัยที่เป็นรูปธรรม (ที่แน่นอน) ซึ่งวัดปริมาณความได้เปรียบของคู่ต่อสู้เป็นฟังก์ชันของทรัพยากร เป็นที่นิยมมากกว่าข้อความเชิงอสมการอย่างเดียวสำหรับการตั้งค่าพารามิเตอร์จริง

History

ระเบียบวิธีลดทอนเกิดขึ้นพร้อมกับการปฏิวัติเชิงนิยามในช่วงต้นทศวรรษ 1980 และได้รับการจัดระบบตลอดทศวรรษ 1990 Bellare และ Rogaway ได้นำเสนอแบบจำลองออราเคิลสุ่ม (1993) เพื่อพิสูจน์ว่าระบบที่ใช้งานได้จริงมีความปลอดภัย และต่อมาได้มีการวิเคราะห์ 'ความปลอดภัยที่เป็นรูปธรรม' เพื่อวัดปริมาณการรับประกัน ผลลัพธ์ของ Canetti, Goldreich และ Halevi ในปี 1998 ที่แสดงให้เห็นว่าระบบที่ปลอดภัยในแบบจำลองออราเคิลสุ่มแต่ไม่ปลอดภัยเมื่อนำไปใช้งานจริง ได้ทำให้การถกเถียงเกี่ยวกับแบบจำลองในอุดมคติมีความชัดเจนยิ่งขึ้น

Key figures

• Mihir Bellare
• Phillip Rogaway
• Oded Goldreich
• Shafi Goldwasser
• Silvio Micali

Seminal works

• bellare1993
• katz2020
• goldreich2001

Frequently asked questions

การพิสูจน์ความปลอดภัยหมายความว่าระบบจะไม่ถูกทำลายเลยใช่หรือไม่?

ไม่ การพิสูจน์แสดงให้เห็นว่าการทำลายระบบหมายถึงการแก้ปัญหาที่ถือว่ายากภายในแบบจำลองที่ระบุ หากข้อสมมติฐานล้มเหลว แบบจำลองไม่สมจริง หรือการนำไปใช้งานเบี่ยงเบนไปจากระบบที่วิเคราะห์ การโจมตียังคงเป็นไปได้ การพิสูจน์ช่วยลดความเสี่ยง แต่ไม่กำจัดความเสี่ยง

เหตุใดแบบจำลองออราเคิลสุ่มจึงเป็นที่ถกเถียง?

มันจำลองฟังก์ชันแฮชเป็นฟังก์ชันสุ่มที่สมบูรณ์แบบ ซึ่งไม่มีฟังก์ชันที่เป็นรูปธรรมใดเป็นเช่นนั้นอย่างแท้จริง การพิสูจน์ในแบบจำลองนี้เป็นหลักฐานที่แข็งแกร่งและช่วยให้ระบบมีประสิทธิภาพ แต่มีระบบ (ที่สร้างขึ้นมา) ที่ปลอดภัยในแบบจำลองแต่ไม่ปลอดภัยเมื่อออราเคิลถูกแทนที่ด้วยแฮชจริงใดๆ ดังนั้นการพิสูจน์ดังกล่าวจึงเป็นเชิงการคาดคะเน