Symbolic Reachability Analysis Using Narrowing and its Application to Verification of Cryptographic Protocols.

José Meseguer Prasanna Thati

Published in: WRLA (2004)

Keyphrases

cryptographic protocols
reachability analysis
model checking
formal verification
markov decision processes
timed automata
incremental algorithms
standard model
state space
temporal logic
authentication protocol
security protocols
dynamic programming
real time
sufficient conditions
encryption decryption