From Secrecy to Authenticity in Security Protocols

Blanchet, Bruno

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

From Secrecy to Authenticity in Security Protocols

MPS-Authors

/persons/resource/persons44141

Blanchet, Bruno
Static Analysis, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Blanchet, B. (2002). From Secrecy to Authenticity in Security Protocols. In M. Hermenegildo, & G. Puebla (Eds.), Static Analysis, 9th International Symposium, SAS 2002 (pp. 342-359). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-30F2-1

Abstract

We present a new technique for verifying authenticity in cryptographic protocols. This technique is fully automatic, it can handle an unbounded number of sessions of the protocol, and it is efficient in practice. It significantly extends a previous technique for the verification of secrecy. The protocol is represented in an extension of the pi calculus with fairly arbitrary cryptographic primitives. This protocol representation includes the authentication specification to be verified, but no other annotation. Our technique has been proved correct, implemented, and tested on various protocols from the literature. The experimental results show that we can verify these protocols in less than 1~s.