GNY

GNY has 45 rules and 13 language concepts. GNY extends BAN by adding more notions:

• Recognizability, type checking. : P believes or is entitled to believe, that formula X is recognizable.

  That is, P would recognize X if P has certain expectations about the contents of X before actually receiving X . P may recognize a particular value (e.g. his own identifier), a particular structure (e.g. the format of a timestamp), or a particular form of redundancy.

• Not-originated-here, to prevent replay. indicates that P is told a formula X which he did not convey previously in the current run.
• Idealization: No need for idealization, can treat plaintext and ciphertext similarly.
• Truth: GNY removes the restriction that one can say only what he believes, one can say any thing he possesses.
• GNY does not deal with how to make initial assumptions and that some notions like freshness are ill-defined.

GNY also adds the idea of one-way functions H(X):

• Given X it is computationally feasible to compute H(X).
• Given H(X) it is infeasible to compute X.
• It is infeasible to compute X and X' s.t. X is not X' but H(X) = H(X')

GNY claims that their logic can analyze protocols which use one-way functions. Among other additions GNY adds to take use of one way functions. Recently however a protocol was proposed which questions the soundness of R6:

1. 
2. 
3. 

If we analyze this we can conclude that A can authenticate to B by this protocol.

1. B received : by T4, B possesses .
2. S received A:
3. B received : by T6, B possesses by R6, B believes B can recognize A.

Again the flaw is misauthentication, let's look at how E can authenticate to B as A.

1. 
2. 
3. 
4.