/* 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