Constraint solving for bounded-process cryptographic protocol analysis

By J. Millen, Vitaly Shmatikov. Conference on Computer and Communications Security, 2001

368 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Scyther : semantics and verification of security protocols (2006, methodology): “The approach provides an elegant way to reason about protocol executions in the presence of a Dolev-Yao intruder, and has been used to prove many theoretical results [96, 181, 95, 78, 180] and is the basis of several tools [140, 57, 173].”
OFMC: A symbolic model checker for security protocols (2005, methodology): “Millen and Shmatikov [40] independently proposed a similar generalization to nonatomic keys (although in their case the public-key infrastructure is fixed) and gave simpler proofs than [1].”
Verifying privacy-type properties of electronic voting protocols (2009, background): “Symbolic reasoning has proved successful for reachab ility properties [38,6], in which terms input from the environment are represented as symbolic variables, together with some constraints.”