Abstract:

The article took the formal analysis method to prove the security protocol security as the research purpose, and took the SIP protocol with the characteristics of flexibility, openness and scalability as the research object. The article employed a formal analysis approach based on the improved recursive authentication test within the framework of strand space theory. It scrutinized a SIP authentication negotiation protocol that had been proven secure using BAN logic, revealing inaccuracies in protocol format and vulnerabilities to man-in-the-middle attacks during its execution. Subsequently, the article proposed a revised scheme tailored to address these identified deficiencies. The results indicate that the recursive authentication test formal analysis method employed in this article is more applicable and effective than BAN logic. Furthermore, the proposed improvements significantly enhance the security of the SIP authentication negotiation protocol.

Key words: SIP protocol, recursive authentication test, strand space, formal analysis methods