Abstract: The formal analysis of Open-ended Protocols is one of emerging areas of research. The IKEv2 protocol offers a complex example. Our work is based on Athena which is an efficient automatic checking approach. We introduce set theory to deal with Open-ended s

Key words: Open-ended protocol, Diffie-hellman, Security association, Strand spaces, Athena