ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ
ระบุและตรวจสอบคุณสมบัติของแฮนด์เชก TLS ด้วย ProVerif
ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ เป็นบทเรียน Cryptology Academy ฟรีบน CoddyKit นี่คือบทเรียนที่ 3 จากทั้งหมด 4 บทเรียน คุณสามารถอ่านบทเรียนทั้งหมดด้านล่างฟรี — จากนั้นลองปฏิบัติด้วยตัวคุณเองในเบราว์เซอร์พร้อมตัวแก้ไขโค้ดในตัวและติวเตอร์ AI ตลอด 24/7 บทเรียนนี้เป็นส่วนหนึ่งของเส้นทางการเรียน Cryptology Academy และความก้าวหน้าของคุณจะซิงค์ข้ามเว็บและแอป CoddyKit คอร์ส Cryptology Academy มีบทเรียนทั้งหมด 4 บทเรียน
ProVerif คืออะไร
ProVerif (Bruno Blanchet, 2001) เป็นเครื่องมือตรวจสอบโพรโทคอลการเข้ารหัสแบบอัตโนมัติ เครื่องมือนี้รับโพรโทคอลที่อธิบายด้วยแคลคูลัสไพประยุกต์ และตัดสินคุณสมบัติด้านการรักษาความลับและการพิสูจน์ตัวตนโดยอัตโนมัติ
ProVerif ทำงานอย่างไร
ProVerif แปลงโพรโทคอลเป็นอนุประโยคฮอร์น และใช้อัลกอริทึมแบบรีโซลูชันเพื่ออนุมานสิ่งที่ผู้โจมตีสามารถเรียนรู้ได้ หากข้อเท็จจริงด้านการรักษาความลับสามารถอนุมานได้ โพรโทคอลก็ถูกเจาะ หากอนุมานไม่ได้ โพรโทคอลก็ได้รับการพิสูจน์ว่าปลอดภัย
ภาษาข้อมูลเข้าของ ProVerif
โพรโทคอลอธิบายแบบเชิงประกาศ โดยประกาศช่องสัญญาณ ชนิดข้อมูล ฟังก์ชัน (enc, dec, sign, verify) สมการ (dec(enc(m,k),k)=m) และกระบวนการที่สื่อสารกันผ่านช่องสัญญาณ
การประกาศองค์ประกอบพื้นฐานทางการเข้ารหัส
ตัวอย่างการประกาศของ ProVerif:
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.การเขียนกระบวนการโพรโทคอลอย่างง่าย
จำลอง Alice และ Bob เป็นกระบวนการแบบขนาน:
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))การระบุข้อคำถามด้านความปลอดภัย
ProVerif ตรวจสอบข้อคำถาม เช่น:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).การตีความผลลัพธ์จาก ProVerif
ProVerif แสดงผลลัพธ์เป็น "RESULT ... เป็นจริง" (พิสูจน์ว่าปลอดภัย) หรือ "RESULT ... เป็นเท็จ" และพิมพ์ร่องรอยการโจมตีที่เป็นตัวอย่างโต้แย้ง ซึ่งแสดงข้อความของผู้โจมตี ร่องรอยนี้แสดงให้เห็นอย่างชัดเจนว่าการโจมตีทำงานอย่างไร
การตรวจสอบ TLS 1.3 ด้วย ProVerif
Bhargavan และคณะ (2016) ใช้ ProVerif วิเคราะห์แบบจำลองของ TLS 1.3 พวกเขาค้นพบและรายงานการโจมตีกลไกการกลับมาใช้เซสชัน 0-RTT ซึ่งได้รับการแก้ไขก่อนที่ RFC จะสรุปเป็นฉบับสุดท้าย
ข้อจำกัด: การประมาณและการวนซ้ำ
ProVerif ใช้การประมาณแบบครอบคลุมเกินจริง จึงอาจรายงานการโจมตีที่เป็นเท็จ (กล่าวว่า "เป็นเท็จ" ทั้งที่จริงแล้วโพรโทคอลปลอดภัย) แต่จะไม่พลาดการโจมตีจริง เซสชันโพรโทคอลที่มีจำนวนไม่จำกัดอาจไม่สิ้นสุด เพราะ ProVerif คลี่การวนซ้ำตามหลักฮิวริสติก
เมื่อ ProVerif ระบุว่า "CANNOT BE PROVED"
หาก ProVerif ไม่สามารถกำหนดผลลัพธ์ได้ภายใต้การประมาณของตน เครื่องมือจะแสดงผลว่า "CANNOT BE PROVED." นี่ไม่ใช่การพิสูจน์ว่าไม่ปลอดภัย แต่หมายความว่าเครื่องมือใช้ความสามารถด้านฮิวริสติกจนหมดแล้ว Tamarin อาจตรวจสอบกรณีเหล่านี้ได้สำเร็จ
ตรวจสอบความเข้าใจ
ผลลัพธ์ของ ProVerif ที่เป็น "RESULT ... เป็นเท็จ" หมายความว่าอย่างไรสำหรับข้อคำถามด้านการรักษาความลับ
ทบทวนบทเรียน
ProVerif ทำให้การตรวจสอบโพรโทคอลเป็นอัตโนมัติด้วยการหาคำตอบจากอนุประโยคฮอร์น โพรโทคอลเขียนด้วยแคลคูลัสไพประยุกต์และสมการทางการเข้ารหัส ข้อคำถามใช้สอบถามเรื่องการรักษาความลับและการพิสูจน์ตัวตน ผลลัพธ์ที่เป็นเท็จหมายถึงพิสูจน์ว่าปลอดภัย ส่วนผลลัพธ์ที่เป็นจริงหมายถึงถูกเจาะ ข้อจำกัดคือการประมาณอาจทำให้ได้ผลว่า "พิสูจน์ไม่ได้"
คำถามที่พบบ่อย
บทเรียน “ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ” ฟรีหรือไม่
ใช่ — ข้อความเต็มของ “ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ” ฟรีให้อ่านที่นี่บนเว็บ เพื่อปฏิบัติแบบโต้ตอบ (ตัวแก้ไขโค้ดในตัวและติวเตอร์ AI ตลอด 24/7) และปลดล็อคส่วนที่เหลือของคอร์ส Cryptology Academy ให้อัปเกรดเป็น CoddyKit PRO คอร์ส Cryptology Academy มีบทเรียนทั้งหมด 4 บทเรียน
คุณจะเรียนรู้อะไรในบทเรียน “ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ”
ระบุและตรวจสอบคุณสมบัติของแฮนด์เชก TLS ด้วย ProVerif คุณปฏิบัติ Cryptology Academy ด้วยโค้ดที่ใช้งานได้จริงที่คุณเรียกใช้โดยตรงในเบราว์เซอร์ และติวเตอร์ AI ตลอด 24/7 ตอบคำถามของคุณขณะที่คุณไปผ่านบทเรียน
คุณต้องมีประสบการณ์ก่อนที่จะเริ่มเรียน Cryptology Academy หรือไม่
ไม่จำเป็นต้องมีประสบการณ์มาก่อน Cryptology Academy บน CoddyKit ออกแบบมาสำหรับผู้เริ่มต้นไปจนถึงผู้เรียนขั้นสูง คุณสามารถเริ่มต้นที่นี่หรือเริ่มจากตัวแรกและเรียนด้วยความเร็วของคุณเอง นี่คือบทเรียนที่ 3 จากทั้งหมด 4 บทเรียน
บทเรียน “ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ” ใช้เวลานานแค่ไหน
บทเรียน CoddyKit ส่วนใหญ่ใช้เวลาประมาณ 5–10 นาที แต่ละบทเรียนจึงสั้นและเป็นแบบโต้ตอบ คุณสามารถก้าวหน้าอย่างต่อเนื่องและกลับมาเรียนต่อจากตรงที่เพิ่งหยุดบนเว็บและแอปได้เลย
ฉันเขียนและรันโค้ดในบทเรียน Cryptology Academy นี้ได้ไหม
ได้ บทเรียน Cryptology Academy ทุกบทมีตัวแก้ไขโค้ดในตัว คุณจึงเขียนและรันโค้ดจริงได้เลยในเบราว์เซอร์ และได้รับข้อเสนอแนะจาก AI ในทันที — ไม่ต้องติดตั้งในเครื่องของคุณ
บทเรียนทั้งหมดในหลักสูตรนี้
- เหตุใดบทพิสูจน์อย่างไม่เป็นทางการจึงไม่เพียงพอ
- แบบจำลองผู้โจมตี Dolev-Yao และการเข้ารหัสเชิงสัญลักษณ์
- ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ
- Tamarin และบทพิสูจน์เชิงคำนวณ