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