/* IMPORTANT: run this with --diff! * * tamarin-prover --diff --prove ex10-observational-equivalence.spthy * * See also Tamarin's manual ยง7 (Property Specification). * * Note that Tamarin automatically generates a new lemma to test observational * equivalence. */ theory ObservationalEquivalence begin builtins: asymmetric-encryption // The usual PKI rule RegisterPublicKey: [ Fr(~sk) ] --> [ !Sk($X, ~sk), !Pk($X, pk(~sk)), Out(pk(~sk)) ] // Choose two fresh values a and b and reveal one of it. // Encrypt either the first or the second fresh value. rule ObservationalEquivalence_1: /* * Tamarin has a special diff() operator to model observational equivalence. * Think of diff(x,y) as a non-deterministic choice between x and y. */ let msg = aenc(diff(~a,~b), pkX) in [ !Pk(X, pkX), Fr(~a), Fr(~b) ] --[ Secret(~b) ]-> /* * Ideally, we do not want the attacker to be able to distinguish whether * a or b was encrypted. If a is sent to the network, however, the attacker * can apply this strategy: * * 1. Encrypt a with pkX * 2. Compare the encrypted message with msg. * * If the two encrypted messages are equal, then the encrypted message was a; * otherwise b was encrypted. So, the attacker can gain information about * an encrypted message even if the attacker is not able to decrypt it. * This works because the encryption function is deterministic: see Example 11 * for a model using probabilistic encryption. * * If a is /not/ sent out, then observational equivalence holds (try!). */ [ Out(~a), Out(msg) ] // [ Out(msg) ] lemma b_is_secret: " /* The intruder cannot know which value was encrypted: */ All x #i. ( /* ~b is claimed secret implies... */ Secret(x) @ #i ==> /* ...the adversary does not learn ~b */ not (Ex #j. K(x) @ #j) ) " end