แบบจำลองผู้โจมตี Dolev-Yao และการเข้ารหัสเชิงสัญลักษณ์

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

ผู้โจมตีตามแบบจำลอง Dolev-Yao สามารถ ดักจับข้อความใด ๆ จัดเก็บข้อความ เล่นซ้ำข้อความเก่า และ ปลอมแปลงข้อความใหม่จากองค์ประกอบที่ทราบ แต่ไม่สามารถทำลายส่วนประกอบพื้นฐานของการเข้ารหัสได้

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

ข้อความถูกจำลองเป็นพจน์ เช่น enc(k, m), sig(sk, m), hash(m), pair(a, b) ผู้โจมตีรู้จักพจน์บางรายการ และอนุมานพจน์ใหม่โดยใช้กฎที่กำหนดไว้ (กฎการอนุมาน)

ความรู้ของผู้โจมตีปิดภายใต้การอนุมาน กล่าวคือ หากผู้โจมตีรู้จัก enc(k,m) และ k ก็สามารถอนุมาน m ได้ หากรู้จัก pair(a,b) ก็สามารถอนุมาน a และ b ได้ การปิดของความรู้เริ่มต้น = ทุกสิ่งที่ผู้โจมตีสามารถเรียนรู้ได้

ความปลอดภัยของโพรโทคอลระบุว่า "ความรู้ของผู้โจมตีจะไม่มีทางมีความลับ s อยู่ในสถานะใด ๆ ที่เข้าถึงได้" การรักษาความลับ = การเข้าถึงได้ การพิสูจน์ตัวตน = การไม่มีรูปแบบร่องรอยที่ไม่พึงประสงค์บางอย่าง

โพรโทคอลสองฝ่าย: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B} ในพีชคณิตพจน์: Alice ส่ง enc(pubkey_B, pair(Na, A)) เราตรวจสอบว่าหลังจากการทำงานเสร็จสิ้น มีเพียง B เท่านั้นที่รู้จัก Na

แคลคูลัสไพประยุกต์ (Abadi และ Fournet, 2001) เป็นพีชคณิตกระบวนการสำหรับสร้างแบบจำลองโพรโทคอล กระบวนการสื่อสารกันผ่านช่องสัญญาณ และผู้โจมตีควบคุมช่องสัญญาณสาธารณะ ProVerif และ Tamarin ใช้รูปแบบเชิงรูปนัยนี้

โพรโทคอลที่ปลอดภัยในแบบจำลอง Dolev-Yao อาจยังไม่ปลอดภัยเชิงคำนวณ หากการนำองค์ประกอบการเข้ารหัสไปใช้งานมีจุดอ่อน ทฤษฎีความถูกต้องเชิงคำนวณ (Cortier และคณะ) เชื่อมช่องว่างนี้สำหรับองค์ประกอบพื้นฐานบางประเภทโดยเฉพาะ

Dolev-Yao ไม่สามารถสร้างแบบจำลองสิ่งต่อไปนี้ได้: คุณสมบัติเชิงพีชคณิต (เช่น การสลับที่ของ XOR) การโจมตีช่องทางข้างเคียง ข้อบกพร่องในการนำไปใช้งาน หรือความล้มเหลวแบบมีความน่าจะเป็น ส่วนขยายอย่างแบบจำลองทฤษฎีสมการสามารถจัดการคุณสมบัติเชิงพีชคณิตบางส่วนได้

ความสามารถใดที่ผู้โจมตีแบบ Dolev-Yao ไม่มี (NOT)

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