Authentication via localized names
- 1 January 1999
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636900,p. 98-110
- https://doi.org/10.1109/csfw.1999.779766
Abstract
We address the problem of message authentication using the /spl pi/-calculus, which has been given an operational semantics 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.Keywords
This publication has 10 references indexed in Scilit:
- A calculus of mobile processes, IPublished by Elsevier ,2004
- Strand spaces: why is a security protocol correct?Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Automated analysis of cryptographic protocols using MurφPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A hierarchy of authentication specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Calculus for Cryptographic Protocols: The Spi CalculusInformation and Computation, 1999
- Verifying authentication protocols in CSPIEEE Transactions on Software Engineering, 1998
- From CML to its process algebraTheoretical Computer Science, 1996
- Three systems for cryptographic protocol analysisJournal of Cryptology, 1994
- Modal logics for mobile processesTheoretical Computer Science, 1993
- A logic of authenticationACM Transactions on Computer Systems, 1990