Cited in
(94)- Security protocol verification: symbolic and computational models
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Zabbix
- Relating Process Languages for Security and Communication Correctness (Extended Abstract)
- Alice and Bob meet equational theories
- Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity
- Formal verification of e-auction protocols
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- YAPA: A Generic Tool for Computing Intruder Knowledge
- Proving more observational equivalences with ProVerif
- Automated Verification of Dynamic Root of Trust Protocols
- Terminating non-disjoint combined unification
- The Applied Pi Calculus
- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
- Alice and Bob: reconciling formal models and implementation
- Implementing and measuring \textsf{KEMTLS}
- TulaFale
- ASSET
- AGVI
- HOL/SPIN
- YAPA
- AVISPA
- CASPA_
- FAST
- Casper
- SeVe
- ATGen
- Automated verification of selected equivalences for security protocols
- OFMC
- SATMC
- scyther
- ASPIER
- Spi2Java
- OpenNebula
- Maude-NPA
- NRL
- Cryptyc
- ConfiChair
- PIC2LNT
- RapidNet
- SANDLog
- PrologCheck
- VCGen
- TS#
- RiTHM
- Akiss
- SPEC
- Flicker
- Plutus
- SGX
- JavaSPI
- scyther-proof
- TAMARIN
- CoSP
- liboqs
- F*
- AnBx
- JSLINQ
- SeLINQ
- AODV
- CPSA
- Helios
- U-Prove
- gRPC
- Formal verification of fair exchange based on Bitcoin smart contracts
- Verification of security protocols with lists: from length one to unbounded length
- Programming Languages and Systems
- DABSTERS: a privacy preserving e-voting protocol for permissioned blockchain
- Universally composable symbolic security analysis
- Privacy-preserving authenticated key exchange for constrained devices
- Belenios
- revTPL
- \textsf{CaPiTo}: Protocol stacks for services
- Model Checking Security Protocols
- Abstractions of non-interference security: probabilistic versus possibilistic
- Automated type-based analysis of injective agreement in the presence of compromised principals
- Formal analysis and offline monitoring of electronic exams
- Computing knowledge in equational extensions of subterm convergent theories
- Analysing routing protocols: four nodes topologies are sufficient
- Theory of Cryptography
- Combining proverif and automated theorem provers for security protocol verification
- Formal methods for web security
- Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
- SeVe: automatic tool for verification of security protocols
- YAPA: a generic tool for computing intruder knowledge
- A program logic for verifying secure routing protocols
- PIC2LNT: model transformation for model checking an applied pi-calculus
- Formalizing provable anonymity in Isabelle/HOL
- Formal analysis of a TTP-free blacklistable anonymous credentials system
- Security protocols analysis including various time parameters
- Verified interoperable implementations of security protocols
- CIRCL
- Processes against tests: on defining contextual equivalences
- Gaining trust by tracing security protocols
This page was built for software: ProVerif
