ProVerifเป็นเครื่องมือซอฟต์แวร์สำหรับการวิเคราะห์อัตโนมัติเกี่ยวกับคุณสมบัติด้านความปลอดภัยของโปรโตคอลการเข้ารหัสลับเครื่องมือนี้ได้รับการพัฒนาโดย Bruno Blanchet และคณะ

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

ProVerif ถูกนำไปใช้ในกรณีศึกษาต่อไปนี้ ซึ่งรวมถึงการวิเคราะห์ความปลอดภัยของโปรโตคอลเครือข่ายจริง:

• Abadi & Blanchet ^{[ 2 ]}ใช้การยืนยันการติดต่อเพื่อตรวจสอบโปรโตคอลอีเมลที่ได้รับการรับรอง^{[ 3 ]}
• Abadi, Blanchet & Fournet ^{[ 4 ]}วิเคราะห์โปรโตคอล Just Fast Keying ^{[ 5 ]}ซึ่งเป็นหนึ่งในตัวเลือกที่จะแทนที่Internet Key Exchange (IKE) ในฐานะโปรโตคอลการแลกเปลี่ยนคีย์ในIPsecโดยการรวมการพิสูจน์ด้วยตนเองเข้ากับการพิสูจน์ความสอดคล้องและความเท่าเทียมกันของ ProVerif
• Blanchet & Chaudhuri ^{[ 6 ]}ศึกษาความสมบูรณ์ของระบบไฟล์ Plutus ^{[ 7 ]}บนพื้นที่จัดเก็บที่ไม่น่าเชื่อถือ โดยใช้การยืนยันการติดต่อ ส่งผลให้มีการค้นพบและแก้ไขจุดอ่อนในระบบเริ่มต้นในภายหลัง
• Bhargavan และคณะ^{[ 8 ] [ 9 ] [ 10 ]}ใช้ ProVerif เพื่อวิเคราะห์การใช้งานโปรโตคอลการเข้ารหัสที่เขียนด้วยF#โดยเฉพาะอย่างยิ่ง โปรโตคอล Transport Layer Security (TLS) ได้รับการศึกษาในลักษณะนี้
• Chen & Ryan ^{[ 11 ]}ได้ประเมินโปรโตคอลการตรวจสอบสิทธิ์ที่พบในTrusted Platform Module (TPM) ซึ่งเป็นชิปฮาร์ดแวร์ที่ใช้งานอย่างแพร่หลาย และค้นพบช่องโหว่
• Delaune, Kremer & Ryan ^{[ 12 ] [ 13 ]}และ Backes, Hritcu & Maffei ^{[ 14 ]}ได้กำหนดรูปแบบและวิเคราะห์คุณสมบัติความเป็นส่วนตัวสำหรับการลงคะแนนเสียงทางอิเล็กทรอนิกส์โดยใช้ความเท่าเทียมกันของการสังเกต
• Delaune, Ryan & Smyth ^{[ 15 ]}และ Backes, Maffei & Unruh ^{[ 16 ]}วิเคราะห์ คุณสมบัติ การไม่เปิดเผยตัวตนของแผนการคอมพิวเตอร์ที่เชื่อถือได้Direct Anonymous Attestation (DAA) โดยใช้ความเท่าเทียมกันของการสังเกต
• Kusters & Truderung ^{[ 17 ] [ 18 ]} ตรวจ สอบโปรโตคอลด้วย การยกกำลัง Diffie-HellmanและXOR
• Smyth, Ryan, Kremer & Kourjieh ^{[ 19 ]}กำหนดรูปแบบและวิเคราะห์คุณสมบัติการตรวจสอบได้สำหรับการลงคะแนนเสียงทางอิเล็กทรอนิกส์โดยใช้การเข้าถึงได้
• Google ^{[ 20 ]}ได้ตรวจสอบโปรโตคอลเลเยอร์การขนส่งALTSแล้ว
• Sardar และคณะ^{[ 21 ] [ 22 ]}ได้ตรวจสอบโปรโตคอลการรับรองระยะไกลในIntel SGX

ตัวอย่างเพิ่มเติมสามารถพบได้ทางออนไลน์: [1 ]

เครื่องมือวิเคราะห์ทางเลือกอื่นๆ ได้แก่ AVISPA (สำหรับการยืนยันการเข้าถึงและความสอดคล้องกัน), KISS (สำหรับความเท่าเทียมกันแบบสถิต), YAPA (สำหรับความเท่าเทียมกันแบบสถิต) CryptoVerifสำหรับการตรวจสอบความปลอดภัยจาก การโจมตีของศัตรูที่ ใช้เวลาในการประมวลผลแบบพหุนามในแบบจำลองการคำนวณTamarin Proverเป็นทางเลือกที่ทันสมัยกว่า ProVerif โดยให้การสนับสนุนที่ดีเยี่ยมสำหรับการให้เหตุผลเชิงสมการ Diffie-Hellman และการตรวจสอบคุณสมบัติความเท่าเทียมกันจากการสังเกต

• เว็บไซต์อย่างเป็นทางการ