/* IMPORTANT: run this with --diff!
*
* tamarin-prover --diff --prove ex11-observational-equivalence-probabilistic-encryption.spthy
*
* See also Tamarin's manual ยง7 (Property Specification).
*
* Note that Tamarin automatically generates a new lemma to test observational
* equivalence.
*/
theory ObservationalEquivalence
begin
/*
* The following is the simplest model of probabilistic encryption. The
* encryption function has a third parameter r, which abstractly models the
* randomness of the encryption algorithm. Decryption is still deterministic,
* of course!
*/
functions: penc/3, pdec/2, pk/1
equations: pdec(penc(m, pk(k), r), k) = m
// The usual PKI
rule RegisterPublicKey:
[ Fr(~sk) ]
-->
[
!Sk($X, ~sk),
!Pk($X, pk(~sk)),
Out(pk(~sk))
]
/*
* This is the same rule as in Example 10, except that we now use
* probabilistic encryption instead of deterministic encryption. This
* prevents the adversary to learn ~b, even if ~a is sent to the adversary.
*/
rule ObservationalEquivalence_2:
let msg = penc(diff(~a, ~b), pkX, ~r)
in
[ !Pk(X, pkX), Fr(~a), Fr(~b), Fr(~r) ]
--[ Indistinguishable(~b) ]->
[ Out(pkX), Out(~a), Out(msg) ]
// Let's verify that!
lemma b_is_secret_bis:
" /* The intruder cannot know which value was encrypted: */
All x #i. (
/* ~b is claimed secret implies... */
Indistinguishable(x) @ #i ==>
/* ...the adversary does not know ~b */
not (Ex #j. K(x) @ #j)
)
"
end