The perfect ‘spy’ for model−checking cryptoprotocols
Michael H. Goldsmith · 1997
This paper describes the modeling of a fully potent attacker against cryptoprotocols, including its inference system, in the process algebra CSP. Techniques for keeping the state space within practical bounds for the model checker FDR2 are explained.