ProVerif

swMATH6558MaRDI QIDQ18650FDOQ18650

Author name not available (Why is that?)

Official website: http://prosecco.gforge.inria.fr/personal/bblanche/proverif/

Cited In (88)

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

This page was built for software: ProVerif