Tamarin และบทพิสูจน์เชิงคำนวณ
ใช้ตัวพิสูจน์ Tamarin สำหรับการเขียนใหม่แบบหลายเซตและการตรวจสอบจากร่องรอย
Tamarin และบทพิสูจน์เชิงคำนวณ เป็นบทเรียน Cryptology Academy ฟรีบน CoddyKit นี่คือบทเรียนที่ 4 จากทั้งหมด 4 บทเรียน คุณสามารถอ่านบทเรียนทั้งหมดด้านล่างฟรี — จากนั้นลองปฏิบัติด้วยตัวคุณเองในเบราว์เซอร์พร้อมตัวแก้ไขโค้ดในตัวและติวเตอร์ AI ตลอด 24/7 บทเรียนนี้เป็นส่วนหนึ่งของเส้นทางการเรียน Cryptology Academy และความก้าวหน้าของคุณจะซิงค์ข้ามเว็บและแอป CoddyKit คอร์ส Cryptology Academy มีบทเรียนทั้งหมด 4 บทเรียน
Tamarin คืออะไร
Tamarin (ETH Zurich, 2012) เป็นเครื่องมือตรวจสอบโพรโทคอลความปลอดภัยที่ใช้การเขียนใหม่แบบมัลติเซต ต่างจากแนวทางอนุประโยคฮอร์นของ ProVerif ตรงที่ Tamarin ใช้เหตุผลเกี่ยวกับ ร่องรอย ของการทำงานของโพรโทคอลผ่านตัวพิสูจน์แบบโต้ตอบ
Tamarin กับ ProVerif
ProVerif: ทำงานอัตโนมัติเต็มรูปแบบ แต่อาจให้ผลว่า "พิสูจน์ไม่ได้" Tamarin: มีผู้ช่วยพิสูจน์แบบโต้ตอบและโหมดอัตโนมัติ รองรับทฤษฎีสมการ (XOR, Diffie-Hellman และการจับคู่แบบบิลิเนียร์) แสดงคุณสมบัติได้มากกว่า แต่มีเส้นโค้งการเรียนรู้ที่ชันกว่า
กฎการเขียนใหม่แบบมัลติเซต
Tamarin สร้างแบบจำลองโพรโทคอลเป็นกฎการเขียนใหม่บนข้อเท็จจริง ข้อเท็จจริงใช้แทนสถานะ กฎ [ L ] --[ A ]-> [ R ] ใช้ข้อเท็จจริงด้านซ้าย L สร้างข้อเท็จจริงด้านขวา R และบันทึกการกระทำ A ลงในร่องรอย
ภาษาข้อมูลเข้าของ Tamarin (.spthy)
ไฟล์ทฤษฎีของ Tamarin ประกาศฟังก์ชัน สมการ กฎ และบทตั้ง:
/* Diffie-Hellman key exchange */
builtins: diffie-hellman
rule Alice_1:
[ Fr(~a) ] /* fresh random a */
--[ AliceSent($A, $B, 'g'^~a) ]->
[ Alice_St($A, $B, ~a), Out('g'^~a) ]
rule Bob_1:
[ In(ga), Fr(~b) ]
--[ BobReceived($A, $B, ga) ]->
[ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]การระบุบทตั้ง
เป้าหมายด้านความปลอดภัยแสดงเป็นบทตั้งเหนือร่องรอย:
/* Secrecy: shared secret not known to attacker */
lemma secret_key:
"All A B k #i #j.
AliceKey(A, B, k) @ i &
BobKey(A, B, k) @ j
==> not (Ex #r. K(k) @ r)"
/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
"All A B k #j. BobKey(A, B, k) @ j
==> Ex #i. AliceKey(A, B, k) @ i & i < j"การเรียกใช้ Tamarin
เปิดส่วนติดต่อผู้ใช้แบบกราฟิกของ Tamarin: tamarin-prover interactive my_protocol.spthy ส่วนติดต่อผู้ใช้บนเบราว์เซอร์จะแสดงภาระการพิสูจน์ คุณสามารถชี้นำกลยุทธ์อัตโนมัติหรือใช้ขั้นตอนด้วยตนเองสำหรับกรณีที่การทำงานไม่สิ้นสุด
ความถูกต้องเชิงคำนวณ
การพิสูจน์เชิงสัญลักษณ์ (ProVerif, Tamarin) รับรองความปลอดภัยภายใต้สมมติฐานว่าการเข้ารหัสสมบูรณ์แบบ ทฤษฎี ความถูกต้องเชิงคำนวณ (Cortier, Backes) ยกระดับการพิสูจน์เชิงสัญลักษณ์ไปสู่ความปลอดภัยเชิงคำนวณ เมื่อนำไปสร้างอินสแตนซ์ด้วยองค์ประกอบพื้นฐานที่พิสูจน์ได้ว่าปลอดภัย
F* และ HACL*: การนำไปใช้งานที่ผ่านการตรวจสอบ
F* (Microsoft Research) เป็นภาษาการเขียนโปรแกรมที่มุ่งเน้นการพิสูจน์ HACL* เป็นไลบรารีการเข้ารหัสที่เขียนด้วย F* พร้อมการพิสูจน์ความถูกต้องและความต้านทานต่อการโจมตีช่องทางข้างเคียงที่ตรวจสอบด้วยเครื่องจักร ใช้ใน Firefox NSS และ mbedTLS
EasyCrypt: การพิสูจน์เชิงคำนวณแบบอิงเกม
EasyCrypt ช่วยให้สามารถพิสูจน์ความปลอดภัยเชิงคำนวณแบบเต็มรูปแบบ (อิงเกม) สำหรับโครงสร้างการเข้ารหัส ไม่ใช่เฉพาะโพรโทคอลเท่านั้น ชั้นระเบียนของ TLS 1.3 และ ChaCha20-Poly1305 ได้รับการตรวจสอบด้วย EasyCrypt แล้ว
ผลกระทบในทางปฏิบัติ
การเข้ารหัสที่ผ่านการตรวจสอบอย่างเป็นรูปนัยกำลังเข้าสู่การใช้งานจริง: NSS (Firefox) ใช้ HACL*, AWS ใช้ s2n-tls พร้อมข้อยืนยันที่มาพร้อมหลักฐานการพิสูจน์ และโพรโทคอล Signal ได้รับการตรวจสอบด้วย ProVerif และ Tamarin วิธีการเชิงรูปนัยไม่ได้จำกัดอยู่แค่ในแวดวงวิชาการอีกต่อไป
ตรวจสอบความเข้าใจ
Tamarin แตกต่างจาก ProVerif อย่างไรในการจัดการกรณีที่ระบบอัตโนมัติทำงานไม่สำเร็จ
ทบทวนบทเรียน
Tamarin ใช้การเขียนใหม่แบบมัลติเซตและการให้เหตุผลตามร่องรอยผ่านส่วนติดต่อผู้ใช้แบบกราฟิกสำหรับการพิสูจน์แบบโต้ตอบ รองรับทฤษฎีสมการ DH และ XOR บทตั้งใช้แสดงเป้าหมายด้านการรักษาความลับและการพิสูจน์ตัวตน ความถูกต้องเชิงคำนวณเชื่อมการพิสูจน์เชิงสัญลักษณ์เข้ากับความปลอดภัยจริง HACL* และ EasyCrypt ขยายการตรวจสอบไปยังการนำไปใช้งานและโครงสร้างการเข้ารหัส
เรียนรู้ Cryptology Academy ด้วย AI tutor — ฟรี
เขียนและเรียกใช้โค้ดจริงในเบราว์เซอร์ของคุณ รับความช่วยเหลือทันทีจาก AI tutor 24/7 และเรียนรู้ต่อจากที่คุณหยุดบนเว็บหรือในแอป
- คอร์ส
- 67
- บทเรียน
- 261
คำถามที่พบบ่อย
บทเรียน “Tamarin และบทพิสูจน์เชิงคำนวณ” ฟรีหรือไม่
ใช่ — ข้อความเต็มของ “Tamarin และบทพิสูจน์เชิงคำนวณ” ฟรีให้อ่านที่นี่บนเว็บ เพื่อปฏิบัติแบบโต้ตอบ (ตัวแก้ไขโค้ดในตัวและติวเตอร์ AI ตลอด 24/7) และปลดล็อคส่วนที่เหลือของคอร์ส Cryptology Academy ให้อัปเกรดเป็น CoddyKit PRO คอร์ส Cryptology Academy มีบทเรียนทั้งหมด 4 บทเรียน
คุณจะเรียนรู้อะไรในบทเรียน “Tamarin และบทพิสูจน์เชิงคำนวณ”
ใช้ตัวพิสูจน์ Tamarin สำหรับการเขียนใหม่แบบหลายเซตและการตรวจสอบจากร่องรอย คุณปฏิบัติ Cryptology Academy ด้วยโค้ดที่ใช้งานได้จริงที่คุณเรียกใช้โดยตรงในเบราว์เซอร์ และติวเตอร์ AI ตลอด 24/7 ตอบคำถามของคุณขณะที่คุณไปผ่านบทเรียน
คุณต้องมีประสบการณ์ก่อนที่จะเริ่มเรียน Cryptology Academy หรือไม่
ไม่จำเป็นต้องมีประสบการณ์มาก่อน Cryptology Academy บน CoddyKit ออกแบบมาสำหรับผู้เริ่มต้นไปจนถึงผู้เรียนขั้นสูง คุณสามารถเริ่มต้นที่นี่หรือเริ่มจากตัวแรกและเรียนด้วยความเร็วของคุณเอง นี่คือบทเรียนที่ 4 จากทั้งหมด 4 บทเรียน
บทเรียน “Tamarin และบทพิสูจน์เชิงคำนวณ” ใช้เวลานานแค่ไหน
บทเรียน CoddyKit ส่วนใหญ่ใช้เวลาประมาณ 5–10 นาที แต่ละบทเรียนจึงสั้นและเป็นแบบโต้ตอบ คุณสามารถก้าวหน้าอย่างต่อเนื่องและกลับมาเรียนต่อจากตรงที่เพิ่งหยุดบนเว็บและแอปได้เลย
ฉันเขียนและรันโค้ดในบทเรียน Cryptology Academy นี้ได้ไหม
ได้ บทเรียน Cryptology Academy ทุกบทมีตัวแก้ไขโค้ดในตัว คุณจึงเขียนและรันโค้ดจริงได้เลยในเบราว์เซอร์ และได้รับข้อเสนอแนะจาก AI ในทันที — ไม่ต้องติดตั้งในเครื่องของคุณ
บทเรียนทั้งหมดในหลักสูตรนี้
- เหตุใดบทพิสูจน์อย่างไม่เป็นทางการจึงไม่เพียงพอ
- แบบจำลองผู้โจมตี Dolev-Yao และการเข้ารหัสเชิงสัญลักษณ์
- ProVerif: การตรวจสอบโพรโทคอลอัตโนมัติ
- Tamarin และบทพิสูจน์เชิงคำนวณ