Email Gateway (Aug 22 2022 at 15:00): Email Gateway (Aug 22 2022 at 15:00):From: Lawrence Paulson <lp15@cam.ac.uk>
The year’s second AFP entry is a new application of the inductive method for verifying cryptographic protocols. Full details here:
https://www.isa-afp.org/entries/Password_Authentication_Protocol.shtml
Many thanks to Pasquale Noce for this contribution!
Larry Paulson
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.
Last updated: Nov 21 2024 at 12:39 UTC