formal_verification

https://github.com/hosseingeranfar/formal_verification

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 (8.7%) to scientific vocabulary

Last synced: 10 months ago · JSON representation ·

Repository

Basic Info

Host: GitHub
Owner: hosseingeranfar
Default Branch: main
Size: 25.4 KB

Statistics

Stars: 1
Watchers: 1
Forks: 0
Open Issues: 0
Releases: 0

Created about 4 years ago · Last pushed over 1 year ago

Metadata Files

Readme Citation

Formal security verification using Tamarin Prover

Overview

This repository contains the Tamarin Prover code related to the security protocol verification discussed in our paper titled “An Enhanced Security Protocol for Vehicular Adhoc Networks.” The Tamarin Prover is a powerful tool for analyzing cryptographic protocols and verifying their security properties.

Installation and Usage

For detailed installation instructions and usage guidelines, refer to Chapter 2 of the Tamarin Prover manual.

How to run the code

Formal_Verifiaction.spthy: Contains our protocol's Tamarin Prover source code.

Then run the model via the command line tool:

tamarin-prover interactive Formal_Verifiaction.spthy

Then, you can just open the generated link in your browser. The link will be something like this:

http://localhost:3001

Results

To check the model, open the Tamarin GUI and choose the correct file. Once the tab opens, you can find the model code on the left.

To prove a lemma, click "sorry" at the bottom of the lemma you want to prove. This will open the "Visualization display". You can check all lemmas by clicking "a. autoprove".

Depending on whether a lemma makes an "exists trace" statement or an "all traces" statement, different results indicate success. For proving an "exists trace" statement, Tamarin will output a trace (as a picture) that shows a fulfilling trace for the lemma. Proving an "all traces" statement means that Tamarin finds no trace that contradicts the statement.

Lemmas that can be proven will display a green trace on the left and, in the case of "exists trace" lemmas, a picture of a fulfilling trace. Lemmas that can be disproven will display a red trace on the left and, in the case of "all traces" lemmas, a picture of a contradicting trace.

Owner

Login: hosseingeranfar
Kind: user

Repositories: 1
Profile: https://github.com/hosseingeranfar

Citation (CITATION.cff)

cff-version: 1.2.0
message: "If you use this code, please cite it as below."
authors:
  - family-names: Geranfar, Bagheri
    given-names: Hossein, Nasour
    orcid: https://orcid.org/0000-0003-4925-7248
title: "Tamarin Prover "
version: 2.0.4
doi: 10.5281/zenodo.1234
date-released: 2021-08-11

ecosyste.ms

Data

Tools

Indexes

Applications

Experiments

Open Source Science