tamarin-prover/tamarin-proverStrumento di verifica simbolica per protocolli di sicurezza che utilizza la riscrittura di multiset e la risoluzione di vincoli per dimostrare proprietà di segretezza, autenticazione ed equivalenza.
Questo README descrive l'organizzazione del repository del prover Tamarin per la verifica dei protocolli di sicurezza. Il suo pubblico previsto è costituito da utenti interessati e futuri sviluppatori del prover Tamarin. Per le istruzioni di installazione e utilizzo del prover Tamarin, consultare il capitolo 2 del manuale: https://tamarin-prover.github.io/manual/master/book/002_installation.html
Consultare le istruzioni per i contributi per istruzioni su come sviluppare, testare e rilasciare modifiche al codice sorgente del prover Tamarin.
Utilizziamo numeri di versione con quattro componenti.
Garantiamo che l'interfaccia esterna di una versione del prover Tamarin sia retrocompatibile con l'interfaccia esterna di tutte le versioni che concordano sul numero di versione principale e secondaria.
Annunciamo tutte le versioni del prover Tamarin su: http://tamarin-prover.github.io
Il manuale è disponibile in formato PDF o HTML all'indirizzo https://tamarin-prover.github.io/manual/index.html
È possibile utilizzare il nostro output grafico sperimentale migliorato che può essere utile per grafi molto grandi che possono essere creati per protocolli complessi. Per abilitare questa funzionalità, leggere le istruzioni sui grafi migliorati.
Il progetto contiene il supporto per l'evidenziazione della sintassi spthy e il supporto nella directory etc. Questo include il supporto per Sublime Text, VIM e Notepad++.
Gli strumenti esterni possono utilizzare la grammatica Tree-sitter nella directory tree-sitter/.
Tutti i modelli di protocollo di esempio si trovano nella directory
./examples/
Tutti i modelli che consideriamo stabili
fanno parte di ogni installazione del prover Tamarin. Consultare
tamarin-prover.cabal per l'elenco dei protocolli installati. Utilizziamo le
seguenti sottodirectory per organizzare i modelli.
accountability/ casi di studio che utilizzano l'implementazione di accountability presentata nel
paper "Verifying Accountability for Unbounded Sets of Participants"
csf12/ i casi di studio AKE dal nostro paper CSF'12.
classic/ protocolli di sicurezza classici come quelli di
[SPORE](http://www.lsv.ens-cachan.fr/Software/spore/table.html)
loops/ esperimenti per testare loop-invariants e protocolli con
stato non monotono
related_work/ esempi da lavori correlati su protocolli con loop o
stato non monotono
experiments/ tutti gli altri esperimenti
ake/ altri esempi AKE tra cui protocolli KE di gruppo basati su ID e tripartiti
basati su bilinear pairing
features/ modelli (piccoli) che dimostrano una data funzionalità
ccs15/ i casi di studio di equivalenza osservazionale dal nostro paper CCS'15
csf-18/ i casi di studio XOR dal paper CSF'18
Sentitevi liberi di aggiungere altre sottodirectory e descriverle qui.
In generale, cerchiamo di usare nomi descrittivi per i file contenenti i modelli. Inoltre documentiamo tutti i nostri risultati come commenti nel modello di protocollo. Inoltre, utilizziamo il seguente header in tutti i file per rendere più esplicito il loro contesto.
/*
Protocol: Example
Modeler: Simon Meier, Benedikt Schmidt
Date: January 2012
Status: working
Description of protocol.
*/