ikev2-rfc8784-tamarin-analysis
https://github.com/sophie-arqit/ikev2-rfc8784-tamarin-analysis
Science Score: 44.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
○DOI references
-
○Academic publication links
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (4.5%) to scientific vocabulary
Repository
Basic Info
- Host: GitHub
- Owner: sophie-arqit
- Language: HTML
- Default Branch: main
- Size: 215 KB
Statistics
- Stars: 1
- Watchers: 1
- Forks: 0
- Open Issues: 0
- Releases: 0
Metadata Files
readme.md
This repository contains the analysis corresponding to the article "Formal verification of the post-quantum security properties of IKEv2 PPK (RFC 8784) using the Tamarin Prover and CPSA", by Sophie Stevens, Paul D. Rowe and Emily Gray.
The Tamarin files (.spthy) should be run using the Tamarin prover https://tamarin-prover.github.io/. The CPSA file (.scm) should be run using CPSA https://hackage.haskell.org/package/cpsa.
There are four Tamarin files: - IKEv2-PSKmain.spthy; this is the main analysis; it assumes that Create Child occurs before Rekeying - IKEv2-PSKcreateChildafterRekey.spthy; similar to above, except that Create Child occurs after Rekeying - IKEv2-main-mitigation.spthy; this analyses the recommendation that we make in the article that the PPK be automatically integrated into all keys as soon as possible. - IKEv3PSKmainInitialchildnoninjectiveagreementRcounterexample.spthy; this is the interactive proof version of the lemma "Initial childnon..." from the IKEv2-PSK_main.spthy file. This is because the proof of this lemma was problemantic on a second device.
There are three files associated to the CPSA analysis: - rfc8784ss.scm; this is the main analysis including both variations of whether Rekeying occurs before or after Create Child - rfc8784allshapes.xhtml; this file has all shapes - rfc8784keyintegrityshape.xhtml; this file has only the shape corresponding to the key integrity attack (shape 90 in the previous)
Owner
- Login: sophie-arqit
- Kind: user
- Repositories: 1
- Profile: https://github.com/sophie-arqit
Citation (CITATION.cff)
cff-version: 1.2.0
authors:
- family-names: Stevens
given-names: Sophie
title: "Github Code Repository: Formal verification of the post-quantum security properties of IKEv2 PPK (RFC 8784) using the Tamarin Prover"
date-released: 2023-11-13