feat: Rung 4 + Extended Rung 4 — TLA+/ProVerif formal models#35

Merged

cuihtlauac merged 7 commits into

mainfrom

rung4-protocol-models

Jun 11, 2026

Commits on Jun 11, 2026

feat: Rung 4 — TLA+ approval state machine + ProVerif SSH model

cuihtlauac
and
claude
committed
docs: add three Extended Rung 4 backlog items

cuihtlauac
and
claude
committed
feat: Extended Rung 4 — freshness↔replay window-sizing TLA+ model

cuihtlauac
and
claude
committed
feat: Extended Rung 4 — concurrent-handler interleaving TLA+ model

cuihtlauac
and
claude
committed
feat: Extended Rung 4 — derive SSH first-contact MITM via key-acceptance (ProVerif)

cuihtlauac
and
claude
committed
ci: refresh apt index before installing ProVerif

cuihtlauac
and
claude
committed
docs: mark the original Rung 4 ProVerif changelog entry as superseded

cuihtlauac
and
claude
committed