ProVerif: Pengesahan Protokol Automatik
Nyatakan dan sahkan sifat jabat tangan TLS dengan ProVerif.
ProVerif: Pengesahan Protokol Automatik ialah pelajaran Cryptology Academy percuma di CoddyKit. Ini ialah pelajaran 3 daripada 4. Anda boleh membaca keseluruhan pelajaran di bawah secara percuma — kemudian berlatih secara praktikal dalam pelayar menggunakan penyunting kod terbina dalam dan tutor kecerdasan buatan 24/7. Pelajaran ini merupakan sebahagian daripada laluan pembelajaran Cryptology Academy, dan kemajuan anda disegerakkan merentas web serta aplikasi CoddyKit. Kursus Cryptology Academy merangkumi sejumlah 4 pelajaran.
Apakah ProVerif?
ProVerif (Bruno Blanchet, 2001) ialah pengesah automatik protokol kriptografi. Ia mengambil protokol yang diterangkan dalam kalkulus pi gunaan dan menentukan sifat kerahsiaan serta pengesahan secara automatik.
Cara ProVerif Berfungsi
ProVerif menterjemahkan protokol kepada klausa Horn dan menggunakan algoritma berasaskan resolusi untuk memperoleh perkara yang boleh dipelajari oleh penyerang. Jika fakta kerahsiaan boleh diterbitkan, protokol itu telah dipecahkan; jika tidak, keselamatannya terbukti.
Bahasa Input ProVerif
Protokol diterangkan secara deklaratif: isytiharkan saluran, jenis, fungsi (enc, dec, sign, verify), persamaan (dec(enc(m,k),k)=m) dan proses yang berkomunikasi melalui saluran.
Mengisytiharkan Primitif Kriptografi
Contoh pengisytiharan 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.Menulis Proses Protokol Mudah
Modelkan Alice dan Bob sebagai proses selari:
(* 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)))Menyatakan Pertanyaan Keselamatan
ProVerif menyemak pertanyaan seperti:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).Mentafsir Output ProVerif
ProVerif menghasilkan "RESULT ... adalah benar" (keselamatan terbukti) atau "RESULT ... adalah palsu" dan mencetak jejak serangan balas yang menunjukkan mesej penyerang. Jejak itu menunjukkan dengan tepat cara serangan tersebut berlaku.
Mengesahkan TLS 1.3 dengan ProVerif
Bhargavan et al. (2016) menggunakan ProVerif untuk menganalisis model TLS 1.3. Mereka menemui dan melaporkan serangan terhadap mekanisme penyambungan semula 0-RTT, yang telah dibaiki sebelum RFC itu dimuktamadkan.
Batasan: Anggaran dan Gelung
ProVerif membuat anggaran berlebihan: ia mungkin melaporkan serangan palsu (mengatakan "palsu" apabila protokol sebenarnya selamat) tetapi tidak pernah terlepas serangan sebenar. Sesi protokol tanpa had mungkin tidak berakhir — ProVerif mengembangkan gelung secara heuristik.
Apabila ProVerif Mengatakan "CANNOT BE PROVED"
Jika ProVerif tidak dapat menentukan hasil dalam anggarannya, ia menghasilkan "CANNOT BE PROVED." Ini bukan bukti ketidakselamatan — ini bermaksud alat tersebut telah kehabisan keupayaan heuristiknya. Tamarin mungkin berjaya dalam kes ini.
Semakan Pengetahuan
Apakah maksud output ProVerif "RESULT ... adalah palsu" untuk pertanyaan kerahsiaan?
Ulang Kaji Pelajaran
ProVerif mengautomasikan pengesahan protokol menggunakan resolusi klausa Horn. Protokol ditulis dalam kalkulus pi gunaan dengan persamaan kriptografi. Pertanyaan menanyakan tentang kerahsiaan dan pengesahan. Palsu bermaksud terbukti selamat; benar bermaksud telah dipecahkan (dengan jejak serangan). Batasan: anggaran mungkin menghasilkan "tidak dapat dibuktikan."
Pelajari Cryptology Academy dengan tutor kecerdasan buatan — percuma
Tulis dan jalankan kod sebenar dalam pelayar anda, dapatkan bantuan segera daripada tutor kecerdasan buatan yang tersedia 24/7, dan sambung semula dari tempat anda berhenti di web atau dalam aplikasi.
- Kursus
- 67
- Pelajaran
- 261
Soalan Lazim
Adakah pelajaran “ProVerif: Pengesahan Protokol Automatik” percuma?
Ya — teks penuh “ProVerif: Pengesahan Protokol Automatik” boleh dibaca secara percuma di web ini. Untuk berlatih secara interaktif menggunakan penyunting kod terbina dalam dan tutor kecerdasan buatan 24/7, serta membuka kunci baki kursus Cryptology Academy, tingkat taraf kepada CoddyKit PRO. Kursus Cryptology Academy merangkumi sejumlah 4 pelajaran.
Apakah yang akan saya pelajari dalam “ProVerif: Pengesahan Protokol Automatik”?
Nyatakan dan sahkan sifat jabat tangan TLS dengan ProVerif. Anda berlatih Cryptology Academy menggunakan kod praktikal yang dijalankan terus dalam pelayar, manakala tutor kecerdasan buatan 24/7 menjawab soalan anda semasa anda mengikuti pelajaran.
Adakah saya memerlukan pengalaman untuk memulakan Cryptology Academy?
Tiada pengalaman terdahulu diperlukan. Pembelajaran Cryptology Academy di CoddyKit disusun untuk pelajar daripada peringkat pemula hingga lanjutan, jadi anda boleh bermula di sini atau dari awal dan belajar mengikut kadar anda sendiri. Ini ialah pelajaran 3 daripada 4.
Berapa lamakah pelajaran “ProVerif: Pengesahan Protokol Automatik” diambil?
Kebanyakan pelajaran CoddyKit mengambil masa kira-kira 5–10 minit. Setiap pelajaran ringkas dan interaktif, jadi anda boleh membuat kemajuan secara berterusan dan menyambung tepat dari tempat anda berhenti di web atau aplikasi.
Bolehkah saya menulis dan menjalankan kod dalam pelajaran Cryptology Academy ini?
Ya. Setiap pelajaran Cryptology Academy menyertakan penyunting kod terbina dalam, jadi anda boleh menulis dan menjalankan kod sebenar terus dalam pelayar serta menerima maklum balas kecerdasan buatan serta-merta — tanpa memerlukan persediaan setempat.
Semua pelajaran dalam kursus ini
- Mengapa Bukti Tidak Formal Tidak Mencukupi
- Model Penyerang Dolev-Yao & Kripto Simbolik
- ProVerif: Pengesahan Protokol Automatik
- Tamarin & Bukti Pengiraan