เหตุใดบทพิสูจน์อย่างไม่เป็นทางการจึงไม่เพียงพอ

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

Needham-Schroeder (1978) ได้รับการออกแบบเพื่อการยืนยันตัวตนซึ่งกันและกัน ในปี 1995 Gavin Lowe ค้นพบการโจมตีแบบคนกลางโดยใช้การตรวจสอบอัตโนมัติ ซึ่งเกิดขึ้น 17 ปีหลังการเผยแพร่ การพิสูจน์อย่างไม่เป็นทางการพลาดการโจมตีซ้ำที่ซับซ้อนจุดหนึ่ง

IEEE อนุมัติ WEP ในปี 1997 พร้อมคำกล่าวอ้างด้านความปลอดภัยอย่างไม่เป็นทางการ ภายในปี 2001 นักวิจัยพบการใช้กระแสกุญแจ RC4 ซ้ำ การชนกันของ IV และการขาดความครบถ้วนถูกต้อง ซึ่งทำให้ WEP ถูกทำลายได้ภายในไม่กี่นาที การให้เหตุผลอย่างไม่เป็นทางการพลาดปัญหาเหล่านี้ทั้งหมด

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

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

เชิงสัญลักษณ์ (Dolev-Yao): มองการเข้ารหัสเป็นกล่องดำที่สมบูรณ์แบบ และมุ่งเน้นตรรกะของโพรโทคอล เชิงคำนวณ: ใช้เกมความปลอดภัยเชิงความน่าจะเป็นจริง ซึ่งใกล้เคียงการรับรองในโลกจริงมากกว่า ทั้งสองแบบช่วยตรวจจับข้อผิดพลาดจริงได้

POODLE (2014) ใช้ออราเคิลแพดดิ้งใน CBC ของ SSL 3.0 ช่องโหว่นี้เป็นข้อบกพร่องด้านการออกแบบระดับโพรโทคอล ไม่ใช่ข้อผิดพลาดในการนำไปใช้งาน การวิเคราะห์ข้อกำหนด SSL 3.0 อย่างเป็นทางการน่าจะตรวจพบออราเคิลนี้ก่อนการนำไปใช้งาน

TLS 1.3 (RFC 8446) ได้รับการออกแบบควบคู่กับการวิเคราะห์อย่างเป็นทางการโดยใช้ ProVerif และ miTLS มีการปรับปรุงข้อกำหนดตามผลการตรวจสอบอย่างเป็นทางการ นับเป็นหมุดหมายสำคัญที่องค์กรกำหนดมาตรฐานนำวิธีการอย่างเป็นทางการมาใช้

เครื่องมืออย่างเป็นทางการตรวจสอบแบบจำลองโพรโทคอล ไม่ใช่การนำไปใช้งาน โพรโทคอลที่ผ่านการตรวจสอบอย่างเป็นทางการจึงยังอาจมีการนำไปใช้งานที่ไม่ปลอดภัยได้ F* / HACL* ขยายการตรวจสอบไปยังโค้ดการเข้ารหัสด้วย

การตรวจสอบอย่างเป็นทางการมีต้นทุนสูง การสร้างแบบจำลองโพรโทคอลใช้เวลาหลายสัปดาห์และต้องอาศัยความเชี่ยวชาญเฉพาะทาง แต่สำหรับเป้าหมายที่มีมูลค่าสูง เช่น TLS, SSH และ Signal ต้นทุนนี้ถือว่าคุ้มค่า เพราะข้อบกพร่องของโพรโทคอลเพียงจุดเดียวอาจส่งผลกระทบต่อผู้ใช้หลายพันล้านคน

อะไรทำให้การค้นพบการโจมตี Needham-Schroeder ของ Lowe ในปี 1995 มีความสำคัญ

การพิสูจน์อย่างไม่เป็นทางการล้มเหลวเพราะการให้เหตุผลโดยมนุษย์มองข้ามปฏิสัมพันธ์ระหว่างเซสชันที่ทำงานพร้อมกันและกลยุทธ์ของผู้โจมตี Needham-Schroeder, WEP และ POODLE ล้วนมีข้อโต้แย้งด้านความปลอดภัยอย่างไม่เป็นทางการ TLS 1.3 รวมการวิเคราะห์อย่างเป็นทางการไว้ในระหว่างการออกแบบ เครื่องมืออย่างเป็นทางการช่วยตรวจจับข้อผิดพลาดระดับโพรโทคอลก่อนการนำไปใช้งาน