Formally verifying security protocols built on watermarking and jamming

Physical layer security mechanisms use primitives that exploit physical properties of the communication channel to protect data. Protecting communications at the physical layer offers some advantages, e.g., in terms of reduced computations, since complex cryptographic procedures are not executed, However, these mechanisms lack a formal specification that prevent protocols and applications that use them from being verified and compared with those based on cyptography. Here we start filling this gap by providing an axiomatization of key physical layer security primitives and proposing a variant of the Dolev-Yao attacker model that takes them into account. We show that our formalization enables applying existing automatic tools for verifying security of protocols. Then, we show that these primitives are a valuable alternative and effective complement to cryptography, because they ensure confidentiality and integrity but require a lower energy consumption and often they also reduce transmission time. Finally, we characterize the specific application domains and network features that make adopting these security mechanisms particularly profitable with respect to the AES cypher.