Email Gateway (Aug 22 2022 at 15:02): Email Gateway (Aug 22 2022 at 15:02):From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new and ambitious entry concerning the development of cryptographic protocols by refinement. Details below. Have fun!
Larry Paulson
Refining Authenticated Key Agreement with Strong Adversaries
We develop a family of key agreement protocols that are correct by construction. Our work substantially extends prior work on developing security protocols by refinement. First, we strengthen the adversary by allowing him to compromise different resources of protocol participants, such as their long-term keys or their session keys. This enables the systematic development of protocols that ensure strong properties such as perfect forward secrecy. Second, we broaden the class of protocols supported to include those with non-atomic keys and equationally defined cryptographic operators. We use these extensions to develop key agreement protocols including signed Diffie-Hellman and the core of IKEv1 and SKEME.
https://www.isa-afp.org/entries/Key_Agreement_Strong_Adversaries.shtml
Email Gateway (Aug 22 2022 at 15:09):From: Lars Hupel <hupel@in.tum.de>
This entry fails the "afp_check_roots" check:
The following entries contain sessions without timeouts:
Key_Agreement_Strong_Adversaries (Compromising_DH, Compromising_Infra,
Compromising_L1, Compromising_SKEME)
The following sessions have wrong groups:
Compromising_DH {}
Compromising_Infra {}
Compromising_L1 {}
Compromising_SKEME {}
Errors found.
I see that the ROOT file explicitly states:
(* THE REMAINING SESSIONS WILL NOT BE TESTED BY THE AFP *)
But running all of these sessions takes less than 5 minutes in total on
my puny laptop, so I don't see any reason for excluding them. Thoughts?
Cheers
Lars
Last updated: Apr 20 2024 at 08:16 UTC