TAMARIN
From MaRDI portal
Cited in
(55)- Belenios
- YAPA
- KEM-DEM
- AVISPA
- CASPA_
- FAST
- ProVerif
- A procedure for deciding symbolic equivalence between sets of constraint systems
- A decidable class of security protocols for both reachability and equivalence properties
- Gaining trust by tracing security protocols
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Symbolic computation in Maude: some tapas
- Terminating non-disjoint combined unification
- MoSS: modular security specifications framework
- OFMC
- scyther
- Protocol analysis with time and space
- MFE
- MTT
- ITP
- ASPIER
- LALBLC
- Anima
- Programming and symbolic computation in Maude
- Combining proverif and automated theorem provers for security protocol verification
- Formal analysis and offline monitoring of electronic exams
- NRL
- Maude-NPA
- GNUC
- Cryptyc
- Built-in variant generation and unification, and their applications in Maude 2.7
- RiTHM
- Alice and Bob meet equational theories
- Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later
- Apte
- Akiss
- SPEC
- Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
- On Communication Models When Verifying Equivalence Properties
- scyther-proof
- CoSP
- margrave
- Z3str2
- ACUOS2
- ABETS
- CPSA
- Automated type-based analysis of injective agreement in the presence of compromised principals
- scientific article; zbMATH DE number 7453112 (Why is no real title available?)
- A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
- Helios
- A reduced semantics for deciding trace equivalence
- GLINTS
- Relating Process Languages for Security and Communication Correctness (Extended Abstract)
- Designing reliable distributed systems. A formal methods approach based on executable modeling in Maude
- MoSS
This page was built for software: TAMARIN