Compiling and verifying security protocols

DOI10.1007/3-540-44404-1_10MaRDI QIDQ2767013zbMATH OpenFDO

Authors Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron

Publication date 30 June 2002

Published in Lecture Notes in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44404-1_10

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Recommendations

• The practice of cryptographic protocol verification
• Logics in Artificial Intelligence
• Automatic SAT-compilation of protocol insecurity problems via reduction to planning
• Compiling and securing cryptographic protocols
• Abstracting cryptographic protocols with tree automata.

Cited in

(20)

• The Austin Protocol Compiler.
• On the symbolic reduction of processes with cryptographic functions.
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• A formal semantics for protocol narrations
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• The practice of cryptographic protocol verification
• Information based reasoning about security protocols
• Towards an independent semantics and verification technology for the HLPSL specification language
• On the Automated Correction of Protocols with Improper Message Encoding
• The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
• Alice and Bob: reconciling formal models and implementation
• scientific article; zbMATH DE number 1330435 (Why is no real title available?)
• Automatic SAT-compilation of protocol insecurity problems via reduction to planning
• Logics in Artificial Intelligence
• Multi-attacker protocol validation
• Distributed temporal logic for the analysis of security protocol models
• On the semantics of Alice \& Bob specifications of security protocols
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Termination of narrowing via termination of rewriting
• Compiling and securing cryptographic protocols

Describes a project that uses

Uses Software

• Casper

This page was built for publication: Compiling and verifying security protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2767013)