Report

Anonymity Analysis of Onion Routing in the Universally Composable Framework Joan Feigenbaum Aaron Johnson Paul Syverson Yale University U.S. Naval Research Laboratory Provable Privacy Workshop July 9, 2012 Problem ● ● ● ● ● [FJS07a] - Onion-routing I/O-automata model - Possibilistic anonymity analysis [FJS07b] - Onion-routing abstract model - Probabilistic anonymity analysis […] - How do we apply results in standard cryptographic models? [CL05] - “Onion routing” formalized with Universal Composability (UC) - No anonymity analysis [BGKM12] - Onion routing formalized with UC - Our work will provide anonymity Solution ● ● ● Formalize abstract (black-box) model of onion routing in UC framework Focus on information leaked Anonymity analysis on earlier abstract model is inherited by UC version Problem ● ● ● ● ● [FJS07a] - Onion-routing I/O-automata model - Possibilistic anonymity analysis [FJS07b] - Onion-routing abstract model - Probabilistic anonymity analysis […] - How do we apply results in standard cryptographic models? [CL05] - “Onion routing” formalized with Universal Composability (UC) - No anonymity analysis [BGKM12] - Onion routing formalized with UC - Our work will provide anonymity I/O-automata model Adversary controls relays 1 2 u 3 5 User u running client d Internet destination d 4 Onion routing relays Encrypted onion-routing hop Unencrypted onion-routing hop I/O-automata model 1 2 u 3 5 d 4 u 1 2 Main theorem: Adversary can only determine parts of a circuit it controls or is next to. I/O-automata model u v w 1. 2. 3. 4. 1 2 d 3 5 4 e f I/O-automata model u v w 1 2 d 3 5 4 1. First router compromised 2. 3. 4. e f I/O-automata model u v w 1 2 d 3 5 4 1. First router compromised 2. Last router compromised 3. 4. e f I/O-automata model u v w 1 2 d 3 5 4 1. First router compromised 2. Last router compromised 3. First and last compromised 4. e f I/O-automata model u v w 1 2 d 3 5 4 e f 1. First router compromised 2. Last router compromised 3. First and last compromised 4. Neither first nor last compromised Problem ● ● ● ● ● [FJS07a] - Onion-routing I/O-automata model - Possibilistic anonymity analysis [FJS07b] - Onion-routing abstract model - Probabilistic anonymity analysis […] - How do we apply results in standard cryptographic models? [CL05] - “Onion routing” formalized with Universal Composability (UC) - No anonymity analysis [BGKM12] - Onion routing formalized with UC - Our work will provide anonymity Black-box Abstraction u d v e w f Black-box Abstraction u d v e w f 1. Users choose a destination Black-box Abstraction u d v e w f 1. Users choose a destination 2. Some inputs are observed Black-box Abstraction u d v e w f 1. Users choose a destination 2. Some inputs are observed 3. Some outputs are observed Black-box Anonymity u d v e w f • The adversary can link observed inputs and outputs of the same user. Black-box Anonymity u d v e w f • The adversary can link observed inputs and outputs of the same user. • Any configuration consistent with these observations is indistinguishable to the adversary. Black-box Anonymity u d v e w f • The adversary can link observed inputs and outputs of the same user. • Any configuration consistent with these observations is indistinguishable to the adversary. Black-box Anonymity u d v e w f • The adversary can link observed inputs and outputs of the same user. • Any configuration consistent with these observations is indistinguishable to the adversary. Probabilistic Black-box u d v e w f Probabilistic Black-box u d v e w f pu • Each user v selects a destination from distribution pv Probabilistic Black-box u d v e w f pu • Each user v selects a destination from distribution pv • Inputs and outputs are observed independently with probability b Problem ● ● ● ● ● [FJS07a] - Onion-routing I/O-automata model - Possibilistic anonymity analysis [FJS07b] - Onion-routing abstract model - Probabilistic anonymity analysis […] - How do we apply results in standard cryptographic models? [CL05] - “Onion routing” formalized with Universal Composability (UC) - No anonymity analysis [BGKM12] - Onion routing formalized with UC - Our work will provide anonymity Problem ● ● ● ● ● [FJS07a] - Onion-routing I/O-automata model - Possibilistic anonymity analysis [FJS07b] - Onion-routing abstract model - Probabilistic anonymity analysis [FJS12] – Onion-routing UC formalization - “Free” probabilistic anonymity analysis [CL05] - “Onion routing” formalized with Universal Composability (UC) - No anonymity analysis [BGKM12] - Onion routing formalized with UC - Our work will provide anonymity Onion-Routing UC Ideal Functionality Upon receiving destination d from user U x u with probability b ø with probability 1-b y d with probability b ø with probability 1-b Send (x,y) to the adversary. FOR Black-box Model ● ● Ideal functionality FOR Environment assumptions – – ● Each user gets a destination Destination for user u chosen from distribution pu Adversary compromises a fraction b of routers before execution UC Formalization ● ● ● ● Captures necessary properties of any crytographic implementation Easy to analyze resulting information leaks Functionality is a composable primitive Anonymity results are valid in probabilistic version of I/O-automata model Anonymity Analysis of Black Box ● ● ● ● Can lower bound expected anonymity with standard approximation: b2 + (1-b2)pud Worst case for anonymity is when user acts exactly unlike or exactly like others Worst-case anonymity is typically as if √b routers compromised: b + (1-b)pud Anonymity in typical situations approaches lower bound Future Extensions ● ● ● ● Compromised links Non-uniform path selection Heterogeneous path selection Anonymity over time Problem ● ● ● ● ● [FJS07a] - Onion-routing I/O-automata model - Possibilistic anonymity analysis [FJS07b] - Onion-routing abstract model - Probabilistic anonymity analysis [FJS12] – Onion-routing UC formalization - “Free” probabilistic anonymity analysis [CL05] - “Onion routing” formalized with Universal Composability (UC) - No anonymity analysis [BGKM12] - Onion routing formalized with UC - Our work will provide anonymity [BGKM12] Ideal Functionality ● ● ● Functionality can actually send messages Needs wrapper to hide irrelevant circuit-building options Shown to UC-emulate FOR References [BGKM12] Provably Secure and Practical Onion Routing, by Michael Backes, Ian Goldberg, Aniket Kate, and Esfandiar Mohammadi, in CSF12. [CL05] A Formal Treatment of Onion Routing, by Jan Camenisch and Anna Lysyanskaya, in CRYPTO 05. [FJS07a] A Model of Onion Routing with Provable Anonymity, by Joan Feigenbaum, Aaron Johnson, and Paul Syverson, in FC07. [FJS07b] Probabilistic Analysis of Onion Routing in a Black-box Model, id., in WPES07. [FJS12] A Probabilistic Analysis of Onion Routing in a Black-box Model, id. in TISSEC (forthcoming)