/* This lemma shows that the chip has NOT non-repudiation */
// We use the fact that every value the chip can calculate its partner could too
// We state the possibility that with a finished protocol run the terminal could identify as a chip because it knows all the computations too
// Problems: pkTe is a fresh value used in the DH key, T could simply get a chip certificate and key pair (this could be solved but would limit our model), limited by our model at the moment because the identity from Completed is from the sent certificate which prevents T from trying a replay scenario