Abstract: Strand space model is an important research field in security protocol analysis scopes. Song extends strand space model, borrows some efficient techniques from both model checking and theorem proving, proposes an efficient automatic checking approach, Ath

Key words: Strand spaces, Athena, Security protocol, Theorem proving, Model checking