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