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.

Formally verifying security protocols built on watermarking and jamming

Gabriele Costa
;
Letterio Galletta
;
Simone Soderi
2023-01-01

Abstract

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.
2023
Physica lLayer Security, Formal Security Models, Cryptographic Protocol Verification, Confidentiality, Integrity
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11771/22678
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
social impact