Estoy estudiando sobre TOR . Necesito verificar formalmente que los protocolos involucrados proporcionen anonimato. Sin embargo, no pude encontrar un adecuado formalismo de anonimato. ¿Si existe alguna formulación / propiedad que denota privacidad? Tu ayuda es apreciada.
Una prueba formal solo se puede realizar contra una especificación formal . En otras palabras: no puede probar matemáticamente que un software coincida con un comportamiento si primero no puede definir matemáticamente este comportamiento.
Tengo serias dudas de que un concepto general como "anonimato" o "privacidad" pueda especificarse formalmente y, por lo tanto, se pueda probar formalmente de cualquier manera.
En el mejor de los casos, podría probar formalmente que algunos subconjuntos de las características técnicas de Tor funcionan según lo diseñado, pero no que estos diseños cumplan con ningún objetivo de privacidad o anonimato.
Ha habido bastante trabajo sobre el anonimato en los protocolos criptográficos. Los enfoques de este problema se basan en varios modelos y técnicas de prueba, por ejemplo, teoría de la información (también llamada seguridad semántica), teoría de la complejidad y métodos formales. Recientemente, la seguridad de TOR se demostró formalmente en el modelo de composición universal (UC). Puede echar un vistazo a este documento "AnoA: Un marco para analizar protocolos de comunicación anónimos" por Michael Backes y otros. Tenga en cuenta que la noción de anonimato en este documento es bastante débil, ya que no considera varias rondas de protocolo. En mi opinión, hay otra definición que captura mejor el anonimato que se basa en privacidad diferencial . Este podría ser el enfoque correcto al que deberías ir.