add non-inclusion for proof of correct operation

Author: sebasti810

doc/book/insert-update-proofs.html

@@ -209,15 +209,22 @@ <h2 id="proof-of-update"><a class="header" href="#proof-of-update">Proof-of-Upda
 <p>The value of the leaf of the Merkle tree changes, but the index of the leaf remains the same, because it depends on the identifier (the e-mail address). We know that when the input to a hash function changes, the output also changes. Since the "value" field is part of the input of the hash of the leaf, the hash of the leaf changes accordingly.
 To proof the update, it is sufficient if we consider the old root (the cryptographic commitment) and perform a proof-of-membership before the value was updated, with the "old" leaf, so to say. The verification of the proof then involves performing a proof-of-membership of the leaf with the updated value and using this to calculate the new root and compare it with the current root.</p>
 <p>In Jellyfish Merkle trees, a new version of the tree is created with each update, enabling efficient history recording while maintaining the integrity of previous states. This versioning system ensures that updates can be tracked and verified across different states of the tree and also allows reuse of unmodified parts, which helps to increase efficiency. Accordingly, when updates are made, all nodes along the updated path are given a higher version, so the verifier needs to know which version to check the update against.</p>
-<h2 id="insert-proofs"><a class="header" href="#insert-proofs">Insert Proofs</a></h2>
-<p>The insertion proof consists</p>
+<h2 id="proof-of-insert"><a class="header" href="#proof-of-insert">Proof-of-Insert</a></h2>
 <h3 id="why-uniqueness-matters"><a class="header" href="#why-uniqueness-matters">Why uniqueness matters</a></h3>
 <blockquote>
 <p>Non-membership queries are important [...] as well; otherwise, the service's dictionary might contain more than one tuple for the <a href="mailto:bob@dom.org">bob@dom.org</a> label, allowing the service to show different tuples to different clients. [...] Alice can safely encrypt sensitive data using the public key the service returns for Bob.</p>
 </blockquote>
 <p>We briefly recall what the unique identifier means and why this is important. The email addresses in Prism act as unique identifiers and in order for the service to behave correctly, it must be ensured that no email address can be inserted twice. We imagine scenarios including when the Id <a href="mailto:bob@dom.org">bob@dom.org</a> appears twice or more in the dictionary:
 Bob adds multiple keys and also revokes some of those keys. If there are several entries for <a href="mailto:bob@dom.org">bob@dom.org</a>, scenarios are conceivable in which Bob adds a key to his first entry '<a href="mailto:bob@dom.org">bob@dom.org</a>' and later has to revoke it because the corresponding private key was stolen by Oskar. Now it could happen that the revoke operation is entered in the hashchain of the second entry '<a href="mailto:bob@dom.org">bob@dom.org</a>', in which the add operation of this key doesn't occur. Now when Alice goes through the operations in the first entry '<a href="mailto:bob@dom.org">bob@dom.org</a>', she will find that the stolen key has not been revoked and she thinks that she can perform encryption with this key. Since a requirement of Verdict is that we rule out these scenarios (as best we can), accordingly we need to make use of Proofs-of-Non-Membership for this.</p>
-<p>TODO: uniqueness still matters but should it be discussed somewhere here?</p>
+<h3 id="proof-of-correct-insert-operation"><a class="header" href="#proof-of-correct-insert-operation">Proof of correct insert operation</a></h3>
+<p>Insertion proofs consist of the inserted key, a non-membership proof of the node in the current tree, a membership proof of the new node in the JMT, and the updated merkle root.</p>
+<p>The non-inclusion proof has two variants for different cases:</p>
+<ol>
+<li>A leaf exists where the missing leaf <em>should</em> be, sharing a prefix with the key (recall that the path to the leaf is determined by the key bytes, and paths get compressed for effeciency)</li>
+<li>The node key leads to an empty subtree</li>
+</ol>
+<p>After finding the position the new node should be inserted into, it is inserted and a membership proof is created.</p>
+<p>Verification of update proofs is pretty self explanatory -- The non-inclusion proof is verified against the current state root, then the insertion is carried out locally to test that the membership proof leads to the same new root.</p>
 
                     </main>
 

doc/book/print.html

@@ -379,15 +379,22 @@ <h2 id="proof-of-update"><a class="header" href="#proof-of-update">Proof-of-Upda
 <p>The value of the leaf of the Merkle tree changes, but the index of the leaf remains the same, because it depends on the identifier (the e-mail address). We know that when the input to a hash function changes, the output also changes. Since the "value" field is part of the input of the hash of the leaf, the hash of the leaf changes accordingly.
 To proof the update, it is sufficient if we consider the old root (the cryptographic commitment) and perform a proof-of-membership before the value was updated, with the "old" leaf, so to say. The verification of the proof then involves performing a proof-of-membership of the leaf with the updated value and using this to calculate the new root and compare it with the current root.</p>
 <p>In Jellyfish Merkle trees, a new version of the tree is created with each update, enabling efficient history recording while maintaining the integrity of previous states. This versioning system ensures that updates can be tracked and verified across different states of the tree and also allows reuse of unmodified parts, which helps to increase efficiency. Accordingly, when updates are made, all nodes along the updated path are given a higher version, so the verifier needs to know which version to check the update against.</p>
-<h2 id="insert-proofs"><a class="header" href="#insert-proofs">Insert Proofs</a></h2>
-<p>The insertion proof consists</p>
+<h2 id="proof-of-insert"><a class="header" href="#proof-of-insert">Proof-of-Insert</a></h2>
 <h3 id="why-uniqueness-matters"><a class="header" href="#why-uniqueness-matters">Why uniqueness matters</a></h3>
 <blockquote>
 <p>Non-membership queries are important [...] as well; otherwise, the service's dictionary might contain more than one tuple for the <a href="mailto:bob@dom.org">bob@dom.org</a> label, allowing the service to show different tuples to different clients. [...] Alice can safely encrypt sensitive data using the public key the service returns for Bob.</p>
 </blockquote>
 <p>We briefly recall what the unique identifier means and why this is important. The email addresses in Prism act as unique identifiers and in order for the service to behave correctly, it must be ensured that no email address can be inserted twice. We imagine scenarios including when the Id <a href="mailto:bob@dom.org">bob@dom.org</a> appears twice or more in the dictionary:
 Bob adds multiple keys and also revokes some of those keys. If there are several entries for <a href="mailto:bob@dom.org">bob@dom.org</a>, scenarios are conceivable in which Bob adds a key to his first entry '<a href="mailto:bob@dom.org">bob@dom.org</a>' and later has to revoke it because the corresponding private key was stolen by Oskar. Now it could happen that the revoke operation is entered in the hashchain of the second entry '<a href="mailto:bob@dom.org">bob@dom.org</a>', in which the add operation of this key doesn't occur. Now when Alice goes through the operations in the first entry '<a href="mailto:bob@dom.org">bob@dom.org</a>', she will find that the stolen key has not been revoked and she thinks that she can perform encryption with this key. Since a requirement of Verdict is that we rule out these scenarios (as best we can), accordingly we need to make use of Proofs-of-Non-Membership for this.</p>
-<p>TODO: uniqueness still matters but should it be discussed somewhere here?</p>
+<h3 id="proof-of-correct-insert-operation"><a class="header" href="#proof-of-correct-insert-operation">Proof of correct insert operation</a></h3>
+<p>Insertion proofs consist of the inserted key, a non-membership proof of the node in the current tree, a membership proof of the new node in the JMT, and the updated merkle root.</p>
+<p>The non-inclusion proof has two variants for different cases:</p>
+<ol>
+<li>A leaf exists where the missing leaf <em>should</em> be, sharing a prefix with the key (recall that the path to the leaf is determined by the key bytes, and paths get compressed for effeciency)</li>
+<li>The node key leads to an empty subtree</li>
+</ol>
+<p>After finding the position the new node should be inserted into, it is inserted and a membership proof is created.</p>
+<p>Verification of update proofs is pretty self explanatory -- The non-inclusion proof is verified against the current state root, then the insertion is carried out locally to test that the membership proof leads to the same new root.</p>
 <div style="break-before: page; page-break-before: always;"></div><link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.16.4/dist/katex.min.css">
 <h1 id="jellyfish-merkle-proofs"><a class="header" href="#jellyfish-merkle-proofs">Jellyfish Merkle Proofs</a></h1>
 <p>Jellyfish Merkle Trees (JMT) are designed to support efficient membership and non-membership proofs, similar to Indexed Merkle Trees from Verdict. However, the proof format and verification process are optimized for better performance and smaller proof sizes.</p>

doc/book/searchindex.js

@@ -43,9 +43,7 @@ To proof the update, it is sufficient if we consider the old root (the cryptogra
 
 In Jellyfish Merkle trees, a new version of the tree is created with each update, enabling efficient history recording while maintaining the integrity of previous states. This versioning system ensures that updates can be tracked and verified across different states of the tree and also allows reuse of unmodified parts, which helps to increase efficiency. Accordingly, when updates are made, all nodes along the updated path are given a higher version, so the verifier needs to know which version to check the update against.
 
-## Insert Proofs
-
-The insertion proof consists 
+## Proof-of-Insert
 
 ### Why uniqueness matters
 
@@ -54,4 +52,15 @@ The insertion proof consists
 We briefly recall what the unique identifier means and why this is important. The email addresses in Prism act as unique identifiers and in order for the service to behave correctly, it must be ensured that no email address can be inserted twice. We imagine scenarios including when the Id <bob@dom.org> appears twice or more in the dictionary:
 Bob adds multiple keys and also revokes some of those keys. If there are several entries for <bob@dom.org>, scenarios are conceivable in which Bob adds a key to his first entry '<bob@dom.org>' and later has to revoke it because the corresponding private key was stolen by Oskar. Now it could happen that the revoke operation is entered in the hashchain of the second entry '<bob@dom.org>', in which the add operation of this key doesn't occur. Now when Alice goes through the operations in the first entry '<bob@dom.org>', she will find that the stolen key has not been revoked and she thinks that she can perform encryption with this key. Since a requirement of Verdict is that we rule out these scenarios (as best we can), accordingly we need to make use of Proofs-of-Non-Membership for this.
 
-TODO: uniqueness still matters but should it be discussed somewhere here?
+### Proof of correct insert operation
+
+Insertion proofs consist of the inserted key, a non-membership proof of the node in the current tree, a membership proof of the new node in the JMT, and the updated merkle root.
+
+The non-inclusion proof has two variants for different cases:
+
+1. A leaf exists where the missing leaf *should* be, sharing a prefix with the key (recall that the path to the leaf is determined by the key bytes, and paths get compressed for effeciency)
+2. The node key leads to an empty subtree
+
+After finding the position the new node should be inserted into, it is inserted and a membership proof is created.
+
+Verification of update proofs is pretty self explanatory -- The non-inclusion proof is verified against the current state root, then the insertion is carried out locally to test that the membership proof leads to the same new root.