โพรโทคอล Needham-Schroeder และการโจมตี

โพรโทคอล Needham-Schroeder (1978) เป็นหนึ่งในความพยายามเชิงรูปแบบยุคแรก ๆ ในการออกแบบโพรโทคอลการยืนยันตัวตนด้วยการเข้ารหัสโดยใช้บุคคลที่สามที่เชื่อถือได้ (TTP) เป้าหมายคือให้สองฝ่าย ได้แก่ Alice และ Bob ยืนยันตัวตนซึ่งกันและกันและสร้างกุญแจเซสชันร่วมกัน โดยใช้เซิร์ฟเวอร์ยืนยันตัวตน (AS) ที่เชื่อถือได้ ซึ่งมีกุญแจระยะยาวร่วมกับผู้เข้าร่วมแต่ละฝ่าย โพรโทคอลนี้เกิดขึ้นก่อนโครงสร้างพื้นฐานกุญแจสาธารณะ แต่ได้นำแนวคิดต่าง ๆ เช่น ค่าที่ใช้ครั้งเดียวเพื่อรับรองความใหม่ และการแจกจ่ายกุญแจผ่านเซิร์ฟเวอร์ที่เชื่อถือได้ ซึ่งยังคงเป็นแกนสำคัญของโพรโทคอลสมัยใหม่อย่าง Kerberos การทำความเข้าใจ NS และข้อบกพร่องของโพรโทคอลนี้มีอิทธิพลต่อวงการวิเคราะห์โพรโทคอลทั้งหมด

โพรโทคอลกุญแจสมมาตร NS ดำเนินการเป็นห้าขั้นตอน (1) Alice ส่ง {A, B, Na} ไปยัง AS เพื่อขอกุญแจเซสชันสำหรับสื่อสารกับ Bob (2) AS ตอบ Alice ด้วย {Na, B, Kab, {Kab, A}_Kb}_Ka ซึ่งประกอบด้วยกุญแจเซสชัน Kab และตั๋วสำหรับ Bob โดยทั้งหมดเข้ารหัสด้วยกุญแจระยะยาว Ka ของ Alice (3) Alice ส่งต่อ ตั๋ว {Kab, A}_Kb ให้ Bob (4) Bob ถอดรหัสตั๋ว ดึง Kab ออกมา และส่ง {Nb}_Kab ให้ Alice เพื่อเป็นคำท้าทาย (5) Alice ตอบกลับด้วย {Nb-1}_Kab เพื่อพิสูจน์ว่าครอบครอง Kab ค่า Nb ช่วยป้องกันการเล่นซ้ำของขั้นตอนที่ 4 โพรโทคอลนี้มีการโจมตีแบบเล่นซ้ำที่ Denning และ Sacco ค้นพบในปี 1981

Denning และ Sacco (1981) พบข้อบกพร่องว่า การตอบกลับของ AS ในขั้นตอนที่ 2 ไม่ใช่ข้อมูลใหม่ เนื่องจากไม่มีการประทับเวลาหรือค่าที่ใช้ครั้งเดียวจากเซิร์ฟเวอร์ ผู้โจมตีชื่อ Mallory ซึ่งเคยดักจับกุญแจเซสชันเก่า Kab ไว้ก่อนหน้านี้ (โดยเจาะเซสชันในอดีต) สามารถส่งตั๋วเก่า {Kab, A}_Kb ซ้ำให้ Bob ได้ทุกเมื่อในอนาคต เมื่อ Bob ได้รับสิ่งที่ดูเหมือนเป็นตั๋วที่ถูกต้องจาก Alice เขาจะใช้กุญแจ Kab ที่ถูกเจาะสำหรับเซสชันนั้น วิธีแก้ของ Denning และ Sacco คือเพิ่มการประทับเวลาในการตอบกลับของ AS และในตั๋ว แนวทางนี้ถูกนำไปใช้ใน Kerberos โดยฝังการประทับเวลาไว้ในตั๋วเพื่อจำกัดช่วงเวลาที่ตั๋วใช้งานได้

โพรโทคอลกุญแจสาธารณะ NS (ซึ่งพัฒนาขึ้นในปี 1978 เช่นกัน) ออกแบบมาสำหรับการยืนยันตัวตนซึ่งกันและกันระหว่างสองฝ่ายโดยใช้การเข้ารหัสด้วยกุญแจสาธารณะ (1) Alice ส่ง {Na, A}_PKb ให้ Bob โดยค่า Na ถูกเข้ารหัสด้วยกุญแจสาธารณะของ Bob (2) Bob ตอบกลับด้วย {Na, Nb}_PKa ซึ่งเป็นค่าทั้งสองที่เข้ารหัสด้วยกุญแจสาธารณะของ Alice (3) Alice ตอบกลับด้วย {Nb}_PKb โดยส่งค่า Nb ของ Bob กลับไปหลังเข้ารหัสด้วยกุญแจสาธารณะของเขา หลังจากแลกเปลี่ยนข้อความนี้ ทั้งสองฝ่ายจะมีค่าทั้ง Na และ Nb และสามารถสร้างกุญแจเซสชันได้ โพรโทคอลนี้ดูปลอดภัยมาเป็นเวลา 17 ปี จนกระทั่งเกิดการโจมตีของ Lowe ในปี 1995

Gavin Lowe (1995) พบข้อบกพร่องร้ายแรงโดยใช้แบบจำลองตรวจสอบความล้มเหลวในการให้เหตุผลเชิงองค์ประกอบ (FDR) Mallory สามารถปลอมตัวเป็น Bob ต่อ Alice ขณะส่งต่อข้อความไปยัง Bob ที่ซื่อสัตย์ ขั้นตอนที่ 1: Alice ส่ง {Na, A}_PKm ให้ Mallory โดยคิดว่ากำลังสื่อสารกับ Bob Mallory ส่งต่อ {Na, A}_PKb ให้ Bob ขั้นตอนที่ 2: Bob ตอบกลับด้วย {Na, Nb}_PKa ซึ่ง Mallory ถอดรหัสแล้วเข้ารหัสใหม่เพื่อส่งให้ Alice เป็น {Na, Nb}_PKa Alice ถอดรหัสและดึง Nb ออกมา ขั้นตอนที่ 3: Alice ส่ง {Nb}_PKm โดยคิดว่าข้อความนี้จะไปถึง Bob Mallory ถอดรหัสแล้วส่งต่อ {Nb}_PKb ให้ Bob Bob เชื่อว่าตนยืนยันตัวตนกับ Alice สำเร็จแล้ว แต่จริง ๆ Alice กำลังยืนยันตัวตนกับ Mallory วิธีแก้คือ ในขั้นตอนที่ 2 Bob ต้องใส่ข้อมูลระบุตัวตนของตนเองด้วย โดยส่ง {Na, Nb, B}_PKa

วิธีแก้ไขของ Lowe สำหรับโพรโทคอล NSPK นั้นเรียบง่ายแต่ลึกซึ้ง: การตอบกลับของ Bob ในขั้นตอนที่ 2 ต้องมีตัวตนของ Bob คือ B อยู่ด้วย ทำให้เป็น {Na, Nb, B}_PKa เมื่อ Alice ได้รับการตอบกลับ เธอจะตรวจสอบว่าตัวตน B ที่ระบุไว้นั้นตรงกับฝ่ายที่เธอตั้งใจจะติดต่อหรือไม่ Mallory ไม่สามารถนำการตอบกลับของตนมาแทนที่ได้ เพราะ Mallory ต้องมีกุญแจส่วนตัวของ Alice จึงจะสร้าง {Na, Nb, M}_PKa ที่ถูกต้องและผ่านการตรวจสอบของ Alice ได้ แนวคิดนี้สรุปเป็นหลักการ Needham-Abadi: ข้อความสำหรับการพิสูจน์ตัวตนต้องผูกตัวตนของผู้ส่งไว้อย่างชัดเจน ไม่ใช่อาศัยบริบทเพียงอย่างเดียวในการระบุฝ่าย

การค้นพบข้อบกพร่องของ NSPK โดย Lowe ได้รับความช่วยเหลือจากเครื่องตรวจสอบแบบจำลอง FDR (การปรับละเอียดด้านความล้มเหลวและความเบี่ยงเบน) ซึ่งสำรวจการทำงานของโพรโทคอลที่เป็นไปได้ทั้งหมดอย่างครบถ้วน รวมถึงการแทรกแซงของผู้โจมตี เรื่องนี้กระตุ้นให้เกิดการพัฒนาเครื่องมือวิเคราะห์โพรโทคอลอย่างเป็นทางการ: โพรเวอริฟ (อิงแคลคูลัสไพประยุกต์) สามารถพิสูจน์หรือหักล้างคุณสมบัติด้านการพิสูจน์ตัวตนและความลับในเซสชันจำนวนไม่จำกัดได้ ทามารินพรอเวอร์ใช้การเขียนทับแบบหลายเซตและรองรับโพรโทคอลที่ซับซ้อน เช่น TLS 1.3 และซิกแนล AVISPA และไซเธอร์ก็เป็นเครื่องมืออื่นเช่นกัน การออกแบบโพรโทคอลสมัยใหม่ (TLS 1.3, ซิกแนล, นอยส์) ผ่านการตรวจสอบอย่างเป็นทางการก่อนนำไปใช้งาน ซึ่งเป็นมรดกโดยตรงจากเหตุการณ์ NS/Lowe

การโจมตี NS ทำให้เห็นความแตกต่างระหว่างเป้าหมายของการพิสูจน์ตัวตนอย่างชัดเจน การพิสูจน์ตัวตนของฝ่าย: การพิสูจน์ว่าฝ่ายหนึ่งกำลังทำงานอยู่และเข้าร่วมโพรโทคอลในขณะนั้น (ความใหม่มีความสำคัญ) การพิสูจน์แหล่งที่มาของข้อมูล: การพิสูจน์ว่าข้อความหนึ่ง ๆ ถูกสร้างโดยฝ่ายหนึ่ง ๆ (อาจไม่ได้หมายความว่าฝ่ายนั้นยังทำงานอยู่) ข้อกำหนดของโพรโทคอลสมัยใหม่จะระบุเป้าหมายอย่างแม่นยำ เช่น "Alice ได้รับการพิสูจน์ตัวตนกับ Bob ว่าเป็นผู้เริ่มต้นของเซสชันนี้" เป้าหมายที่คลุมเครือนำไปสู่ข้อกำหนดกำกวม ซึ่งอาจผ่านการทบทวนแบบไม่เป็นทางการแต่ไม่ผ่านการวิเคราะห์อย่างเป็นทางการ

การโจมตีที่เกี่ยวข้องกับ NS อีกประเภทหนึ่งคือการโจมตีแบบสะท้อนกลับ: Mallory นำข้อความจาก Alice ส่งกลับไปยัง Alice หากโพรโทคอลมีความสมมาตร (ทั้งสองฝ่ายใช้กุญแจและรูปแบบข้อความเดียวกัน) Alice อาจยอมรับคำท้าทายของตนเองว่าเป็นการตอบกลับที่ถูกต้องจาก Bob การป้องกันคือใช้ทิศทางกุญแจที่แตกต่างกัน (แยกกุญแจเข้ารหัสและถอดรหัสสำหรับแต่ละทิศทาง) หรือใส่ตัวบ่งชี้บทบาทไว้ในข้อความ (ผู้เข้ารหัสใส่ "ฉันเป็นผู้เริ่มต้น" ไว้ในข้อความ) โพรโทคอลสมัยใหม่อย่าง TLS ใส่สตริงป้ายกำกับเฉพาะบทบาทไว้ในกุญแจที่ได้จาก HKDF (ใช้ "c e traffic" สำหรับไคลเอนต์ และ "s hs traffic" สำหรับเซิร์ฟเวอร์) เพื่อป้องกันการโจมตีแบบสะท้อนกลับ

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

โพรโทคอล Needham-Schroeder มีอิทธิพลโดยตรงต่อการออกแบบเคอร์เบอรอส (ใช้การประทับเวลาเพื่อป้องกันการเล่นซ้ำ โดยยืมแนวคิดจากวิธีแก้ของ Denning-Sacco) TLS (MAC ของบันทึกการแลกเปลี่ยนในข้อความ Finished ป้องกันการสอดแทรกและการสะท้อนกลับ) โพรโทคอลซิกแนล (การผูกเซสชันผ่านสถานะของกลไกเลื่อน) และกรอบงานโพรโทคอลนอยส์ (การผูกตัวตนในรูปแบบการจับมือ) การโจมตี NS ทำให้เห็นชัดว่าการให้เหตุผลด้านความปลอดภัยแบบไม่เป็นทางการไม่เพียงพอ ทุกโพรโทคอลต้องได้รับการวิเคราะห์โดยพิจารณาผู้โจมตีเชิงรุกที่ควบคุมเครือข่ายและสามารถเล่นซ้ำ เรียงลำดับใหม่ และแก้ไขข้อความได้ แบบจำลองผู้โจมตีนี้ (Dolev-Yao) เป็นมาตรฐานในการตรวจสอบโพรโทคอลอย่างเป็นทางการในปัจจุบัน

Lowe เสนอการเปลี่ยนแปลงง่าย ๆ ใดเพื่อแก้ไขช่องโหว่ของโพรโทคอลกุญแจสาธารณะ NS

โพรโทคอล Needham-Schroeder แบบสมมาตร (1978) นำเสนอการแจกจ่ายกุญแจเซสชันโดยอาศัย TTP การโจมตีของ Denning-Sacco (1981) พบช่องโหว่จากการเล่นซ้ำ ซึ่งแก้ไขด้วยการประทับเวลาในเคอร์เบอรอส โพรโทคอลกุญแจสาธารณะ NSPK ตกเป็นเป้าหมายของการโจมตี MITM ซึ่ง Lowe ค้นพบในปี 1995 ผ่านการตรวจสอบแบบจำลอง และแก้ไขด้วยการใส่ตัวตนของผู้ส่งไว้ในข้อความ การโจมตีเหล่านี้ทำให้การตรวจสอบอย่างเป็นทางการ (โพรเวอริฟ, ทามารินพรอเวอร์) กลายเป็นสิ่งจำเป็นสำหรับการออกแบบโพรโทคอล บทเรียนสำคัญคือ ข้อความต้องผูกตัวตนของผู้ส่ง เซสชันต้องแยกออกจากกัน การโจมตีแบบสะท้อนกลับป้องกันได้ด้วยการสร้างกุญแจแยกตามทิศทาง และการโจมตีแบบสอดแทรกป้องกันได้ด้วย MAC ของบันทึกการแลกเปลี่ยน