MSR to ProVerif translation #538
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-authored-by: Yavor Ivanov <s8yaivan@stud.uni-saarland.de>
|
Seems fine to me :) |
|
Thanks @yavivanov and @kevinmorio ! |
yavivanov
added a commit
to yavivanov/tamarin-prover
that referenced
this pull request
Jul 2, 2023
commit 3abfc25 Author: Yavor Ivanov <s8yaivan@stud.uni-saarland.de> Date: Sun Jul 2 21:33:50 2023 +0200 massive simplifications commit 64b75d8 Merge: 6fbaa34 7d77450 Author: Yavor Ivanov <s8yaivan@stud.uni-saarland.de> Date: Fri Jun 30 21:19:21 2023 +0200 Merge remote-tracking branch 'origin' into pr-spthy-config-mirror commit 7d77450 Author: jdreier <jdreier@users.noreply.github.com> Date: Thu Jun 29 09:53:06 2023 +0200 Show exception (tamarin-prover#557) * show IOException * fix compile error * better message commit b62bb18 Author: Jérôme <43431957+Azurios-git@users.noreply.github.com> Date: Tue Jun 27 17:24:22 2023 +0200 Add checks for potential modelling errors in rules (tamarin-prover#541) * Message Derivation Checks (Squashed) * Update all regression case studies to version with ** new warnings (from Message Derivation Checks, this commit) ** tactics included --------- Message Derivation Checks authored-by: Jérôme Schneider <jerome.schneider@inf.ethz.ch> Regression update by: Ralf Sasse <ralf.sasse@gmail.com> commit 8861567 Author: ValentinYuri <135957879+ValentinYuri@users.noreply.github.com> Date: Fri Jun 23 10:40:39 2023 +0200 Adding Maude version to --version option of Tamarin (tamarin-prover#550) * Adding Maude version to --version option of Tamarin * Removing useless comments and moving others comments commit 6bb7704 Author: ValentinYuri <135957879+ValentinYuri@users.noreply.github.com> Date: Wed Jun 21 13:14:34 2023 +0200 Improving regression tests (tamarin-prover#548) * adding regression tests * Giving more information to the user * fix typos mistake and improving the information given commit e2f1107 Author: ValentinYuri <135957879+ValentinYuri@users.noreply.github.com> Date: Wed Jun 21 09:31:00 2023 +0200 forall to forAll (tamarin-prover#549) * Changing the forall occurence to forAll * remplacing all foreall function occurence by forAll on Haskell file commit f606bac Author: Kevin Morio <kevin.morio@cispa.de> Date: Tue Jun 20 12:25:07 2023 +0200 Remove duplicates in clashes check (tamarin-prover#542) commit 3e88255 Author: Pops <55747975+racoucho1u@users.noreply.github.com> Date: Fri Jun 9 10:32:47 2023 +0200 Tactic parser (tamarin-prover#547) Correcting an error in the help message of Tamarin (it said the default heuristic was C instead of s) Co-authored-by: Maiwenn Racouchot <mracouch@maiwenn.loria.fr> commit 0dfcf68 Author: charlie-j <jacomme@crans.org> Date: Thu Apr 20 15:35:32 2023 +0200 Sapic fixes diverse (tamarin-prover#540) * Fix overly strong error in Sapic translation Multiset can only be used for the specific integer modeling, we thuse raise a warning when multiset is translated, not an error. This should disappear once builtin natural numbers are included in Tamarin and translated in Sapic. * Example fix due to event renaming Events are now renamed to correclty export msr to proverif, manulaly specified queries thus need to be updated. * Fix newly raised multiple definition error * Fix non exported exist trace commit 57c1d05 Author: yavivanov <72205545+yavivanov@users.noreply.github.com> Date: Thu Apr 20 08:57:27 2023 +0200 MSR to ProVerif translation (tamarin-prover#538) Co-authored-by: Julian Biehl <julianbiehl@yahoo.de> commit 1bc24b9 Author: Pops <55747975+racoucho1u@users.noreply.github.com> Date: Tue Apr 4 17:27:55 2023 +0200 Tactic parser (tamarin-prover#531) * Correcting a typo --------- Co-authored-by: Maiwenn Racouchot <mracouch@maiwenn.loria.fr> Co-authored-by: Jannik Dreier <jannik.dreier@loria.fr> Co-authored-by: jdreier <jdreier@users.noreply.github.com> commit d9eaa24 Author: rkunnema <robert.kuennemann@cispa.de> Date: Thu Mar 30 14:46:33 2023 +0200 SAPIC: translate processes by default (tamarin-prover#530) * Updated Stack to LTS 20-12 (GHC 9.2.6). * Have translation into MSR rules be the default. --------- Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland> commit 2106e17 Author: rkunnema <robert.kuennemann@cispa.de> Date: Thu Mar 30 09:51:16 2023 +0200 Remove warnings and some linting in SAPIC. (tamarin-prover#528) * Remove warnings and some linting in SAPIC. * Updated Stack to LTS 20-12 (GHC 9.2.6). --------- Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland> commit c168e24 Merge: 12560ff daf7d18 Author: Cas Cremers <cas.cremers@gmail.com> Date: Tue Mar 28 15:56:33 2023 +0200 Merge pull request tamarin-prover#533 from felixlinker/develop Make proof tree more readable when going wide commit 12560ff Merge: ef1c24a 98495c2 Author: Cas Cremers <cas.cremers@gmail.com> Date: Tue Mar 28 15:56:07 2023 +0200 Merge pull request tamarin-prover#534 from felixlinker/vscode gitignore .vscode commit daf7d18 Author: Felix Linker <linkerfelix@gmail.com> Date: Mon Mar 27 16:58:02 2023 +0200 Make proof tree more readable when going wide commit 98495c2 Author: Felix Linker <linkerfelix@gmail.com> Date: Tue Mar 14 15:19:26 2023 +0100 gitignore .vscode commit ef1c24a Author: rkunnema <robert.kuennemann@cispa.de> Date: Wed Mar 8 14:15:06 2023 +0100 Renaming SAPIC options for consistency. (tamarin-prover#526) Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland> commit 958f8b1 Author: Pops <55747975+racoucho1u@users.noreply.github.com> Date: Mon Feb 13 13:09:51 2023 +0100 Tactic parser (tamarin-prover#508) * Modification du parseur, issue 338 * issue333, stopping user to put predefined functions in equations * fixing issue338, disallowing persistent fresh facts * issue 296, correcting macro preprocessing * issue 323/334, adding options in lemma selection * New way of dealing with oracles: tactics * Tactics * Première version pour le parsing de tactic * Basic tactic parser functionning * Première intégration du parser * Fonctionnement de base de TacticI validée * Fonctionnement des tactics par appel dans les [] * Fonctionnement du flag heuristic pour les tacticI, plusieurs fonctions par prio et tacticI non spécifiée * Option heuristic par defaut dans les tacticI * Corrections diverses * Ecriture de tactics pour le benchmark * Ecriture de tactic pour le benchmark * Affichage plus efficace de l'output * Changement du parseur pour creer les objets fonctions + ajout des not, or, and (not fonctionne) * Parser with functionning OR, AND and NOT * Changement heuristic en presort * Prettyprint des tactics * Correction problème affichage tactic dans choix heuristic et dans prettyprint des lemmas * started using functions from Token.hs - fixes issues with spacing and comments * Changements de types dans le parser + script pour le banchmark * Premier run du benchmark sur le serveur cassis * New oracles * Ajout de l'option oracle aux scripts * Res temp benchmark serveur * Modif pour serveur * Corrections script * Version correcte oracle oracle_correctness_two_valid_linked_certs * script * Matériel pour Elise * nettoyage * Ajout des tactics dans les fichiers théories * Nouvelle version du script et des inputs * Modif script: non écrasage des resultats tampons * Input spécialisé par fichier * Nouvelles tactics * Correction beug * Nex library for regex * Allowing tactics to use proofcontext and system * On going work on Noise oracle, not wworking version * Integration of Vacarme's oracle.py _ it's workiiiiiiiiiiiiiing! * Nettoyage * Gestion des oracle de vacarme (sans curve) * Finished merging with sapic * First pass on the code * Minor changes * Minor changes * Revert "Minor changes" This reverts commit 1845a45. * Tying up loose ends * Corrections merge * Merge correction * Small change * Slight change in printing * Cleaning * Adding comments * Commit before merge * Regression test passing * Nettoyage * Affichage en rouge + nettoyage * Nettoyage * Correction on export * Correction import de preuve * Removing a warning * Noise tactics examples --------- Co-authored-by: Maiwenn Racouchot <mracouch@maiwenn.loria.fr> Co-authored-by: Jannik Dreier <jannik.dreier@loria.fr> Co-authored-by: jdreier <jdreier@users.noreply.github.com> commit 3bc614f Author: charlie-j <jacomme@crans.org> Date: Mon Feb 13 08:52:43 2023 +0100 Output module fix (tamarin-prover#524) * Output module fix option -m=msr set parseonlyflags to true, which disabled the sapic translation, and thus produced an empty output. * Commenting and code cleanup. --------- Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland> commit 7485e6b Author: charlie-j <jacomme@crans.org> Date: Mon Feb 13 08:52:30 2023 +0100 Sapic diverse fixes (tamarin-prover#525) * make export queries be non unique * Typing now includes the signature Equations specified in the signature are now used to initialize the typing environment. Enhance the precision of the typing, and fixes a bug where a function symbol not occuring in the process was not typed. * Improve error reporting Errors are not printed anymore inside the exported file, but directly raised as exceptions. * Raise warning over in(=~x) commit 7c98032 Merge: 9d97e71 5747a3b Author: Cas Cremers <cas.cremers@gmail.com> Date: Thu Feb 2 09:51:02 2023 +0100 Merge pull request tamarin-prover#522 from jdreier/fix-issue-519 Fix issue 519 commit 5747a3b Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Jan 27 20:57:55 2023 +0100 correct regression output, fixed wrong Term.hs commit deed4ce Merge: c8509cf ef9a228 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Jan 27 20:21:29 2023 +0100 Merge branch 'develop' into fix-issue-519 commit ef9a228 Merge: e6ff0af 9d97e71 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Jan 27 20:21:14 2023 +0100 Merge remote-tracking branch 'upstream/develop' into develop commit c8509cf Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Jan 27 20:20:33 2023 +0100 fix issue 519 commit 9d97e71 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Jan 27 20:19:54 2023 +0100 fixed regression targets commit e6ff0af Merge: 565626b 334a0df Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Jan 27 16:42:05 2023 +0100 Merge remote-tracking branch 'upstream/develop' into develop commit 334a0df Author: charlie-j <jacomme@crans.org> Date: Fri Jan 27 13:31:21 2023 +0100 Feature destructor option (tamarin-prover#521) * Make destructor non default in builtins * Update regressions * Fix report funsym that should be destructor (only a sapic builtin) commit a810774 Author: Kevin Morio <kevin.morio@cispa.de> Date: Mon Jan 23 15:33:03 2023 +0100 Fix reporting of processing time (tamarin-prover#517) Fixes a regression introduced in tamarin-prover#484 where the processing time was incorrectly measured due to the missing full evaluation of the IO action. Additionally, the precission of the reported time is now set to 2. commit df1aa9f Author: Felix Yan <felixonmars@archlinux.org> Date: Tue Jan 17 21:01:18 2023 +0800 Allow Maude 3.2.2 (tamarin-prover#518) All self tests are passing. Below are the results of regression tests: ``` $ python regressionTests.py -noi running 'make -j 1 fast-case-studies FAST=y 2>/dev/null' ... The time changed from 0.04s to 5.78s in /fast-tests/csf12/KAS2_original_analyzed.spthy The steps changed from 246 steps to 254 steps in KAS_key_secrecy The time changed from 0.04s to 22.74s in /fast-tests/csf12/DH2_original_analyzed.spthy The steps changed from 501 steps to 503 steps in KAS_key_secrecy The time changed from 0.03s to 0.08s in /fast-tests/loops/Minimal_Loop_Example_analyzed.spthy The steps changed from 12 steps to 14 steps in Stop_unique The time changed from 0.04s to 0.22s in /fast-tests/loops/Typing_and_Destructors_analyzed.spthy The steps changed from 14 steps to 17 steps in Responder_secrecy The time changed from 0.05s to 14.51s in /fast-tests/related_work/YubiSecure_KS_STM12/Yubikey_analyzed.spthy The steps changed from 1141 steps to 1145 steps in slightly_weaker_invariant The time changed from 0.03s to 4.68s in /fast-tests/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM_multiset_analyzed.spthy The steps changed from 119 steps to 132 steps in slightly_weaker_invariant The time changed from 0.03s to 1.46s in /fast-tests/features/multiset/counter_analyzed.spthy The steps changed from 50 steps to 52 steps in counters_linear_order The steps changed from 44 steps to 58 steps in counter_increases The steps changed from 25 steps to 26 steps in lesser_senc_secret The time changed from 0.04s to 1.65s in /fast-tests/csf18-xor/KCL07_analyzed.spthy The steps changed from 113 steps to 128 steps in recentalive_tag The time changed from 0.04s to 16.28s in /fast-tests/csf18-xor/LAK06_analyzed.spthy The steps changed from 2082 steps to 2148 steps in noninjectiveagreementTAG -------------------------------------------------------------------------------- The total amount of time changed from 3s to 718s - this is 22401% The total amount of steps changed from 18858 steps to 18988 steps - this is 100% Time elapsed: 0:08:17s ``` commit 3a0d2ee Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Jan 17 11:49:50 2023 +0100 removed obsolete sapic-clean target commit 2ae120c Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Mon Jan 16 10:16:58 2023 +0100 Update Maude version for GitHub actions commit 75b0a8d Author: JulianBiehl <julianbiehl@yahoo.de> Date: Wed Dec 21 08:55:41 2022 +0100 Fixed asiaccs20-eccDAA examples (tamarin-prover#516) commit 7cec6d2 Author: rkunnema <robert.kuennemann@cispa.de> Date: Wed Dec 21 08:51:12 2022 +0100 export: Translate K()-events to attacker() (tamarin-prover#505) * export: Translate K()-events to attacker() * Updated regressions. Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland> commit 54242a0 Author: Kevin Morio <kevin.morio@cispa.de> Date: Fri Dec 9 13:09:22 2022 +0100 Revise artifact of exposure notification systems paper (USENIX 23) (tamarin-prover#514) commit 17c44fe Author: JulianBiehl <julianbiehl@yahoo.de> Date: Tue Nov 29 17:17:07 2022 +0100 Fixed event translation in Export module (tamarin-prover#513) * Fixed event translation in Export module * Fixed human errors examples commit c0921c7 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Nov 8 13:41:23 2022 +0100 deactivate protection for reserved names commit fd76a55 Merge: 3063551 3d33cbc Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Nov 8 13:35:57 2022 +0100 Merge remote-tracking branch 'upstream/develop' into free-equations commit 3063551 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Sep 23 15:59:05 2022 +0200 fix dh-neutral for maude commit 565626b Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Sep 23 15:57:18 2022 +0200 Revert "fix DH-neutral" This reverts commit e22a24f. commit e22a24f Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Sep 23 15:55:23 2022 +0200 fix DH-neutral commit d9d192f Merge: 181f55e f1f3969 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Sep 23 15:52:50 2022 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 181f55e Merge: 68ecaa6 cd9b3a5 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Wed Aug 31 17:29:25 2022 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 68ecaa6 Merge: 8439dc7 0515fbf Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Mon Jun 27 14:30:52 2022 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 8439dc7 Merge: 0bb6d8c 0660aba Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Wed Jun 15 15:37:19 2022 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 0bb6d8c Merge: 969da84 b14a9e0 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Wed Jun 15 15:11:43 2022 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 969da84 Merge: c10cb30 8f00a71 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri May 6 10:45:47 2022 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit c10cb30 Merge: 7b3f0ce 96ec81b Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Wed Apr 13 14:28:52 2022 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 7b3f0ce Merge: 3aa6c8a 7ee0b21 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Aug 24 11:57:12 2021 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 3aa6c8a Merge: a11ad1b 4219028 Author: jdreier <jdreier@users.noreply.github.com> Date: Tue Jul 20 11:19:31 2021 +0200 Merge branch 'tamarin-prover:develop' into develop commit a11ad1b Merge: 8703fc6 52fb4f8 Author: jdreier <jdreier@users.noreply.github.com> Date: Mon Jul 12 14:59:03 2021 +0200 Merge branch 'tamarin-prover:develop' into develop commit 8703fc6 Merge: c13899c c78c7af Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Mon Mar 29 09:42:51 2021 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit c13899c Merge: a5c7cce 0a82085 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Sun Mar 21 20:53:07 2021 +0100 Merge remote-tracking branch 'upstream/develop' into develop commit a5c7cce Merge: b64bbb6 51ab611 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Jan 19 11:40:41 2021 +0100 Merge remote-tracking branch 'upstream/develop' into develop commit b64bbb6 Merge: 8f8f9a0 e8a5cb5 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Wed Oct 7 16:32:07 2020 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 8f8f9a0 Merge: 11700f8 4ac0b9d Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Thu Sep 24 14:55:26 2020 +0200 Merge branch 'develop' of github.com:jdreier/tamarin-prover into develop commit 4ac0b9d Merge: acd929d 2884fce Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Wed Sep 23 13:36:49 2020 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 11700f8 Merge: acd929d 2884fce Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Mon Sep 21 17:38:47 2020 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit acd929d Merge: 7e47b41 ca22287 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Thu Jul 23 09:52:41 2020 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 7e47b41 Merge: d7faf3f cb1add2 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Jul 21 15:04:41 2020 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit d7faf3f Merge: 836d7eb eac524e Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Jun 30 16:37:12 2020 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit 836d7eb Merge: fbde116 23c9eef Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Tue Oct 8 09:34:28 2019 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit fbde116 Merge: f12512f ab0c43d Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Fri Jun 28 13:49:53 2019 +0200 Merge remote-tracking branch 'upstream/develop' into develop commit f12512f Merge: ed14a32 0127d60 Author: Jannik Dreier <jannik.dreier@loria.fr> Date: Thu Sep 27 10:25:22 2018 +0200 merge from upstream commit ed14a32 Author: Ralf Sasse <ralf.sasse@gmail.com> Date: Mon May 7 09:37:18 2018 +0200 Added change log for 1.4.0, upgraded stack to LTS 11.7, and extended copyright notice to 2018
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hi,
This PR is a refactoring of the code from PR #520, which adds a translation from Tamarin's rewrite rules to ProVerif.
I implemented the suggestions described in the PR, shortened long lines of code, contracted/ melded function definitions, removed compiler warnings and implemented the linter suggestions.