Tamarin ve Hesaplamalı İspatlar
Çoklu küme yeniden yazımı ve iz tabanlı doğrulama için Tamarin ispatlayıcısını kullanın.
Tamarin ve Hesaplamalı İspatlar, CoddyKit'te ücretsiz bir Cryptology Academy dersidir. Bu, 4 dersinin 4. 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.
Tamarin Nedir
Tamarin (ETH Zurich, 2012), çoklu-küme yeniden yazımına dayanan bir güvenlik protokolü doğrulayıcısıdır. ProVerif'in Horn tümcesi yaklaşımından farklı olarak Tamarin, etkileşimli bir kanıtlayıcıyla protokol yürütmelerinin izleri hakkında akıl yürütür.
Tamarin ve ProVerif
ProVerif: tamamen otomatik, "kanıtlanamaz" diyebilir. Tamarin: etkileşimli kanıt yardımcısı + otomatik kip; eşitliksel teorileri (XOR, Diffie-Hellman, bilineer dönüşümler) ele alır. Daha ifade gücü yüksektir, ancak öğrenme eğrisi daha diktir.
Çoklu-Küme Yeniden Yazma Kuralları
Tamarin, protokolleri olgular üzerindeki yeniden yazma kuralları olarak modeller. Olgular durumu temsil eder. Bir kural [ L ] --[ A ]-> [ R ], sol taraftaki L olgularını tüketir, sağ taraftaki R olgularını üretir ve A eylemini iz günlüğüne kaydeder.
Tamarin Girdi Dili (.spthy)
Bir Tamarin teori dosyasında işlevler, denklemler, kurallar ve önermeler bildirilir:
/* 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) ]Önermeleri Belirtme
Güvenlik hedefleri, izler üzerindeki önermeler olarak ifade edilir:
/* 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'i Çalıştırma
Tamarin'in etkileşimli GUI'sini başlatın: tamarin-prover interactive my_protocol.spthy. Tarayıcı arayüzü kanıt yükümlülüklerini gösterir; otomatik stratejileri yönlendirir veya sonlanmayan durumlarda elle adımlar uygularsınız.
Hesaplamalı Sağlamlık
Sembolik kanıtlar (ProVerif, Tamarin), kusursuz kriptografi varsayımları altında güvenliği garanti eder. Hesaplamalı sağlamlık teoremleri (Cortier, Backes), sembolik kanıtları, kanıtlanabilir şekilde güvenli ilkellerle gerçekleştirildiğinde hesaplamalı güvenliğe taşır.
F* ve HACL*: Doğrulanmış Uygulamalar
F* (Microsoft Research), kanıt odaklı bir programlama dilidir. HACL*, doğruluk ve yan kanal saldırılarına direnç konusunda makine tarafından doğrulanmış kanıtlar içeren, F* ile yazılmış bir kriptografik kütüphanedir. Firefox NSS ve mbedTLS'de kullanılır.
EasyCrypt: Oyun Tabanlı Hesaplamalı Kanıtlar
EasyCrypt, yalnızca protokoller için değil, kriptografik yapılar için de tamamen hesaplamalı (oyun tabanlı) güvenlik kanıtları oluşturmayı sağlar. TLS 1.3 kayıt katmanı ve ChaCha20-Poly1305 EasyCrypt'te doğrulanmıştır.
Pratik Etki
Biçimsel olarak doğrulanmış kriptografi üretime giriyor: NSS (Firefox) HACL* kullanıyor, AWS kanıt taşıyan iddialarla s2n-tls kullanıyor ve Signal protokolü ProVerif ile Tamarin'de doğrulandı. Biçimsel yöntemler artık yalnızca akademik değildir.
Bilgi Kontrolü
Otomasyon başarısız olduğunda ortaya çıkan durumları ele alma konusunda Tamarin, ProVerif'ten nasıl farklıdır?
Ders Özeti
Tamarin, çoklu-küme yeniden yazımını ve etkileşimli bir kanıt GUI'siyle iz tabanlı akıl yürütmeyi kullanır. DH ve XOR eşitliksel teorilerini ele alır. Önermeler gizlilik ve kimlik doğrulama hedeflerini ifade eder. Hesaplamalı sağlamlık, sembolik kanıtları gerçek güvenliğe bağlar. HACL* ve EasyCrypt, doğrulamayı uygulamalara ve yapılara genişletir.
Yapay zeka eğitmeniyle Cryptology Academy öğren — ücretsiz
Tarayıcında gerçek kod yaz ve çalıştır, 7/24 yapay zeka eğitmeninden anında yardım al; web'de ya da uygulamada kaldığın yerden devam et.
- Kurslar
- 67
- Dersler
- 261
Sıkça Sorulan Sorular
“Tamarin ve Hesaplamalı İspatlar” dersi ücretsiz mi?
Evet — “Tamarin ve Hesaplamalı İspatlar” 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.
“Tamarin ve Hesaplamalı İspatlar” dersinde ne öğreneceğim?
Çoklu küme yeniden yazımı ve iz tabanlı doğrulama için Tamarin ispatlayıcısını kullanı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 4. dersidir.
“Tamarin ve Hesaplamalı İspatlar” 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