## Stream: General

### Topic: CryptHOL: proof obvious advantage difference

#### Tobias Rothmann (Jul 22 2023 at 13:00):

Hi,
I have two games defined as follows:

``````game0 = TRY do {
α::nat ← sample_uniform (order G⇩p);
x::'y ← (𝒜::nat ⇒ 'y spmf) α;
_ :: unit ← assert_spmf (a x);
return_spmf True
} ELSE return_spmf False
``````

and

``````game1 = TRY do {
α::nat ← sample_uniform (order G⇩p);
x::'y ← (𝒜::nat ⇒ 'y spmf) α;
_ :: unit ← assert_spmf (a x);
_ :: unit ← assert_spmf (b x);
return_spmf True
} ELSE return_spmf False
``````

Now I want to show that the advantage the Adversary A can have in game0 is greater-equal to the advantage it can have in game1 , which is trivially true (or at least I thought so..) as game1 literally adds one assert to game0.
However, the proof is not easy (for me).
I would greatly appreciate any help or advice in proving this thing. I already looked through the SPMF theory, but couldn't find anything, but a lot of measure lemmas, which left me clueless.

Ah one more thing, the goal looks like this:

``````spmf (game0 A) True <= spmf (game1) True
``````

#### Yong Kiam (Jul 24 2023 at 00:56):

hi Tobias, have you looked at https://eprint.iacr.org/2018/941 ?
In this case, you need to apply some form of "identical-until-bad" reasoning (see Section 3.6) -- which I do agree was a bit heavyweight when I tried it

#### Tobias Rothmann (Jul 24 2023 at 16:54):

Hi Yong,
thanks a lot for the hint. I looked at it when I started with CryptHOL, but my understanding wasn't good enough to think of it again.
But looks exactly like what I need to do, so thanks a lot! That saved definitely a lot of hours searching around :)

#### Yong Kiam (Jul 25 2023 at 00:50):

FWIW: I found it much easier to start with `spmf` only when trying this out, I'm still totally lost on `gpv`s if I have to be honest :laughing:

#### Tobias Rothmann (Jul 25 2023 at 18:23):

I can relate, even spmf is hard for me now, luckily I don't have to deal with gpv for my project :laughing:

#### Tobias Rothmann (Sep 29 2023 at 14:04):

In case someone every stumbles upon this, I managed to proof this thing without a failure-event proof.
Its the lemma "spmf_reduction" in this file:https://github.com/tobias-rothmann/KZG-Polynomial-Commitment-Scheme/blob/main/KZG_poly_bind.thy#L624

#### Manuel Eberl (Sep 29 2023 at 22:41):

I don't know anything about CryptHOL, but I'd prove this by relational reasoning, without going down all the level to computing integrals. You can insert a `_ :: unit ← assert_pmf True` in the first program at the location where the additional line in the second one is, and then you can prove `rel_spmf (=) game1 game0` compositionally because the two programs are syntactically completely equal except for that one line, and that should give you what you need.

#### Tobias Rothmann (Sep 30 2023 at 13:46):

Manuel Eberl said:

I don't know anything about CryptHOL, but I'd prove this by relational reasoning, without going down all the level to computing integrals. You can insert a `_ :: unit ← assert_pmf True` in the first program at the location where the additional line in the second one is, and then you can prove `rel_spmf (=) game1 game0` compositionally because the two programs are syntactically completely equal except for that one line, and that should give you what you need.

Ahh thanks for the hint! Didn't think of it, I'll try it out and update accordingly sometime soon. Thanks :)

Last updated: Dec 07 2023 at 08:19 UTC