arXiv subjects

Jannik Mähn

Publications and source records attributed to Jannik Mähn.

3 recordsLinked to original sources

arXiv2025

Formally-verified Security against Forgery of Remote Attestation using SSProve

Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of StateSeparating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures.

cs.CR↗

arXiv2023

Enabling Mobility-Oriented JCAS in 6G Networks: An Architecture Proposal

Sensing plays a crucial role in autonomous and assisted vehicular driving, as well as in the operation of autonomous drones. The traditional segregation of communication and onboard sensing systems in mobility applications is due to be merged using Joint Communication and Sensing (JCAS) in the development of the 6G mobile radio standard. The integration of JCAS functions into the future road traffic landscape introduces novel challenges for the design of the 6G system architecture. Special emphasis will be placed on facilitating direct communication between road users and aerial drones. In various mobility scenarios, diverse levels of integration will be explored, ranging from leveraging communication capabilities to coordinate different radars to achieving deep integration through a unified waveform. In this paper, we have identified use cases and derive five higher-level Tech Cases (TCs). Technical and functional requirements for the 6G system architecture for a device-oriented JCAS approach will be extracted from the TCs and used to conceptualize the architectural views.

cs.NI↗

arXiv2023

Improving unlinkability in C-ITS: a methodology for optimal obfuscation

In this paper, we develop a new methodology to provide high assurance about privacy in Cooperative Intelligent Transport Systems (C-ITS). Our focus lies on vehicle-to-everything (V2X) communications enabled by Cooperative Awareness Basic Service. Our research motivation is developed based on the analysis of unlinkability provision methods indicating a gap. To address this, we propose a Hidden Markov Model (HMM) to express unlinkability for the situation where two cars are communicating with a Roadside Unit (RSU) using Cooperative Awareness Messages (CAMs). Our HMM has labeled states specifying distinct origins of the CAMs observable by a passive attacker. We then demonstrate that a high assurance about the degree of uncertainty (e.g., entropy) about labeled states can be obtained for the attacker under the assumption that he knows actual positions of the vehicles (e.g., hidden states in HMM). We further demonstrate how unlinkability can be increased in C-ITS: we propose a joint probability distribution that both drivers must use to obfuscate their actual data jointly. This obfuscated data is then encapsulated in their CAMs. Finally, our findings are incorporated into an obfuscation algorithm whose complexity is linear in the number of discrete time steps in HMM.

cs.CR↗