tamarin-prover/tamarin-prover

Issues

• Incorrect wellformedness error warning in interactive mode

  #675 opened 3 months ago by yavivanov
  0

• [Feature] Click to open constraint system image in new tab

  #604 opened 4 months ago by thgoebel
  0

• tamarin-prover: client_session_key.aes: withBinaryFile: permission denied (Permission denied)

  #603 opened 4 months ago by huahuaLover
  3

• Bug Related to Injective Facts and Tuple Unfolding

  #664 opened 5 months ago by niklasmedinger
  1

• New heuristic isn't documented yet in manual

  #646 opened 5 months ago by cascremers
  1

• Regression Tests Fail

  #640 opened 6 months ago by felixlinker
  11

• tamarin-prover can't run oracle

  #629 opened 7 months ago by mob0226
  7

• --bound argument not parsed correctly

  #630 opened 7 months ago by zevbo
  1

• Verifying hash value

  #628 opened 7 months ago by syafrizaladhitya1
  2

• Performance regression in diff models in Tamarin 180 vs 161

  #615 opened 10 months ago by swesemeyer
  7

• Arch package doesn't link properly

  #625 opened 7 months ago by JakeGinesin
  1

• Injective Fact Detection with Loop Identifier as Second Argument

  #627 opened 8 months ago by felixlinker
  7

• Bound option does not work in CLI

  #626 opened 8 months ago by racoucho1u
  2

• CLI error: "bound: invalid bound given"

  #600 opened 8 months ago by thgoebel
  0

• Diff vs Variants

  #624 opened 9 months ago by sbursuc
  2

• KEM support Question

  #623 opened 9 months ago by d-z-m
  2

• New version with GHC 9.6 support

  #620 opened 9 months ago by Vekhir
  0

• Could not find module ‘Control.Monad.List’

  #613 opened 9 months ago by Vekhir
  4

• Unable to open graphical interface

  #617 opened 9 months ago by luodds
  7

• MTI/B0 modelling error (The following rule is not multiplication restricted)

  #616 opened 10 months ago by landoflord
  1

• Reasoning behind design of annotateWithSystems and execProofMethod

  #614 opened 10 months ago by felixlinker
  0

• built-in function symbols can not find

  #589 opened a year ago by huahuaLover
  1

• Non-termination when solving for premise

  #606 opened a year ago by felixlinker
  6

• Inconsistent behavior of regression tests due to derivation check

  #609 opened a year ago by kevinmorio
  2

• Deepsec export broken due to automatically added equations

  #596 opened a year ago by kevinmorio
  1

• Unintuitive wellformedness warnings for fact usage

  #597 opened a year ago by kevinmorio
  2

• Regression tests: branch names containing "rule" are being parsed as theory rules.

  #592 opened a year ago by yavivanov
  0

• Release 1.8.0 - add to package managers

  #586 opened a year ago by rsasse
  2

• Cannot compile develop: cannot find 'ld'

  #587 opened a year ago by felixlinker
  4

• Release Request

  #574 opened a year ago by ArquintL
  3

• SAPIC, natural-numbers and multisets

  #582 opened a year ago by jdreier
  1

• unable to load the view and ./5G_AKA.oracle: readCreateProcess: runInteractiveProcess: exec: does not exist

  #577 opened a year ago by huahuaLover
  6

• Warn user when a fact occurs in an LHS, but not in any RHS

  #532 opened a year ago by cascremers
  1

• too many dotted arrows: difficult to parse large traces

  #535 opened a year ago by mohitWrangler
  5

• I have some doubts about the content in analysis_results.

  #578 opened a year ago by huahuaLover
  13

• i can not prove weakagreement_seaf_hss_noAsyKeyRev_noSupiRev_noSqnRev_noKeyRev is violated

  #579 opened a year ago by huahuaLover
  1

• Correctness of `equalRuleUpToRenaming`

  #559 opened a year ago by felixlinker
  1

• Tamarin should display a warning when using K/KD/KU facts in protocol rules

  #515 opened a year ago by jdreier
  1

• Feature request: --version output should include Maude version number

  #546 opened a year ago by cascremers
  1

• Question about capitalization issues in Tamarin

  #527 opened a year ago by artimid
  4

• Feature request: Caching precomputations

  #560 opened a year ago by cascremers
  0

• Adding annotation reuse results in non-termination of that lemma

  #558 opened a year ago by hxenia
  4

• Let-binding before variable binding disallowed by SAPIC type check

  #543 opened a year ago by kevinmorio
  1

• Pattern Matching with Let binding

  #551 opened a year ago by mohitWrangler
  1

• Running time issues

  #545 opened 2 years ago by jinshushi
  2

• Two *almost* identical files - differing only for unused rules - one verifies in 70s, the other in 25 minutes

  #539 opened 2 years ago by claudiacauli
  4

• Errors when loading 5G_AKA.spthy file fromtamarin-prover/examples/ccs18-5G/5G-AKA-bindingChannel/

  #537 opened 2 years ago by tracy-jiayi
  2

• Adding support to generate counterexamples' .dot graphs in automatic mode

  #523 opened 2 years ago by claudiacauli
  2

• Tamarin Multiset Source Deconstruction is Unsound

  #519 opened 2 years ago by felixlinker
  10

• Issue with Diffie-Hellman pre-computation when keys are split across rules

  #511 opened 2 years ago by martin-d2
  0