SecureNode — Supplementary Repository

Supplementary material for the article:

SecureNode: A Formally Verified, Dual-Hash Authentication Protocol for IoT Peer-to-Peer Communication with Cross-Platform Energy Analysis R. Campos-Sanchez, C. Feregrino-Uribe, L. Hernandez-Martinez — INAOE, Mexico A. Penuelas-Angulo — CEIT, Basque Research and Technology Alliance (BRTA), Spain

---

Repository Structure

Repo/
├── README.md                        ← this file
├── LICENSE                          ← MIT license
├── formal_verification/
│   ├── proverif/
│   │   ├── securenode.pv            ← ProVerif model (8 security properties Q1–Q8,
│   │   │                               9 query declarations; all HOLDS)
│   │   └── result.txt               ← ProVerif output log (9 RESULT lines)
│   ├── tla/
│   │   ├── SecureNodeChain.tla      ← TLA+ specification
│   │   ├── SecureNodeChain.cfg      ← TLC model checker configuration
│   │   └── result.txt               ← TLC output (35 states, depth 14)
│   └── tamarin/
│       └── securenode_level1_failed.spthy
│                                    ← Tamarin unified model (OOM at 47 min;
│                                      kept as reference artifact; the protocol
│                                      was verified using ProVerif instead)
├── firmware/
│   ├── esp32_idf/                   ← ESP32 C/mbedTLS firmware (ESP-IDF project)
│   └── esp32_micropython/           ← ESP32 MicroPython firmware + C extensions
├── protocol_template/               ← Platform-independent Python reference impl.
├── benchmarks/
│   ├── common/                      ← Shared utilities and analysis scripts
│   ├── instruments/
│   │   └── DAQ_WIRING_GUIDE.md      ← Keithley DAQ6510 wiring and configuration
│   ├── pc/                          ← PC loopback benchmark (SHA-256 + BLAKE3)
│   ├── esp32_idf/                   ← ESP32-IDF energy + TPS benchmarks
│   ├── esp32_micropython/           ← ESP32-MP energy + TPS benchmarks
│   └── rpi4/                        ← Raspberry Pi 4 energy benchmarks
└── figures/
    ├── generate_figures.py          ← Generates all article figures from CSVs
    ├── fig_hash_crossover.pdf       ← Fig. 2: BLAKE3 vs SHA-256 crossover
    ├── fig_aes_reversal.pdf         ← Fig. 3: AES-GCM vs AES-ECB mode reversal
    ├── fig_phase_energy.pdf         ← Fig. 4: Protocol phase energy by platform
    └── fig_tps.pdf                  ← Fig. 5: Transaction throughput comparison

---

Reproducing the Formal Verification

ProVerif

proverif formal_verification/proverif/securenode.pv

Expected output: 9 RESULT ... is true lines (Q1–Q8; Q2 covers both KEY_A_priv and KEY_B_priv as separate declarations). Tested with ProVerif 2.04 on Ubuntu 22.04.

TLA+/TLC

Open formal_verification/tla/SecureNodeChain.tla in the TLA+ Toolbox or run:

tlc formal_verification/tla/SecureNodeChain.tla \
    -config formal_verification/tla/SecureNodeChain.cfg

Expected: 35 states explored, depth 14, no violations. Tested with TLC 1.8.0.

Tamarin (reference only)

formal_verification/tamarin/securenode_level1_failed.spthy is included as a reference artifact. The unified Tamarin model ran out of memory (>16 GB) after 47 minutes; the protocol properties were therefore verified using ProVerif.

---

Reproducing the Energy Benchmarks

Each platform subdirectory under benchmarks/ contains:

• README.md — step-by-step instructions for that platform
• BENCHMARK_GUIDE.md — hardware setup and DAQ6510 configuration
• energy/results/report.csv — canonical CSV result file used in the article

Hardware required: ESP32 DevKit, Raspberry Pi 4, Keithley DAQ6510 multimeter. Wiring instructions: benchmarks/instruments/DAQ_WIRING_GUIDE.md.

---

Reproducing the Figures

pip install matplotlib numpy
python figures/generate_figures.py

Output PDFs are written to figures/ (same directory as the script), overwriting the pre-generated copies already included there.

---

Citation

@misc{secureNode2026repo,
  author       = {Campos-Sanchez, R. and Feregrino-Uribe, C. and
                  Hernandez-Martinez, L. and Penuelas-Angulo, A.},
  title        = {{SecureNode} --- Supplementary Material},
  year         = {2026},
  howpublished = {\url{https://github.com/RazielCS/SecureNode}},
  note         = {ProVerif models, TLA+ specifications, benchmark scripts}
}

---

License

MIT License — see LICENSE.