Tamarin ja laskennalliset todistukset
Käyttäkää Tamarin-proveria multiset rewriting -menetelmään ja jälkipohjaiseen varmennukseen.
Tamarin ja laskennalliset todistukset on ilmainen Cryptology Academy-oppitunti CoddyKitissä. Tämä on oppitunti 4/4. Voit lukea koko oppitunnin alta ilmaiseksi ja harjoitella sen jälkeen käytännössä selaimessa sisäänrakennetulla koodieditorilla ja ympäri vuorokauden käytettävissä olevan tekoälytuutorin avulla. Oppitunti kuuluu Cryptology Academy-oppimispolkuun, ja edistymisesi synkronoituu verkon ja CoddyKit-sovelluksen välillä. Cryptology Academy-kurssilla on yhteensä 4 oppituntia.
Mikä Tamarin on?
Tamarin (ETH Zurich, 2012) on multijoukon uudelleenkirjoitukseen perustuva turvallisuusprotokollien verifiointityökalu. Toisin kuin ProVerifin Horn-lausekkeisiin perustuvassa lähestymistavassa, Tamarin päättelöi protokollan suoritusten jäljistä vuorovaikutteisen todistajan avulla.
Tamarin ja ProVerif
ProVerif: täysin automaattinen, mutta voi ilmoittaa "cannot be proved". Tamarin: vuorovaikutteinen todistusavustin ja automaattinen tila, joka käsittelee yhtälöteorioita (XOR, Diffie-Hellman, bilineaariset kuvaukset). Ilmaisuvoima on suurempi, mutta oppimiskäyrä jyrkempi.
Multijoukon uudelleenkirjoitussäännöt
Tamarin mallintaa protokollat faktoihin kohdistuvina uudelleenkirjoitussääntöinä. Faktat kuvaavat tilaa. Sääntö [ L ] --[ A ]-> [ R ] kuluttaa vasemman puolen faktat L, tuottaa oikean puolen faktat R ja kirjaa toiminnon A jälkeenjäljitykseen.
Tamarinin syötekieli (.spthy)
Tamarinin teoriatiedostossa määritellään funktiot, yhtälöt, säännöt ja lemmat:
/* 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) ]Lemmojen esittäminen
Turvallisuustavoitteet ilmaistaan jälkiä koskevina lemmoina:
/* 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"Tamarinin suorittaminen
Käynnistä Tamarinin vuorovaikutteinen graafinen käyttöliittymä: tamarin-prover interactive my_protocol.spthy. Selainkäyttöliittymä näyttää todistusvelvoitteet. Voit ohjata automaattisia strategioita tai soveltaa manuaalisia vaiheita tapauksiin, joissa suoritus ei pääty.
Laskennallinen pätevyys
Symboliset todistukset (ProVerif, Tamarin) takaavat turvallisuuden täydellisen kryptografian oletusten vallitessa. Laskennallisen pätevyyden lauseet (Cortier, Backes) laajentavat symboliset todistukset laskennalliseksi turvallisuudeksi, kun käytetään todistetusti turvallisia primitiivejä.
F* ja HACL*: todennetut toteutukset
F* (Microsoft Research) on todistuksiin suuntautunut ohjelmointikieli. HACL* on F*:llä kirjoitettu kryptografinen kirjasto, jonka oikeellisuudesta ja sivukanavankestävyydestä on koneellisesti varmennetut todistukset. Sitä käytetään Firefox NSS:ssä ja mbedTLS:ssä.
EasyCrypt: pelipohjaiset laskennalliset todistukset
EasyCrypt mahdollistaa kryptografisten rakenteiden täysin laskennalliset, pelipohjaiset turvallisuustodistukset — ei ainoastaan protokollien todistamista. TLS 1.3:n tietuekerros ja ChaCha20-Poly1305 on todennettu EasyCryptillä.
Käytännön vaikutus
Formaalisti varmennettu kryptografia on siirtymässä tuotantoon: NSS (Firefox) käyttää HACL*:ää, AWS käyttää s2n-tls:ää todistuksia kantavien assertioiden kanssa, ja Signal-protokolla on varmennettu ProVerifillä ja Tamarinilla. Formaalit menetelmät eivät ole enää vain akateemisia.
Tietotesti
Miten Tamarin eroaa ProVerifistä tilanteissa, joissa automaatio ei onnistu?
Oppitunnin yhteenveto
Tamarin käyttää multijoukkojen uudelleenkirjoitusta ja jälkipohjaista päättelyä vuorovaikutteisen todistusgraafisen käyttöliittymän avulla. Se käsittelee DH- ja XOR-yhtälöteorioita. Lemmat ilmaisevat salassapitoa ja autentikointia koskevat tavoitteet. Laskennallinen pätevyys yhdistää symboliset todistukset todelliseen turvallisuuteen. HACL* ja EasyCrypt laajentavat verifioinnin toteutuksiin ja kryptografisiin rakenteisiin.
Opi Cryptology Academy tekoälytuutorin avulla — ilmaiseksi
Kirjoita ja suorita oikeaa koodia selaimessa, saa välitöntä apua tekoälytuutorilta ympäri vuorokauden ja jatka siitä, mihin jäit, verkossa tai sovelluksessa.
- Kurssit
- 67
- Oppitunnit
- 261
Usein kysytyt kysymykset
Onko oppitunti ”Tamarin ja laskennalliset todistukset” ilmainen?
Kyllä – oppitunnin ”Tamarin ja laskennalliset todistukset” koko tekstin voi lukea täällä verkossa ilmaiseksi. Jos haluat harjoitella interaktiivisesti sisäänrakennetulla koodieditorilla ja ympäri vuorokauden käytettävissä olevan tekoälytuutorin avulla sekä avata koko Cryptology Academy-kurssin, päivitä CoddyKit PROhon. Cryptology Academy-kurssilla on yhteensä 4 oppituntia.
Mitä opin oppitunnilla ”Tamarin ja laskennalliset todistukset”?
Käyttäkää Tamarin-proveria multiset rewriting -menetelmään ja jälkipohjaiseen varmennukseen. Harjoittelet Cryptology Academy-aihetta koodilla, jonka suoritat suoraan selaimessa. Ympäri vuorokauden käytettävissä oleva tekoälytuutori vastaa kysymyksiisi oppitunnin aikana.
Tarvitsenko kokemusta aloittaakseni Cryptology Academy-opiskelun?
Aiempi kokemus ei ole tarpeen. CoddyKitin Cryptology Academy-oppimispolku sopii vasta-alkajista edistyneisiin, joten voit aloittaa tästä tai alusta ja edetä omaan tahtiisi. Tämä on oppitunti 4/4.
Kuinka kauan ”Tamarin ja laskennalliset todistukset”-oppitunnin suorittaminen kestää?
Useimmat CoddyKitin oppitunnit kestävät noin 5–10 minuuttia. Jokainen oppitunti on lyhyt ja interaktiivinen, joten edistyt tasaisesti ja voit jatkaa siitä, mihin jäit – sekä verkossa että sovelluksessa.
Voinko kirjoittaa ja suorittaa koodia tällä Cryptology Academy-oppitunnilla?
Kyllä. Jokainen Cryptology Academy-oppitunti sisältää sisäänrakennetun koodieditorin, joten voit kirjoittaa ja suorittaa oikeaa koodia suoraan selaimessa ja saada välitöntä palautetta tekoälyltä – paikallista asennusta ei tarvita.
Kaikki tämän kurssin oppitunnit
- Miksi epämuodolliset todistukset eivät riitä
- Dolev–Yao-hyökkääjämalli ja symbolinen kryptografia
- ProVerif: automaattinen protokollien varmennus
- Tamarin ja laskennalliset todistukset