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: 520667.0, MPI für Informatik / Static Analysis Group
Automatic Proof of Strong Secrecy for Security Protocols
Authors:Blanchet, Bruno
Language:English
Place of Publication:Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany
Publisher:NWG 1 - Blanchet
Date of Publication (YYYY-MM-DD):2004
Audience:Experts Only
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. Applying this technique
to strong secrecy 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 IKE in IPsec).
Last Change of the Resource (YYYY-MM-DD):2005-08-12
Document Type:Report
Communicated by:to be appointed
Affiliations:MPI für Informatik/Static Analysis Group
Identifiers:LOCALID:C1256BDD001D715B-101B1CAFCEF1C690C125705B00327D47-...
ISSN:0946-011X
Full Text:
You have privileges to view the following file(s):
MPI-I-2004-NWG1-001.ps  [737,00 Kb] [Comment:file from upload service]  
 
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.