new Ctxt : bool in new Key : bool in
In our simplest example, Alice receives a Boolean message, encodes it by xor-ing it with a randomly generated Boolean, and leaks the encoding to the adversary. We show that this is equal to leaking a randomly generated ciphertext.
Formally, our signature consists of two symbols: xor : Bool * Bool -> Bool for the Boolean sum, and flip : unit ->> Bool for the uniform distribution on Booleans. If you hover their names below, you can see their typing.
Our single axiom, called flipInvariantXorFixed, states that flip is invariant under xor-ing with a fixed Boolean. You can see it by hovering the axiom name in the proof below.
We now start presenting the protocols in parallel. On the left column we show the real protocol. Firstly, Alice generates a random Boolean key on a channel Key. It then encodes it by xor-ing it with a randomly generated Boolean in the channel Ctxt, and leaks the encoding to the adversary in LeakCtxtAliceAdv. Each of these is depicted as a cell and the parallel composition operator is omitted. We declare the Key and Ctxt channels as internal using new so that the outside context cannot read them.
We will prove that the real protocol is indistinguishable from the ideal protocol composed with a simulator sim. The ideal functionality is that upon receiving the input message, the ideal functionality generates a random ciphertext on an internal channel Ctxt and leaks its value to the adversary in a channel LeakCtxtIdAdv. The simulator mediates between the two leakage channels LeakCtxtIdAdv and LeakCtxtAliceAdv by forwarding the former to the latter. On the right column below we have the composition of ideal with sim followed by making the communication between the two along the channel LeakCtxtIdAdv internal using new.
new Ctxt : bool in new Key : bool in
new LeakCtxtIdAdv : bool in
(Key ::= samp flipdistribution flip : unit -> bool (()) )
(Ctxt ::= m : bool <- read In ; k : bool <- read Key ; return xorfunction xor : bool * bool -> bool((m, k)) )
(Ctxt ::= m : bool <- read In ; samp flipdistribution flip : unit -> bool (()) )
(LeakCtxtIdAdv ::=
c : bool <- read Ctxt ;
return c)
(LeakCtxtAliceAdv ::=
c : bool <- read Ctxt ;
return c)
(LeakCtxtAliceAdv ::=
c : bool <- read LeakCtxtIdAdv ;
return c)
We now simplify both protocols so that they have the same internal structure.
On the left-hand side, we fold the internal channel Key into the channel Ctxt. Then we fold the internal channel Ctxt into the channel LeakCtxtAliceAdv, and finally we can apply the axiom.
On the right-hand side, we fold the internal channel LeakCtxtIdAdv into the channel LeakCtxtAliceAdv, then fold the internal channel Ctxt into the channel LeakCtxtAliceAdv. We notice that we obtain the same result as we did on the left-hand side, so we can connect the two proofs using symmetry.
The next step is strictly syntactic: the IPDL prover lifts all hidden channel declarations to the top level so by restructure we check that we have obtained the same protocol as we did by doing the lifting for idealPlusSim. This allows us to check that we have indeed obtained the desired protocol idealPlusSim, and the proof concludes.