Intellectual Property
Each area below is a design we have modelled in software and checked there, not in shipped equipment. The table names the tools applied to each; it does not give the outcome of each check. The area names are the titles of the drafted designs, not results.
Terms used in the table
- A key exchange or sign-in is how a device and an access point agree on keys; anti-clogging means turning away floods of fake sign-in attempts; a transcript is the record of messages exchanged during sign-in; roaming is moving between access points.
- TLC, the checker for TLA+ models, explores every reachable state of a finite, bounded model; Z3 is a solver that checks whether stated conditions can all hold; bounded model checking explores a design up to a fixed number of steps; Lean 4 is a proof assistant.
- An attack matrix is a set of known attacks replayed against the design; the Linux Wi-Fi simulator runs real Wi-Fi software against simulated radios.
| Area | How it was checked |
|---|---|
| Designs for quantum-safe Wi-Fi sign-in, handover and redundant-path Ethernet, checked in software models (no hardware, 5G or data-centre work is shown here) | Lean 4 proofs, explicit-state model checking |
| Post-quantum Wi-Fi key-management safety envelope, with a machine-checked bound on the memory that admitting new sign-ins can use | Lean 4, TLA+ model checking (TLC) |
| Transition-mode downgrade firewall for post-quantum Wi-Fi | reproduced attack matrix; Linux Wi-Fi simulator captures |
| Retransmission-safe key-install gate (install once per install ID) | bounded model checking; Linux Wi-Fi simulator captures (naive reinstall vs repaired) |
| Fragmentation-safe post-quantum transcript root | reproduced attack matrix; Linux Wi-Fi simulator captures (tampered fragment accepted vs aborted) |
| Adaptive post-quantum anti-clogging gate | TLA+ model checking (TLC) |
| Post-quantum fast-roaming continuity epoch | TLA+ model checking (TLC) |
| Transcript-bound anti-clogging puzzle | TLA+ model checking (TLC); reproduced attack matrix |
| Wi-Fi integration of a post-quantum password-authenticated key exchange | TLA+ model checking (TLC); reproduced attack matrix (the exchange primitive itself is prior art) |
| Multi-link post-quantum per-link key hierarchy | TLA+ model checking (TLC), Z3; attack matrix; Linux Wi-Fi simulator captures |
| Pre-association beacon and management-frame post-quantum authenticity | TLA+ model checking (TLC), Z3; attack matrix; Linux Wi-Fi simulator captures |
| Device-class and battery-aware policy binding to the handshake transcript | TLC model checking, Z3; attack matrix |