| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
| Title: | Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method |
| Author: | Pasquale Noce (pasquale /dot/ noce /dot/ lavoro /at/ gmail /dot/ com) |
| Submission date: | 2017-01-03 |
| Abstract: | This paper constructs a formal model of a Diffie-Hellman password-based authentication protocol between a user and a smart card, and proves its security. The protocol provides for the dispatch of the user's password to the smart card on a secure messaging channel established by means of Password Authenticated Connection Establishment (PACE), where the mapping method being used is Chip Authentication Mapping. By applying and suitably extending Paulson's Inductive Method, this paper proves that the protocol establishes trustworthy secure messaging channels, preserves the secrecy of users' passwords, and provides an effective mutual authentication service. What is more, these security properties turn out to hold independently of the secrecy of the PACE authentication key. |
| BibTeX: |
@article{Password_Authentication_Protocol-AFP,
author = {Pasquale Noce},
title = {Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method},
journal = {Archive of Formal Proofs},
month = jan,
year = 2017,
note = {\url{http://isa-afp.org/entries/Password_Authentication_Protocol.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |