name s0 : index->message. In this file, our goal is to prove a secrecy property regardless of any specific protocol. This is why we declare an empty system. The following secrecy property is expressed by a global meta-logic formula. It states that, if the values stored in the memory cell Note that Note that this global meta-logic formula is defined w.r.t. the same system ( The high-level idea of this proof is to use the strong secrecy hypothesis to prove the weak secrecy, relying on the We start by introducing the hypotheses. Here, we use the In this case, the tactic allows to replace It remains now to show that the attacker cannot deduce a fresh name, using the
mutable s (i:index) : message = s0(i).
name m : message.s
are strongly secret (this is expressed by the formula equiv(frame@tau, diff(s(i)@tau',m))
), then the value s(i)@tau'
is weakly secret, i.e. the attacker cannot deduce this value (this is expressed by the formula [input@tau <> s(i)@tau']
).happens(pred(tau))
is needed for the proof, and actually implies happens(tau)
.default/left
) for the left and the right projections. This is a technical restriction coming from the fact that, in the current implementation of Squirrel, global and local hypotheses cannot coexist.
[happens(pred(tau))]
-> equiv(frame@tau, diff(s(i)@tau',m))
-> [input@tau <> s(i)@tau'].rewrite equiv
tactic which allows to derive a reachability judgement from an equivalence judgement.rewrite equiv
tactic to rewrite the conclusion of the goal: all occurrences of left elements from H
are replaced by their corresponding right elements.s(i)@tau'
by the name m
.fresh
tactic.
Qed.
RUNNING EXAMPLE - secrecy
In this file we illustrate the articulation between equivalence and reachability by showing a proof of (weak) secrecy using a strong secrecy property as hypothesis.
We first declare:
s0(i)
used to initialize the mutable states
;m
used to represent a fresh random message.