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

Thanks for your time :)

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 gpvs 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: May 01 2024 at 20:18 UTC