Sto studiando su TOR . Ho bisogno di verificare formalmente che i protocolli coinvolti forniscano l'anonimato. Tuttavia, non sono riuscito a trovare un formalismo adatto all'anonimato. Se esiste qualche formulazione / proprietà che denoti la privacy? Il tuo aiuto è apprezzato.
Una prova formale può essere fatta solo contro un specifica formale . In altre parole: non puoi provare matematicamente che un software corrisponde a un comportamento se non sei in grado di definire matematicamente questo comportamento.
Ho seri dubbi sul fatto che un concetto generale come "anonimato" o "privacy" possa essere formalmente specificato, e quindi che possano essere dimostrati formalmente in qualsiasi modo.
Nella migliore delle ipotesi, potresti dimostrare formalmente che alcuni sottoinsiemi delle caratteristiche tecniche di Tor funzionano come progettato, ma non che questo design soddisfi qualsiasi obiettivo di privacy o anonimato.
C'è stato abbastanza lavoro sull'anonimato nei protocolli crittografici. Gli approcci a questo problema sono basati su vari modelli e tecniche di dimostrazione, ad esempio, teorico-informativo (chiamato anche sicurezza semantica), teoria della complessità e metodi formali. Recentemente, la sicurezza del TOR è stata formalmente dimostrata nel modello di composizione universale (UC). Puoi dare un'occhiata a questo documento "AnoA: Un quadro per l'analisi dei protocolli di comunicazione anonimi" di Michael Backes e altri. Si noti che la nozione di anonimato in questo articolo è piuttosto debole in quanto non considera più cicli di protocollo. Secondo me, esiste un'altra definizione che cattura meglio l'anonimato che si basa sulla privacy differenziale . Questo potrebbe essere l'approccio giusto per cui dovresti andare.