We extend the P-calculus and the spi-calculus with two primitives that guarantee authentication. They enable us to abstract from various implementations/specifications of authentication, and to obtain idealized protocols which are ``secure by construction''. The main underlying idea, originally proposed in for entity authentication, is to use the locations of processes in order to check who is sending a message (authentication of a party) and who originated a message (message authentication). The theory of local names, developed in for the Pcalculus, gives us almost for free both the partner authentication and the message authentication primitives.
Primitives for Authentication in Process Algebras / Bodei, Chiara; Degano, Pierpaolo; Focardi, Riccardo; Priami, Corrado. - ELETTRONICO. - (2001), pp. 1-32.
Primitives for Authentication in Process Algebras
Priami, Corrado
2001-01-01
Abstract
We extend the P-calculus and the spi-calculus with two primitives that guarantee authentication. They enable us to abstract from various implementations/specifications of authentication, and to obtain idealized protocols which are ``secure by construction''. The main underlying idea, originally proposed in for entity authentication, is to use the locations of processes in order to check who is sending a message (authentication of a party) and who originated a message (message authentication). The theory of local names, developed in for the Pcalculus, gives us almost for free both the partner authentication and the message authentication primitives.File | Dimensione | Formato | |
---|---|---|---|
19.pdf
accesso aperto
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
297.85 kB
Formato
Adobe PDF
|
297.85 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione