Research Team Status

• Names of researchers and position 
  • Christopher Ellis (PhD Student)
  • Felix Engelmann (Post-doc)
     
• Any new collaborations with other universities/researchers?
  • N/A

Project Goals

• What is the current project goal?
  • Regarding our formalization effort, the current goal is to capture the privacy implications which arise when devices communicate with expedited reconnection handshakes to previously known devices according to dynamically changing allowlists.
    We work towards a precise formulation of a trace-equivalence definition. The challenge is to build it in a way that it matches the intuitive understanding of unlinkability as well as allowing for comparison to previous formal definitions. We aim for a definition structure similar to Baelde et al. [1]. which requires all possible real-world executions to be trace-equivalent to an idealized honest scenario in which there is no linkability by design. This is usually a system in which every device only talks once.
  • Given this definition, we want to show that the three existing properties from [1] (Well-authentication, Frame opacity and No-desynchronisation) are not sufficient and then prove that our updated protocol properties are sufficient. This proof hopefully works by showing that, given our conditions, an attacker cannot distinguish between the ideal and the real world protocol.
     
• How does the current goal factor into the long-term goal of the project?
  • Current goal is the natural steps to achieve our long-term goal of the project.

Accomplishments

• Address whether project milestones were met. If milestones were not met, explain why, and what are the next steps.
  • With the new member Felix joining the group, we are making solid progress and have met the current goals. We will continue executing the plan outlined in the proposal.
     

• What is the contribution to foundational cybersecurity research? Was there something discovered or confirmed?

  •  Since the last report in January, we understood the formal modelling done in [1] and its predecessor Hirschi et al. [2] and extracted the overarching trend of expansion of scope. The more powerful the protocols become, the more complexity needs to be formalized. With this understanding, we defined a process algebra powerful enough to model allowlists. Pair and un-pair operations interact with the system configuration and change the behavior of reconnecting devices.
    This is the foundation for our current goals.

  [1] A Method for Proving Unlinkability of Stateful Protocols
  [2] A Method for Verifying Privacy-Type Properties: The Unbounded Case

   

• Impact of research
  • Internal to the university (coursework/curriculum)
    • N/A
  • External to the university (transition to industry/government (local/federal); patents, start-ups, software, etc.)
    • N/A
  • Any acknowledgements, awards, or references in media?
    • N/A

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.