Research Team Status

• Names of researchers and position
  • Christopher Ellis (PhD Student)
  • Jun Yeon Won (PhD Student)
• Any new collaborations with other universities/researchers?
  • N/A

Project Goals

• Current Project Goal:
  In Q3 we broadened our formal analysis of discovery-phase security for short-range wireless protocols. Building on our Q2 work on “well-authentication” in BLE, we set out to (1) precisely characterize when pre-association identifiers can leak in realistic device configurations, (2) capture the relationship between those leaks and linkability across locations and time, and (3) validate enforceable countermeasures that still preserve operational continuity for managed deployments.
• Relation to Long-term Goal:
  These Q3 activities directly support our long-term objective of rigorous, formally verified, privacy-preserving wireless connectivity for IoT. Unifying the discovery-phase properties and the analysis toolchain across BLE and Wi-Fi strengthens our foundations for automated proofs, cross-protocol reasoning, and scalable vulnerability detection in Bluetooth-centric IoT environments.

Accomplishments

• Milestone Achievements:
  • Formal properties for discovery-phase privacy. We specified machine-checkable invariants for pre-association behavior (no identifier disclosure prior to authenticity checks; bounded reuse windows) and linked them to concrete linkability outcomes (individual and group).
  • Tooling integration. We extended our π-calculus execution engine from Q2 to generate protocol traces that feed automatic theorem provers (e.g., Tamarin) for both BLE and Wi-Fi–like discovery workflows. This lets us test privacy conditions alongside authentication and relay-resilience properties within one pipeline.
  • System design validation. We designed and validated a lightweight enforcement overlay for Wi-Fi-style deployments that performs (a) pre-transmission verification of access point beacons and (b) spatiotemporally scoped identifier rotation post-verification. We confirmed the design maintains enterprise continuity while removing the cross-site linkability condition, with negligible overhead in our experiments (details omitted here to avoid oversharing).
  • Manuscript and disclosure. We consolidated these results into a manuscript for academic peer review and initiated responsible communications with relevant stakeholders. 
• Foundational Research Contributions:
  • Clarified the source of residual linkability. We showed that deterministic, per-network identifiers create a reproducible reuse window that enables cross-location linking in realistic deployments, even when scan randomization is present.
  • Sufficient conditions to prevent discovery-phase leakage. We provided formal conditions under which pre-association verification plus scoped rotation eliminate the equality needed for cross-site linking, without breaking roaming or policy enforcement in managed domains.
  • Cross-protocol unification. We mapped these conditions back to BLE “exclusive-use” and “well-authentication” notions from Q2, giving a single set of properties and counterexample patterns that apply across BLE and Wi-Fi–like stacks.

Internal to the university (coursework/curriculum):
N/A

External to the university (transition to industry/government; patents, start-ups, software, etc.):
Once hardened, our specifications and analysis scripts can be applied in continuous assessment pipelines for managed wireless deployments (for example, to validate that discovery-phase policies meet privacy goals without disrupting operations). We anticipate sharing guidance with standards and industry groups after peer review and internal vetting.

Any acknowledgements, awards, or references in media?
No new external acknowledgements, awards, or media references this quarter.

Publications and presentations

• Add publication reference in the publications section below. An authors copy or final should be added in the report file(s) section. This is for NSA's review only.
• Optionally, upload technical presentation slides that may go into greater detail. For NSA's review only.