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:

- an indexed name
`s0(i)`

used to initialize the mutable state`s`

; - a name
`m`

used to represent a fresh random message.

mutable s (i:index) : message = s0(i).

name m : message. system null. System before processing:

null

System after processing:

null

System default registered with actions (init).

In this file, our goal is to prove a secrecy property regardless of any specific protocol. This is why we declare an empty system.

global goal [default/left,default/left] secrecy (i:index,tau,tau':timestamp):[happens(pred(tau))]

-> equiv(frame@tau, diff(s(i)@tau',m))

-> [input@tau <> s(i)@tau']. Goal secrecy :

forall i:index,tau,tau':timestamp,

[happens(pred(tau))] ->

equiv(frame@tau, diff(s(i)@tau', m)) -> [input@tau <> s(i)@tau']

The following secrecy property is expressed by a global meta-logic formula. It states that, if the values stored in the memory cell `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']`

).

Note that `happens(pred(tau))`

is needed for the proof, and actually implies `happens(tau)`

.

Note that this global meta-logic formula is defined w.r.t. the same system (`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.

Systems: left:default/left, right:default/left (same for equivalences)

Variables: i:index,tau,tau':timestamp

----------------------------------------

[happens(pred(tau))] ->

equiv(frame@tau, diff(s(i)@tau', m)) -> [input@tau <> s(i)@tau']

The high-level idea of this proof is to use the strong secrecy hypothesis to prove the weak secrecy, relying on the `rewrite equiv`

tactic which allows to derive a reachability judgement from an equivalence judgement.

[goal> Focused goal (1/1):

System: left:default/left, right:default/left (same for equivalences)

Variables: i:index,tau,tau':timestamp

H: equiv(frame@tau, diff(s(i)@tau', m))

Hap: [happens(pred(tau))]

----------------------------------------

input@tau <> s(i)@tau'

We start by introducing the hypotheses.

rewrite equiv H. [> Line 57: (rewrite equiv ...)[goal> Focused goal (1/1):

System: left:default/left, right:default/left (same for equivalences)

Variables: i:index,tau,tau':timestamp

H: equiv(frame@tau, diff(s(i)@tau', m))

Hap: [happens(pred(tau))]

----------------------------------------

input@tau <> m

Here, we use the `rewrite equiv`

tactic to rewrite the conclusion of the goal: all occurrences of left elements from `H`

are replaced by their corresponding right elements.

In this case, the tactic allows to replace `s(i)@tau'`

by the name `m`

.

[goal> Focused goal (1/1):

System: left:default/left, right:default/left (same for equivalences)

Variables: i:index,tau,tau':timestamp

H: equiv(frame@tau, diff(s(i)@tau', m))

H': input@tau = m

Hap: [happens(pred(tau))]

----------------------------------------

false

It remains now to show that the attacker cannot deduce a fresh name, using the `fresh`

tactic.

[goal> Goal secrecy is proved

Qed. Exiting proof mode.

Press the left and right arrows to do and undo an instruction.

Alternatively, you can double-click on an instruction.

This zone shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.

This zone shows the output given by Squirrel.

This zone shows the output of the previous instruction, to help identifying the change caused by the instruction.

Alternatively, you can double-click on an instruction.

This zone shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.

This zone shows the output given by Squirrel.

This zone shows the output of the previous instruction, to help identifying the change caused by the instruction.

Previously: