Discussion: Formalizing the Privacy Matrix for Security Analysis

[coinstudent2048]

We need to have a formalized version of the privacy matrix (pp. 3-4) for security analysis. So far, it is informal. For now, I don't know how to do this yet, but I already envision a master theorem like as follows:

If (<proof type 1> satisfies <insert security models properties here> and <Seraphis conditions for it>) and (<proof type 2> satisfies <insert security models properties here> and <Seraphis conditions for it>) and ..., then the resulting Seraphis instance satisfies the privacy matrix.

Being an abstraction, we do not need to focus on specific proof systems: we just assume satisfaction of security models properties.

Expected to not be part of security analysis: features akin to multisig-friendliness, etc.

[UkoeHB]

I believe the CryptoNote whitepaper, RingCT, Triptych, and perhaps others, have explored a formal 'big picture' privacy matrix to some extent.

[coinstudent2048]

@UkoeHB Thanks! I will study the security properties in those papers (+ more I found) so that I can just use them (if appropriate) or at least 'derive' variants. I imagine the formal privacy matrix as also a set of security properties anyways.

...:thinking:

[coinstudent2048]

@UkoeHB Minor comments on notation (completely unrelated to this issue):

• I suggest to remove asterisks (*) in multiplication.
• Putting 1/x in "notations" section (as modular inverse).
• The "without exponents" thing is usually called "Additive notation".
• Typo: Membership proofs -> # 2 -> a_{i, 2} G_2 should be a_{1, 2} H_2.

EDIT: Omniring paper has (almost?) exactly what we need! In Section 3 they defined 3 security properties of RingCT: balance, privacy, and non-slanderability, aside from the usual correctness. They defined more in the Appendix B. In Section 4.3 "Analysis" they have theorems like my envisioned "master" theorem. Sweet! :cupcake:

Though the math looks like a big mess to me right now, so I need careful reading...

[UkoeHB]

Re: Notation

Thanks! I have been using asterisks * to improve visual clarity for ugly scalar multiplications.

[UkoeHB]

@coinstudent2048 I updated the Notation section with your suggestions, let me know if I am going in the right direction!

[coinstudent2048]

@UkoeHB asterisks is now alright, as long as there is now clarification, although I still prefer no asterisks. I am now starting formulating security properties based on formalizations in Omniring paper. It will likely take a while before I will put something in my writeups repo.

Then I will suggest further in writing style...

In any case if this would be submitted in iacr, then afaik there is a required template (which looks like the Triptych paper). (See below reply)

[UkoeHB]

@coinstudent2048 IACR has very limited requirements for submission.

[coinstudent2048]

Update: I have not yet formulated the security properties for Seraphis as a whole, but I have security properties of individual components:

• Membership proofs / Ring signature: Correctness, Unforgeability, and Anonimity (found on Triptych paper). The part "The proving system should be considered unusable if" is very similar (if not the same) to Anonimity! From Triptych,

  Anonymity requires that as long as a ring contains at least two members that have not been corrupted, an adversary can do no better than guessing at determining the signer of an honest signature.

• Ownership and unspentness proofs: (Honest verifier) ZK Proof of Knowledge. Schnorr-like proofs satisfy this.

• CT / Peterson Commitment: Perfectly hiding, Computationally binding (of course).

• Range proof: (Honest verifier) ZK Proof of Knowledge. Bulletproofs+ satisfies this.

Again, since Seraphis is an abstraction, the security properties above are assumptions. Now I need to formalize Seraphis as a whole (e.g. tuple of algorithms), so that I can properly formalize our security properties. Hope I am not delayed...

Lastly, more suggestions on notation and format:

• You can use |S| instead of size(S) for the cardinality of S, although I do not know if this notation is common outside set theory, combinatorics, and related fields.
• In membership proofs section, tuple (A, B) instead of tuple {A, B} (confused for set notation), although maybe {A, B} is still fine, I don't know.
• For the "smaller" abstract format, use \begin{abstract} and \end{abstract}.
• Remove the question in the intro. Simply starting with "A p2p (peer-to-peer) electronic cash system is a monetary system..." is just fine (at least for me).
• In notations section, 'denoted like' --> 'written as' or 'denoted by' (?) (I am not a native speaker; I am quite confused by what 'denote' means).

[UkoeHB]

Thanks! I updated with several of your suggestions.

Remove the question in the intro. Simply starting with "A p2p (peer-to-peer) electronic cash system is a monetary system..." is just fine (at least for me).

I will leave this for now. I think it helps set the right pacing/cadence for this section.

In notations section, 'denoted like' --> 'written as' or 'denoted by' (?) (I am not a native speaker; I am quite confused by what 'denote' means).

'Denoted' means 'how the concept is symbolized'. I will update that part to be more clear in the next draft.

Regarding Seraphis as a whole, I refactored the main section to be agnostic to the generators chosen. Please take a look through and let me know what you think (I also moved some implementation details to later sections).

[coinstudent2048]

@UkoeHB The consistent C <-> H and K <-> G for group elements is nice!

I found the square brackets for tuple quite weird. The use of parenthesis for tuples makes it consistent with multivariable function notation f(x,y,z). However, leave this for now because tuple notation is not consistent from paper to paper (others use angle brackets like <x,y,z>) :confounded: . Math notation can be messy.

Btw, Lelantus Spark has preprint now: https://firo.org/blog/assets/Lelantus_Spark_230821.pdf . They are also working on protocol security proofs, similar to what I am trying to do right now.

[UkoeHB]

I found the square brackets for tuple quite weird. The use of parenthesis for tuples makes it consistent with multivariable function notation f(x,y,z). However, leave this for now because tuple notation is not consistent from paper to paper (others use angle brackets like <x,y,z>) 😖 . Math notation can be messy.

I decided not to go with parentheses because the paper already has a lot of parentheses. In terms of 'quality of reading', it is better to mix things up sometimes. Also, it is better to avoid using parentheses for math in the middle of text because it can be confusing whether you are describing a tuple or just adding parenthesized text (like this :p).

Btw, Lelantus Spark has preprint now: https://firo.org/blog/assets/Lelantus_Spark_230821.pdf . They are also working on protocol security proofs, similar to what I am trying to do right now.

Yep I decided to generalize Seraphis like this so Spark qualifies as an instantiation of Seraphis :). If you read closely, you will see they satisfy all of the Seraphis proof requirements and e-note/e-note-image structures.

[coinstudent2048]

If you read closely, you will see they satisfy all of the Seraphis proof requirements and e-note/e-note-image structures.

Yep, I see. This makes my analysis/result more interesting!

Maybe put the notation section before public parameters, and remove specific objects. Something like this:

• We use capital letters like G, H for group elements, and small letters like k,t,a for scalar field elements. We use additive notation for group operations, which means that the binary group operation is denoted G+H, and no exponent blablabla. Also, xP or xP for scalar multiplication blablabla... Lastly, (1/x)P modular multiplicative inverse blablabla...
• We denote a tuple of objects like this: [Obj_1,Obj_2,Obj_3,...]. However, we still indicate that it is a tuple to prevent confusion with interval notation like [0,1].

This is so that readers are aware of specialized notation.

[UkoeHB]

Maybe put the notation section before public parameters, and remove specific objects.

I updated the notation section again. It seems useful to describe specific points in the public parameters section, but I am open to being persuaded these need to move to other sections.

I also added an appendix for a proof structure that satisfies the Seraphis ownership/unspentness requirements. It probably needs a lot of beating to get it in shape.

[coinstudent2048]

No, It's fine to describe specific objects in the public parameters. In my suggestion for the notation section to be moved, there are no specific objects, just the words "group elements" and "scalars". That's what I mean by "removing specific objects". Sorry for not being clear. I also suggest moving the notation because the public parameter section already uses the tuple notation.

For specific proving systems, I am sorry I will do the overall security analysis first. I'll just say that as long as it is "Schnorr-like", I expect Honest Verifier ZK (I just knew :sparkles: how to prove something like this) :D.

[coinstudent2048]

@UkoeHB Is it possible to have a generalization for "Information recovery" (Section 4.6)? I am thinking of plain ECIES (basically Diffie-Hellman + Symmetric Encryption). What do you think?

I need this to 'wrap up' everything. I actually find defining security properties more difficult than proving them.

[UkoeHB]

@coinstudent2048 Ok I will see what I can do.

[UkoeHB]

Added Section 3.8 for generalized information recovery.

[coinstudent2048]

Looks good! Now the 'plain' Seraphis looks complete to me as transaction protocol. I can now start a writeup :writing_hand: . I'll also do proofing on specific instances, but that's another writeup.

I'll update here for progress and once I release the writeup.

[coinstudent2048]

I am sorry I was busy last few days. This 'business' of mine would end tomorrow; I am not yet done there. After all those, I'll have more time to continue the analysis.

Re Section 4.2 "Amount Balancing": If the verifier would check if Sum C'_j == Sum C_t, then the verifier would now know Sum C_t and hence can attempt to find each C_t for every new rings? Are we relying on ring sizes and number of new e-notes here?

Lastly, expect that my early results would be for a bit more "specific" instance of Seraphis (similar to Section 4 instead of Section 3).

[UkoeHB]

Re Section 4.2 "Amount Balancing": If the verifier would check if Sum C'_j == Sum C_t, then the verifier would now know Sum C_t and hence can attempt to find each C_t for every new rings? Are we relying on ring sizes and number of new e-notes here?

I'm not sure what you mean. C_t are the new e-notes created by the transaction and C'_j are the masked commitments in e-note-images. Are you mixing up C_t and C_{\pi, j}?

[coinstudent2048]

Oh, I think I get it. Let's say A sends to B sends to someone else. A constructs C'_j and C_t (among other things) for B. Then, B constructs the ring (containing C_t) when he will spend it (of course, the other elements in the ring are also "potential spends"). Is this correct?

I gonna leave now... I'm sorry I'm focusing on something else for today.

[UkoeHB]

Yep that's right :)

[coinstudent2048]

OK another useless comment: I'm back! I need a few more rests, but lots of free time for now :smile:

[coinstudent2048]

Update: There is now seraphis* in my writeups. Highly incomplete, and may have wrong parts somewhere. I also base my understanding from xmrchain. I wrote in my preferred notation (for now).

On reading proving system relations: {(statement; witness): predicate}. Statements are exposed to the verifier, while witness is the hidden part to verifier and hence known only by prover.

[UkoeHB]

Sweet :)

I am still plugging away at tx protocol mockups... Had to take a detour the past couple days to rethink my architecture design.

[coinstudent2048]

Update: I am now "formalizing" Seraphis security properties. I am basing on the informal descriptions from Section 3 of Omniring paper. As I commented earlier above, the properties are balance, privacy, and non-slanderability (there another one: unforgeability, but apparently balance and non-slanderability already implies this), aside from the usual correctness.

So far, I only have concrete ideas for correctness (it's trivial), and privacy. Here's the rough idea for the privacy game between a PPT adversary A and challenger:

• A picks two different senders S0 and S1 (of course only knowing their public keys), two different receivers R0 and R1 (only knowing their public keys), and two different amounts a0 and a1. A also picks s-2 (where s is the anon set) e-notes, collected as S_corr, that are guaranteed to not be owned by both S0 and S1 (these are the corrupt ring members). A then sends all of those to the challenger.
• The challenger randomly chooses a bit b <--_R {0,1}. If b=0, then the challenger instructs S0 to use S_corr for ring members and to send a0 coins to R0. Else if b=1, then the challenger instructs sender S1 to use S_corr for ring members and to send a1 coins to R1. For both cases, the sender sends back the complete transaction T_comp to the challenger, which the challenger would send back to A.
• A chooses a bit b' \in {0,1}. If Pr[b' = b] = (1/2) + negl(\lambda), then Seraphis is private.

I found a rule-of-thumb for defining security properties: make sure that the adversary A picks all the "public data" as much as possible. I am actually confident about the privacy property above, because I think there's no more "public data" to be picked by adversary. Of course, peer review is needed.

All that being said, I found out that formalizing security properties can be quite tricky.

On the other hand, I already see that proving those properties is easier, thanks to Seraphis being an abstraction.

[coinstudent2048]

OK for the other properties:

• Balance is actually two conditions:
  • Witness extraction: if the sender provides a finite (but small) number of identical transactions, just different blinding factors (via "rewinding time"), then anyone can extract all the sender's private stuff (e.g. all private keys, hidden amounts, etc). This proves that the sender REALLY owns the e-notes.
  • Both the probability that a malicious sender can change the committed amount in Petersen commitment and the probability of breaking linking tag uniqueness (:smile:) is negligible.

The idea behind Balance property is that a malicious sender should not be able to create e-notes or make amounts "out of thin air". Balance property is quite complicated, and needs a lot of polishing.

• For Non-slanderability, the adversary is given a sender public addresses S and all the e-notes S owns. Of course the adversary also gets a receiver public addresses to send amounts to. Then, if Pr[the adversary will produce a complete tx with S as sender that is verified as correct] < negl(lambda), then Seraphis is non-slanderable.

Yey the properties are complete. I still need help for verifying if these definitions correctly correspond to the Omniring.

[UkoeHB]

Yey the properties are complete.

Great! :) Btw the Lelantus-Spark paper is on IACR if you want to check out their security model/proofs.

I still need help for verifying if these definitions correctly correspond to the Omniring.

There is an MRL meeting today at 1700 UTC if you want to look for help from someone qualified in this area.