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?

  • 1
    If you vote the post -ev at least write the reason, why this question is worthless or illogical. It will help me to reformulate or further explain my question. This is my first ever question I asked here and got -ev vote without getting the response. In academics you should share your opinion if you disagree as well
    – Mohaqiq
    Sep 30, 2015 at 6:48
  • Could expand or link to the "logic" approach you mention?
    – RoraΖ
    Sep 30, 2015 at 17:53
  • Sorry that I can't spare much time for a full answer, but consider looking at this paper to see if the proposed framework is helpful in your review. There are probably other relevant papers if you have time to go through the paper index on the site and browse through them.
    – PwdRsch
    Sep 30, 2015 at 18:33
  • 1
    Could you remove all the details about the new protocol and just ask about formal methods for proving strength of authentication protocols? I think that would make the question more accessible to site members. Sep 30, 2015 at 21:22
  • @RoraΖ Please refer to following papers for logic approach: link and link
    – Mohaqiq
    Oct 1, 2015 at 0:46


You must log in to answer this question.