Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: password-based authentication


view this post on Zulip 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: Mar 28 2024 at 12:29 UTC