protocol-verification-refinement
Artifact of the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations"
https://github.com/viperproject/protocol-verification-refinement
Science Score: 26.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
○CITATION.cff file
-
✓codemeta.json file
Found codemeta.json file -
○.zenodo.json file
-
✓DOI references
Found 8 DOI reference(s) in README -
○Academic publication links
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (7.4%) to scientific vocabulary
Keywords
Repository
Artifact of the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations"
Basic Info
Statistics
- Stars: 2
- Watchers: 9
- Forks: 0
- Open Issues: 0
- Releases: 1
Topics
Metadata Files
README.md
Sound Verication of Security Protocols: From Design to Interoperable Implementations (artifact)
I/O Specification Generator & Diffie-Hellman (DH) and WireGuard Case Studies
This repository contains the artifact for the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations", which appeared at the IEEE Symposium on Security and Privacy (S&P), 2023. [published version] [extended version]
This artifact provides the following content:
- Subdirectory wireguard/model contains the Tamarin model together with instructions how to verify it
- Subdirectory wireguard/implementation contains the verified Go implementation together with instructions how to verify and execute it.
- The subdirectory dh contains the verified DH protocol model together with a verified Go and Java implementations. Additionally, dh/faulty-go-implementation contains a Go implementation that tries to send the DH private key in plaintext for which verification fails because the IO specification does not permit such a send operation.
- The subdirectory specification-generator contains the sources of our tool to generate I/O specifications for Gobra & VeriFast from a Tamarin model.
This artifact has been archived on Zenodo (DOI: 10.5281/zenodo.7409524). The paper can be cited as follows (for BibTeX):
BibTex
@inproceedings{ArquintWLSSWBM23,
author = {Arquint, Linard and Wolf, Felix A. and Lallemand, Joseph and Sasse, Ralf and Sprenger, Christoph and Wiesner, Sven N. and Basin, David and M\"uller, Peter},
booktitle = {2023 IEEE Symposium on Security and Privacy (SP)},
title = {Sound Verification of Security Protocols: From Design to Interoperable Implementations},
year = {2023},
volume = {},
number = {},
pages = {1077-1093},
keywords = {protocol-verification;symbolic-security;automated-verification;tamarin;separation-logic;implementation},
publisher = {IEEE},
month = may,
doi = {10.1109/SP46215.2023.10179325},
url = {https://doi.org/10.1109/SP46215.2023.10179325},
urltext = {Publisher},
url1 = {https://pm.inf.ethz.ch/publications/ArquintWolfLallemandSasseSprengerWiesnerBasinMueller23.pdf},
url1text = {PDF}
}
Owner
- Name: Viper Project
- Login: viperproject
- Kind: organization
- Location: ETH Zurich
- Website: viper.ethz.ch
- Repositories: 29
- Profile: https://github.com/viperproject
Verification Infrastructure for Permission-based Reasoning
GitHub Events
Total
- Watch event: 4
Last Year
- Watch event: 4
Issues and Pull Requests
Last synced: 12 months ago
All Time
- Total issues: 0
- Total pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Total issue authors: 0
- Total pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Issue authors: 0
- Pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0