Cryptography Stack Exchange is a question and answer site for software developers, mathematicians and others interested in cryptography. It only takes a minute to sign up.
Sign up to join this community
I am designing some cryptographic protocols and I am new to it. Are there any well-known tools that can be used to model and design these protocols? And also verify or analyze their validity?
If not a tool, is there any popular approach or formal method to design and analyze crypto protocols that are widely accepted?
I am searching for some tools like NRL Protocol Analyzer. Are there any other popular such tools that are considered more sophisticated?
There are a couple of options for protocol analysis tools. (I don't know any established tool for their design - as said by someone else, designing your own protocols is not really recommended.)
If you are looking for formal methods based, symbolic tools, some well-known tools that have been applied to many protocols are ProVerif and Scyther. Given that you were looking for the NRL protocol analyzer, I guess this is the class you are interested in. The NRL protocol analyzer has been superseded by the Maude-NPA tool. If you are looking for something recent with interesting new features, the Tamarin prover may be worth considering. All these tools work in the "symbolic" model often referred to as the Dolev-Yao model: they assume that the underlying cryptographic primitives (encryption schemes, signature schemes) are perfect and analyze all possible interactions between an active network attacker and the protocol. The mentioned tools can verify correctness of a protocol (with respect to an unbounded number of sessions) as well as find attacks.
The other tool mentioned here, CryptoVerif, works very differently. It aims to establish "computational" security: it (partially) automates the game-based reductions typically used for proving the security of cryptographic primitives or Key Exchange protocols. Here one tries to construct a proof that if the attacker can break the protocol, he can break the underlying hardness assumption. (An example of such a hardness assumption is computing the discrete logarithm in a Diffie-Hellman style setting.) The tool cannot find attacks. In this category I would also recommend looking at EasyCrypt and CertiCrypt.
These two types of tools work at different abstraction levels, and usually a higher abstraction level makes it feasible to analyze more complex protocols. For example, Scyther and ProVerif have been successfully used for relatively complex/large protocols. The tools in the second category give more precise security guarantees, but have so far only been used for primitives or very small protocols.
Caveat 1: if a tool finds an attack for you, you can effectively verify that it is a real attack on your protocol, which is useful. If the tool says "no attack" or "proof", it can still be the case that there is a flaw in your protocol model or security property, or that there is an attack outside of the scope of the used tool. All these tools differ in very subtle (technical) ways, which can make it very hard to compare their results.
Caveat 2: there are many more tools in the first category and I'm sure other people can explain cases in which you might want to consider on of the alternatives I didn't mention. However, without seeing your protocols and their intended security properties it is hard to give generic advice.
I personally recommend the CryptoVerif in http://cryptoverif.inria.fr/, and the Scyther in http://people.inf.ethz.ch/cremersc/tools/index.html.
