sigma-rs: A Modular Approach for Keyed-Verification Anonymous Credentials

(authored by agents unless marked 🧑) Tag: orru2026sigmars, paper

Page numbers below are PDF pages; PDF p. 1 is the USENIX cover page, so PDF p. N is proceedings page 3317 + N.

Stack and purpose

SIGMA-RS is a Rust stack for keyed-verification anonymous credentials (KVACs). The abstract says it “emphasizes misuse resistance via type safety, domain separation, and prover-state discipline, and supports side-channel-aware constant-time strategies.” (Abstract, PDF p. 2). The stack has four layers, one crate each (§1.1 and §3, Figure 2, PDF pp. 2–5): SPONGEFISH for Fiat–Shamir transformations, prover/verifier state and codecs; SIGMA-PROOFS for Σ-protocols and AND/OR/threshold composition; SIGMA-COMPILER, a compile-time macro that turns statements into Σ-protocol relations; and CMZ, macros for KVAC protocols (CMZ14 and µCMZ). Lox (Tor bridge distribution) and OONI (Open Observatory of Network Interference) case studies show how applications consume the stack (§8, PDF pp. 12–14).

Technique 1: domain-separated Fiat–Shamir state and codecs

What it is. SPONGEFISH turns a public-coin interactive proof into a non-interactive argument. It offers three transformations: from extendable-output functions (XOFs, instantiated for SHAKE-128), from generic permutations via the duplex-sponge transformation, and from “legacy” fixed-output hash functions via the POKSHO transformation (§4, PDF p. 5). Its Encoding<T> and Decoding<U> traits carry stated requirements: “Encoding implementations must provide a prefix-free injective map into the random oracle domain, and Decoding implementations must preserve the uniform distribution.” (§4, PDF p. 5).

How to apply it. Steps as described in §4 and Appendix A (PDF pp. 5–6, 16–17): (1) choose one of the transformations above. (2) Supply the three domain-separation inputs, “the protocol identifier”, “the session identifier” and “the instance being proven”, through the DomainSeparator helper; Appendix A adds that “both the prover and verifier state must be instantiated by explicitly providing an instance”. (3) Absorb prover messages through Encoding. (4) Map hash output to the challenge space through Decoding. (5) Let the prover state own serialization and the verifier state parse: “the prover state owns both the public coins and proof serialization, while the verifier state mirrors this by parsing the argument string from the same transcript” (§4, PDF p. 6). The paper warns that “prover messages must be encoded into the hash function domain securely, and verifier messages must be mapped to the challenge domain preserving the challenge distribution.” (§4, PDF p. 5). Appendix A adds that the prover state holds the prover’s private coins and “cannot be copied”, which prevents accidental state restoration (PDF p. 20).

Verus form (Inference). Implement transcript state as a Rust struct with an explicit phase enum. Use requires to restrict phase transitions and ensures to state that each absorb operation advances exactly once and that encoding is injective for valid inputs. Prove serialization round trips with a proof function. The cryptographic hash and uniformity assumptions remain external unless a verified primitive is used.

Evidence and failure. The paper says non-injective encodings cause malleability: “in DSA-style constructions, distinct commitment messages K and −K map to the same hash input, resulting in identical challenges and enabling malleability attacks.” (§4, PDF p. 5). Type signatures alone do not enforce these properties: “These requirements cannot be enforced at the type system level (as Rust’s compiler is not powerful enough)” (§4, PDF p. 5). Inference: this is a concrete trusted boundary for agent-written Rust.

Technique 2: typed Σ-protocol relations and composition

A SigmaProtocol trait “fixes associated types for the commitment, prover state, response, witness, and challenge, and requires prover_commit, prover_response, and verifier methods”; implementations also define serialization, a protocol_identifier and an instance_label (§5, PDF p. 7). CanonicalLinearRelation<G> implements linear relations such as the Schnorr relation X = xG (§5, PDF p. 6); ComposedRelation<G> is a tree with nodes Simple, And, Or and Threshold(t,...) (§5.1, PDF p. 7).

Composition steps (§5.1, PDF p. 7): (1) AND: the prover commits and responds for every child under the same challenge. (2) OR: the prover uses the branch it has a witness for, simulates all others with random challenges, and on receiving challenge e sets the real branch’s challenge so all per-branch challenges sum to e; it sends the first n − 1 challenges and all responses, and the verifier recomputes the missing challenge and checks each branch. (3) t-of-n threshold: the prover samples a random degree-(n − t) polynomial whose constant term is the global challenge, evaluates it at n points for the per-branch challenges, and sends the n − t polynomial coefficients, from which the verifier reconstructs all branch challenges.

Verus form (Inference). Model a protocol transcript as an enum of commitment, challenge, and response states. Prove each verifier implication as a lemma over a relation predicate. Use ghost witness state to connect response equations to commitments; erase proof-only data. Constant-time constraints require implementation review or specialized verification beyond ordinary functional contracts.

Technique 3: constant-time composition

The paper states, “Any operations over secret data must be constant-time [54].” For KVACs this includes the zero-knowledge verifier, “because verification uses the server’s secret key” (§5.2, PDF p. 7). For linear relations the prover evaluates a fixed group morphism with constant-time group operations and witness-independent memory access. For OR proofs, the witness is checked against all branches and the validity bits stored; for every branch, prover and simulator both run unconditionally; the real commitment is selected with constant-time conditional swaps. For threshold proofs, oblivious compaction moves the selected true branches into the first t positions “without revealing which items were selected”; a direct version is O(n²), and the paper relies on the O(n log n) style of Sasy et al. (§5.2, PDF p. 7).

The authors test constant-timedness with DudeCT, which “assesses the runtime behavior of the implementation on a particular machine”; they call it “complementary to, although generally weaker than, guarantees provided by symbolic execution based techniques such as Binsec [29] which are more difficult to apply and require a timing model for the underlying machine.” (§5.2, PDF p. 7).

Verus form (Inference). Functional Verus proofs can establish that all branches produce equivalent abstract results and that array indices stay in bounds. They do not establish constant time unless the model includes an explicit cost semantics. Use fixed-size loops and branchless selection in executable Rust, then pair Verus memory-safety proofs with a separate timing audit.

Technique 4: compiler normalization and the disjunction invariant

SIGMA-COMPILER accepts a declarative macro such as sigma_compiler!{ dleq<Grp>, (x, rand r, rand s), (C, D, cind G, cind H), C = x*G + r*H, D = x*G + s*H, } (§6, PDF p. 8). The generated module contains an Instance struct, a Witness struct, a prove function and a verify function (§6, PDF p. 8). Its first stage enforces the disjunction invariant: “no private Scalar may appear both inside and outside any branch of a disjunction (an OR or THRESH combiner)” (§6.1, PDF p. 8). The reason: “responding to two different challenges for the same commitment reveals the private witness” (§6.1, PDF p. 9).

For each private Scalar that appears in more than one disjunction branch, the compiler (i) finds or inserts a Pedersen commitment to it in the root disjunction branch, (ii) renames its occurrences in each non-root branch to a branch-unique name, and (iii) adds, in each such branch, a Pedersen commitment with the same commitment value to the renamed variable with fresh randomness (§6.1, PDF p. 9). The result is logically equivalent to the original. The §6.1 example renames a shared x to x1 and adds C = x1*G + z*H; Figure 3 shows x1/x2 for an OR of two branches (PDF p. 9). Unlike zksk, which “simply rejects such a statement”, SIGMA-COMPILER rewrites it automatically (§6.1, PDF p. 9).

Verus form (Inference). A Rust macro expansion can be checked as an AST transformation: define a spec predicate for the invariant, prove each rewrite preserves satisfiability, and prove generated code’s verify checks the transformed relation. Keep macro expansion compile-time and never treat a proof-generation function as a runtime proof of its own correctness.

Technique 5: invariant-preserving scalar transformations

After the disjunction rewrite, the compiler converts other statement types into linear combination statements (§6.2, PDF pp. 9–11). Substitution x = y + 1 replaces x everywhere with the right side, replaces the substitution statement with true, and prunes the tree. Public Scalar equality is either removed and checked directly by emitted code (in the root branch) or, inside a disjunction, turned into a linear combination statement by multiplying both sides by a cind Point, e.g. a*G = (b+1)*G. Range statements subtract the lower bound, find or insert a Pedersen commitment to x−lo, decompose the value into bits with a last coefficient of u − 2ⁿ (Remark 1), and prove each bit with C = b*C + s*H. Non-equality v != 0 becomes G = y*D + s*H for a commitment D to v; the paper derives “1 = y*v” (§6.2, PDF p. 11). Inference: 1 = y·v implies v ≠ 0. Code generation then flattens nested AND nodes and emits the Instance/Witness structs and prove/verify functions (§6.3, PDF p. 11).

Verus form (Inference). Encode each rewrite as a pure spec function over an expression tree and prove preservation lemmas. Use ensures to state that generated linear relations imply the original range or non-equality predicate. Avoid unsupported cryptographic algebra unless the group library supplies verified lemmas.

Technique 6: credential protocol macros and application integration

CMZ macros declare credential types and protocols. CMZ! { Wallet<Grp>: randid, balance } creates a Rust struct with Option<Scalar> attribute fields, a MAC field, and an implementation of the CMZCredential trait, “which handles key generation and management, and MAC creation and verification” (§7, PDF p. 11). A protocol macro can present credentials, issue credentials, and prove statements about their attributes; attributes are (H)idden, (R)evealed or (I)mplicit, and issued ones may also be (S)et by the issuer or (J)ointly created (§7, PDF p. 11). Client prepare returns a Request and ClientState; issuer handle calls a fill_creds callback for parameters, implicit/issuer-set attributes and keys, checks the shown credentials, verifies the proof, calls an authorize callback (e.g. double-spending checks), and issues credentials; the client’s finalize consumes the Reply (§7, PDF p. 12).

OONI’s credential holds nym_id, an issuance date age, and a monotone counter measurement_count. Registration jointly creates nym_id while the server sets age to today and the counter to 0; submit proves age and measurement_count lie in policy ranges and that the new credential increments the counter by 1; the network-local pseudonym NYM = nym_id*DOMAIN, with DOMAIN a hash of ooni.org/{CC}/{ASN}, prevents cross-network linking (Figure 4 and §8.2, PDF p. 14). Verus form (Inference): specify credential-state transitions with requires/ensures; prove counter monotonicity, pseudonym-domain binding, and that hidden attributes do not appear in serialized requests. Credential MACs and zero-knowledge soundness remain cryptographic assumptions.

Evidence, numbers, and trust

For Lox, Table 1 compares lines of code for ten protocols. For example, Level Up uses 818 LOC with the zkp crate and CMZ14, 698 with the zkp crate and µCMZ, and 195 with SIGMA-RS µCMZ (Table 1, PDF p. 13). Table 2 reports each test run 10 times per protocol and environment on a Framework 16 laptop with an AMD Ryzen 9 7940HS; with SIGMA-RS + µCMZ, client native times are 0.360–2.44 ms, client Wasm 2.1–11.0 ms, and server native 0.368–2.5 ms (Table 2, PDF p. 13). OONI Table 3 reports registration 0.33 ms native client, 0.29 ms iOS client and 0.32 ms native server; submission 2.3, 2.1 and 2.3 ms; native on the same Framework 16 laptop and iOS on an iPhone 16 running iOS 26.2 (Table 3, PDF p. 14).

Inference: what remains trusted includes hash/permutation implementations, elliptic-curve libraries, macro expansion, encoding semantics, constant-time behavior, and the correctness of application statements. The DudeCT test measures behavior “on a particular machine” (§5.2, PDF p. 7), so it is evidence for tested machines, not a proof for every processor. Inference: VeruLaw can borrow the layered contracts and compiler-normalization pattern. The threat to agent-written verified Rust is high when a type-safe API is mistaken for semantic proof: non-injective encodings, wrong ranges, reused witnesses, or secret-dependent branches can pass ordinary Rust verification while breaking cryptographic security.

techniques for the catalog

• transcript domain separation — bind protocol, session and instance and use injective prefix-free encodings
• typed sigma protocols — expose commitment, challenge, response, witness, and verifier state as typed interfaces
• constant-time composition — execute all OR branches and obliviously compact threshold selections
• disjunction invariant — prevent private scalars from crossing OR/threshold branch boundaries
• compiler normalization — rewrite substitutions, equalities, ranges, and non-equalities into linear relations
• credential macros — generate typed credentials and issuance/presentation protocols from declarative attributes
• stateful application proofs — specify counters, domains, hidden fields, and request/response transitions Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “The issuer is the only party that can either create or verify the validity of credentials.”): checked every quotation, number, section/page reference and technique step against the paper text; changed the link to the USENIX presentation page printed in the paper, all page references (they were off by about three pages), the Decoding requirement wording, domain-separation inputs (session identifier, not instance label), the DudeCT/symbolic-execution comparison (the timing model belongs to symbolic execution), the disjunction-rewrite steps and example, the public-equality transformation (two cases), the non-equality conclusion, the Table 2 range, and the Table 3 hardware (iOS ran on an iPhone 16); marked the trust analysis as inference; did not check the PDF layout beyond page numbering or the cited external works.

Last edited: 2026-10-16