Rewriting-Based Verification of Authentication Protocols
Kazuhiro Ogata, Kokichi Futatsugi · Electronic Notes in Theoretical Computer Science · 2004
We propose a method of formally analysing security protocols based on rewriting. The method is roughly as follows. A security protocol is modeled as an observational transition system, which is described in CafeOBJ. Proof scores showing that the protocol has safety (security) properties are then written in CafeOBJ and the proof scores are executed (rewritten) by the CafeOBJ system.