Home News About Us Contact Contributors Disclaimer Privacy Policy Help FAQ

Home
Search
Quick Search
Advanced
Fulltext
Browse
Collections
Persons
My eDoc
Session History
Login
Name:
Password:
Documentation
Help
Support Wiki
Direct access to
document ID:


          Institute: MPI für Informatik     Collection: Static Analysis Group     Display Documents



ID: 520661.0, MPI für Informatik / Static Analysis Group
Automatic Proof of Strong Secrecy for Security Protocols
Authors:Blanchet, Bruno
Language:English
Publisher:IEEE
Place of Publication:Piscataway, USA
Date of Publication (YYYY-MM-DD):2004
Title of Proceedings:2004 IEEE Symposium on Security and Privacy
Start Page:86
End Page:100
Place of Conference/Meeting:Oakland, USA
(Start) Date of Conference/Meeting
 (YYYY-MM-DD):
2004-05-10
End Date of Conference/Meeting 
 (YYYY-MM-DD):
2004-05-12
Audience:Not Specified
Intended Educational Use:No
Abstract / Description:We present a new automatic technique for proving strong secrecy
for security protocols. Strong secrecy means that an adversary cannot
see any difference when the value of the secret changes. Our technique
relies on an automatic translation of the protocol into Horn clauses,
and a resolution algorithm on the clauses. It requires important
extensions with respect to previous work for the proof of (standard)
secrecy and authenticity. This technique can handle a wide range of
cryptographic primitives, and yields proofs valid for an unbounded
number of sessions and an unbounded message space; it is also flexible
and efficient. We have proved its correctness, implemented it,
and tested it on several examples of protocols including JFK
(a proposed replacement for IPsec).
Last Change of the Resource (YYYY-MM-DD):2004-05-10
External Publication Status:published
Document Type:Conference-Paper
Communicated by:to be appointed
Affiliations:MPI für Informatik/Static Analysis Group
Identifiers:LOCALID:C1256BDD001D715B-CF5790F12295ED53C1256E900001A96E-...
ISBN:0-7695-2136-3
The scope and number of records on eDoc is subject to the collection policies defined by each institute - see "info" button in the collection browse view.