I designed an authentication protocol for consumer-producer applications, which barrows features from Kerberos and Tesla.
To check the strength of protocol I considered different well known attacks like Parallel session, Replay, Binding and encapsulation. These attacks require impersonating a Consumer or Producer. Our protocol successfully detects such attacks (based upon the considered scenarios). However, I am not confident about such analysis; I want to use a formal method to prove the strength of the protocol.
I considered using logic approach, like BAN, GNY or CKT5 methods, but on some discussion forums I found that logic methods are considered weak to check protocol strength. What are the pros and cons for such methods and what other formal methods exist to analyze such a system?