Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method

Pasquale Noce 📧

January 3, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Password_Authentication_Protocol