NIPoK-SE Formal Verification Artifact and Reproducibility Package: ProVerif, CryptoVerif, and EasyCrypt Models, Implementation, Deployment Manifests, Benchmark Harnesses, and Raw Measurement Data

Le résumé fourni par la source

Formal-verification artifact and reproducibility package accompanying the manuscript "A Privacy-Preserving Framework Using NIPoK for End-to-End Secure Authentication in Open Banking" (submitted to the Journal of Network and Computer Applications, 2026). Version v2.0 extends the formal-verification artifact of v1 with everything needed to reproduce the performance results of the paper's Section 6: the implementation, the three-cluster Kubernetes deployment, the JMH and k6 benchmark harnesses, the raw logs behind every reported number, and the scripts that turn them into the paper's figures and tables. Contents: - formal/ — the three-tier verification development: ProVerif models (M_E2E, M_NIPoK, M_cust), the CryptoVerif model (G_auth), the EasyCrypt development (D_Sigma), and run-all.sh, which reproduces every verification result reported in Section 5 (all seven ProVerif end-to-end queries, the CryptoVerif concrete bound, and the machine-checked EasyCrypt lemmas).- implementation/ — the NIPoK prover/verifier and all baseline mechanisms (psu-auth-spi; the code measured is the code deployed), the authorization server (registration, nonce store, audit hash chain), the customer-agent with its sealed wallet and RFC 8032-style deterministic nonce derivation, and the TPP service.- deploy/ — Kubernetes manifests and Helm charts for the three trust-domain clusters, cluster-creation and CPU-allocation scripts, the netem RTT injector used by the wide-area sweep, mTLS/certificate setup (all TLS material is generated locally; none is shipped), and per-mechanism end-to-end smoke tests.- bench/micro/ — the JMH harness and the raw results behind the microbenchmark figures and tables, including the fixed-base-comb A/B run.- bench/load/ — the k6 harness driving the complete authorization journey, with the raw capacity campaigns and the injected-RTT sweep (0/20/50/100 ms, three repetitions per point).- plots/ — the figure-to-script map; every figure in Section 6 is regenerated from raw data in this package.- ENVIRONMENT.md — exact hardware and software versions, and the limits of reproduction: absolute numbers are machine-specific, while the relative invariants (knee ratios, CPU-efficiency ratio, RTT slopes, payload ratios) are what a re-run should preserve. All credentials in the tree are demonstration values for a disposable local testbed; no production secret, private key, or certificate is included. Development repository: https://github.com/buihuudong19/nipok-se-artifactLicense: MIT.

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.