### Abstract

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.

### License

GNU Lesser General Public License (LGPL)

### Topics

- Computer science/Security

### Session Key_Agreement_Strong_Adversaries

- Infra
- Refinement
- Messages
- Message_derivation
- IK
- Secrecy
- AuthenticationN
- AuthenticationI
- Runs
- Channels
- Payloads
- Implem
- Implem_lemmas
- Implem_symmetric
- Implem_asymmetric
- pfslvl1
- pfslvl2
- pfslvl3
- pfslvl3_asymmetric
- pfslvl3_symmetric
- dhlvl1
- dhlvl2
- dhlvl3
- dhlvl3_asymmetric
- dhlvl3_symmetric
- sklvl1
- sklvl2
- sklvl3
- sklvl3_asymmetric
- sklvl3_symmetric

## Cite

×

Key_Agreement_Strong_Adversaries-AFP

    @article{Key_Agreement_Strong_Adversaries-AFP,
      author  = {Joseph Lallemand and Christoph Sprenger},
      title   = {Refining Authenticated Key Agreement with Strong Adversaries},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Key_Agreement_Strong_Adversaries.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Feb 3, 2017 : Isabelle2016-1