ProVerif: Otomatik Protokol Doğrulama
TLS el sıkışması özelliklerini ProVerif ile tanımlayın ve doğrulayın.
ProVerif: Otomatik Protokol Doğrulama, CoddyKit'te ücretsiz bir Cryptology Academy dersidir. Bu, 4 dersinin 3. dersidir. Aşağıdan dersin tamamını ücretsiz okuyabilir, sonra tarayıcıda yerleşik kod editörü ve 7/24 yapay zeka koçu ile uygulamalı olarak pratik yapabilirsin. Bu, Cryptology Academy öğrenme yolunun bir parçasıdır ve ilerlemeniz web ve CoddyKit uygulaması arasında senkronize olur. Cryptology Academy kursu toplamda 4 dersten oluşur.
ProVerif Nedir
ProVerif (Bruno Blanchet, 2001), otomatik bir kriptografik protokol doğrulayıcısıdır. Uygulamalı pi hesabında açıklanan bir protokolü alır ve gizlilik ile kimlik doğrulama özelliklerini otomatik olarak doğrular.
ProVerif Nasıl Çalışır
ProVerif, protokolü Horn tümcelerine dönüştürür ve saldırganın neleri öğrenebileceğini türetmek için çözümleme tabanlı bir algoritma uygular. Bir gizlilik olgusu türetilebiliyorsa protokol bozulmuştur; aksi hâlde güvenli olduğu kanıtlanır.
ProVerif Girdi Dili
Protokoller bildirimsel olarak açıklanır: kanallar, türler, işlevler (enc, dec, sign, verify), denklemler (dec(enc(m,k),k)=m) ve kanallar üzerinden iletişim kuran süreçler bildirilir.
Kriptografik İlkelleri Bildirme
Örnek ProVerif bildirimleri:
(* 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.Basit Bir Protokol Süreci Yazma
Alice ve Bob'u paralel süreçler olarak modelleyin:
(* 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)))Güvenlik Sorgularını Belirtme
ProVerif şu tür sorguları denetler:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).ProVerif Çıktısını Yorumlama
ProVerif, "RESULT ... doğrudur" (güvenli olduğu kanıtlanmıştır) veya "RESULT ... yanlıştır" çıktısını verir ve saldırganın iletilerini gösteren karşı örnek saldırı izini yazdırır. İz, saldırının tam olarak nasıl işlediğini gösterir.
TLS 1.3'ü ProVerif ile Doğrulama
Bhargavan ve diğerleri (2016), TLS 1.3 modelini analiz etmek için ProVerif'i kullandı. 0-RTT oturum devam ettirme mekanizmasına yönelik bir saldırı bulup raporladılar; bu saldırı RFC son hâline getirilmeden önce düzeltildi.
Sınırlamalar: Yaklaştırma ve Döngüler
ProVerif üstten yaklaşıklar: yanlış saldırılar bildirebilir (protokol aslında güvenliyken "yanlış" diyebilir) ancak gerçek saldırıları asla kaçırmaz. Sınırsız protokol oturumları sonlanmayabilir — ProVerif döngüleri buluşsal olarak açar.
ProVerif "Kanıtlanamaz" Dediğinde
ProVerif, kendi yaklaştırması içinde sonucu belirleyemezse "CANNOT KANITLANAMADI." çıktısını verir. Bu, güvensizliğin kanıtı değildir — aracın buluşsal gücünün tükendiği anlamına gelir. Tamarin bu durumlarda başarılı olabilir.
Bilgi Kontrolü
Bir gizlilik sorgusu için ProVerif çıktısının "RESULT ... yanlıştır" olması ne anlama gelir?
Ders Özeti
ProVerif, Horn tümcesi çözümlemesini kullanarak protokol doğrulamasını otomatikleştirir. Protokoller, kriptografik denklemlerle birlikte uygulamalı pi hesabında yazılır. Sorgular gizlilik ve kimlik doğrulama hakkında sorular sorar. Yanlış, güvenliğin kanıtlandığı; doğru ise protokolün bozulduğu anlamına gelir (saldırı iziyle birlikte). Sınırlamalar: yaklaştırmalar "kanıtlanamaz" sonucu verebilir.
Sıkça Sorulan Sorular
“ProVerif: Otomatik Protokol Doğrulama” dersi ücretsiz mi?
Evet — “ProVerif: Otomatik Protokol Doğrulama” dersin tüm metni burada web'de ücretsiz olarak okunabilir. Etkileşimli olarak pratik yapmak (yerleşik kod editörü ve 7/24 yapay zeka koçu) ve Cryptology Academy kursunun geri kalanını açmak için CoddyKit PRO'ya yükselt. Cryptology Academy kursu toplamda 4 dersten oluşur.
“ProVerif: Otomatik Protokol Doğrulama” dersinde ne öğreneceğim?
TLS el sıkışması özelliklerini ProVerif ile tanımlayın ve doğrulayın. Cryptology Academy ile uygulamalı kodu tarayıcıda doğrudan çalıştırarak pratik yaparsın ve 7/24 yapay zeka koçu dersi çalışırken sorularını yanıtlar.
Cryptology Academy öğrenmeye başlamak için deneyim gerekli mi?
Önceden deneyim gerekmez. CoddyKit'te Cryptology Academy, başlangıçtan ileri seviyeye kadar yapılandırıldığı için buradan başlayabilir veya başından başlayıp kendi hızında ilerleme yapabilirsin. Bu, 4 dersinin 3. dersidir.
“ProVerif: Otomatik Protokol Doğrulama” dersi ne kadar sürer?
Çoğu CoddyKit dersi yaklaşık 5–10 dakika sürer. Her biri kısa ve etkileşimli olduğu için sabit ilerleme yaparsın ve web ile uygulama arasında tam olarak bıraktığın yerden devam edebilirsin.
Bu Cryptology Academy dersinde kod yazıp çalıştırabilir miyim?
Evet. Her Cryptology Academy dersi yerleşik bir kod editörü içerir, bu sayede tarayıcıda gerçek kod yazıp çalıştırabilir ve anlık yapay zeka geri bildirimi alırsın — yerel kurulum gerekli değildir.
Bu kursun tüm dersleri
- Gayriresmî İspatlar Neden Yeterli Değildir?
- Dolev-Yao Saldırgan Modeli ve Sembolik Kriptografi
- ProVerif: Otomatik Protokol Doğrulama
- Tamarin ve Hesaplamalı İspatlar