This study evaluates the capability of large language models (LLMs) to analyze and verify security protocols, specifically symbolic security protocol analysis using ProVerif and OFMC as benchmarks. The results show that LLMs perform poorly in this task, especially in authentication goals. The study suggests that LLMs might be useful as pre-screening filters, but not as a replacement for formal verification.