We address the problem of message authentication using the pi-calculus, which has been given an operational semantics in [2] that provides each sequential process of a system with its own local space of names. We exploit here that semantics and its localized names to guarantee by construction that a message has been generated by a given entity. Therefore, our proposal can be seen as a reference for the analysis of ``real'' protocols. As an example, we study the way authentication is ensured by encrypting messages in the spi-calculus [1].

Authentication via Localized Names

BODEI, CHIARA;DEGANO, PIERPAOLO;PRIAMI, CORRADO
1999-01-01

Abstract

We address the problem of message authentication using the pi-calculus, which has been given an operational semantics in [2] that provides each sequential process of a system with its own local space of names. We exploit here that semantics and its localized names to guarantee by construction that a message has been generated by a given entity. Therefore, our proposal can be seen as a reference for the analysis of ``real'' protocols. As an example, we study the way authentication is ensured by encrypting messages in the spi-calculus [1].
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/11568/194011
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? 11
social impact