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