Tamarin & Pembuktian Komputasional
Gunakan pembukti Tamarin untuk penulisan ulang multiset dan verifikasi berbasis jejak.
Tamarin & Pembuktian Komputasional adalah pelajaran Cryptology Academy gratis di CoddyKit. Ini adalah pelajaran 4 dari 4. Kamu bisa membaca pelajaran lengkapnya di bawah secara gratis — lalu praktikkan langsung di browser dengan editor kode bawaan dan tutor AI 24/7. Ini adalah bagian dari jalur belajar Cryptology Academy, dan progresmu tersinkronisasi di web dan aplikasi CoddyKit. Kursus Cryptology Academy mencakup 4 pelajaran total.
Apa Itu Tamarin?
Tamarin (ETH Zurich, 2012) adalah pemeriksa protokol keamanan yang didasarkan pada penulisan ulang multihimpunan. Berbeda dari pendekatan klausa Horn ProVerif, Tamarin menalar jejak eksekusi protokol dengan pembukti interaktif.
Tamarin dibandingkan dengan ProVerif
ProVerif: sepenuhnya otomatis, tetapi mungkin menghasilkan "tidak dapat dibuktikan." Tamarin: asisten pembuktian interaktif + mode otomatis, serta menangani teori persamaan (XOR, Diffie-Hellman, dan peta bilinear). Lebih ekspresif, tetapi kurva pembelajarannya lebih curam.
Aturan Penulisan Ulang Multihimpunan
Tamarin memodelkan protokol sebagai aturan penulisan ulang atas fakta. Fakta merepresentasikan keadaan. Aturan [ L ] --[ A ]-> [ R ] menggunakan fakta sisi kiri L, menghasilkan fakta sisi kanan R, dan mencatat tindakan A dalam jejak.
Bahasa Masukan Tamarin (.spthy)
Berkas teori Tamarin mendeklarasikan fungsi, persamaan, aturan, dan lema:
/* 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) ]Menyatakan Lema
Sasaran keamanan dinyatakan sebagai lema atas jejak:
/* 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"Menjalankan Tamarin
Luncurkan GUI interaktif Tamarin: tamarin-prover interactive my_protocol.spthy. Antarmuka peramban menampilkan kewajiban pembuktian; Anda memandu strategi otomatis atau menerapkan langkah manual untuk kasus yang tidak berhenti.
Keterandalan Komputasional
Pembuktian simbolis (ProVerif, Tamarin) menjamin keamanan berdasarkan asumsi kriptografi sempurna. Teorema keterandalan komputasional (Cortier, Backes) mengangkat pembuktian simbolis menjadi keamanan komputasional ketika diinstansiasi dengan primitif yang terbukti aman.
F* dan HACL*: Implementasi Terverifikasi
F* (Microsoft Research) adalah bahasa pemrograman berorientasi pembuktian. HACL* adalah pustaka kriptografi yang ditulis dalam F* dengan pembuktian kebenaran dan ketahanan terhadap kanal samping yang diverifikasi mesin. Pustaka ini digunakan dalam Firefox NSS dan mbedTLS.
EasyCrypt: Pembuktian Komputasional Berbasis Permainan
EasyCrypt memungkinkan pembuktian keamanan yang sepenuhnya komputasional (berbasis permainan) untuk konstruksi kriptografi — bukan hanya protokol. Lapisan rekaman TLS 1.3 dan ChaCha20-Poly1305 telah diverifikasi dalam EasyCrypt.
Dampak Praktis
Kriptografi yang diverifikasi secara formal mulai digunakan dalam produksi: NSS (Firefox) menggunakan HACL*, AWS menggunakan s2n-tls dengan asersi yang disertai bukti, dan protokol Signal telah diverifikasi dalam ProVerif dan Tamarin. Metode formal tidak lagi hanya bersifat akademis.
Uji Pemahaman
Bagaimana Tamarin berbeda dari ProVerif dalam menangani kasus ketika otomatisasi gagal?
Ringkasan Pelajaran
Tamarin menggunakan penulisan ulang multihimpunan dan penalaran berbasis jejak dengan GUI pembuktian interaktif. Tamarin menangani teori persamaan DH dan XOR. Lema menyatakan sasaran kerahasiaan dan autentikasi. Keterandalan komputasional menjembatani pembuktian simbolis dengan keamanan nyata. HACL* dan EasyCrypt memperluas verifikasi ke implementasi dan konstruksi.
Belajar Cryptology Academy dengan tutor AI — gratis
Tulis dan jalankan kode asli di browser kamu, dapatkan bantuan instan dari tutor AI 24/7, dan lanjutkan di mana kamu tinggalkan di web atau aplikasi.
- Kursus
- 67
- Pelajaran
- 261
Pertanyaan yang Sering Diajukan
Apakah pelajaran “Tamarin & Pembuktian Komputasional” gratis?
Ya — teks lengkap “Tamarin & Pembuktian Komputasional” gratis dibaca di sini di web. Untuk praktiknya secara interaktif (editor kode bawaan dan tutor AI 24/7) dan buka sisa kursus Cryptology Academy, upgrade ke CoddyKit PRO. Kursus Cryptology Academy mencakup 4 pelajaran total.
Apa yang akan aku pelajari di “Tamarin & Pembuktian Komputasional”?
Gunakan pembukti Tamarin untuk penulisan ulang multiset dan verifikasi berbasis jejak. Kamu berlatih Cryptology Academy dengan kode praktik yang langsung kamu jalankan di browser, dan tutor AI 24/7 menjawab pertanyaanmu saat kamu mengerjakan pelajaran ini.
Apakah aku perlu pengalaman untuk memulai Cryptology Academy?
Tidak diperlukan pengalaman sebelumnya. Cryptology Academy di CoddyKit dirancang untuk pemula hingga pelajar tingkat lanjut, jadi kamu bisa memulai di sini atau dari awal dan belajar sesuai kecepatan kamu sendiri. Ini adalah pelajaran 4 dari 4.
Berapa lama pelajaran “Tamarin & Pembuktian Komputasional” memakan waktu?
Sebagian besar pelajaran CoddyKit memakan waktu sekitar 5–10 menit. Setiap pelajaran ringkas dan interaktif, jadi kamu membuat kemajuan stabil dan melanjutkan dari tempat kamu tinggalkan di web dan aplikasi.
Bisakah aku menulis dan menjalankan kode dalam pelajaran Cryptology Academy ini?
Ya. Setiap pelajaran Cryptology Academy menyertakan editor kode bawaan, jadi kamu menulis dan menjalankan kode nyata langsung di browser dan mendapatkan umpan balik AI instan — tidak diperlukan penyiapan lokal.
Semua pelajaran dalam kursus ini
- Mengapa Pembuktian Informal Tidak Cukup
- Model Penyerang Dolev-Yao & Kripto Simbolis
- ProVerif: Verifikasi Protokol Otomatis
- Tamarin & Pembuktian Komputasional