diff --git a/ClassicEAC.spthy b/ClassicEAC.spthy
index 1beea11e09343f38c60c63b055cd01d1dcdacd80..403fc9bea44d2d782e321b0c9129013e694b6700 100644
--- a/ClassicEAC.spthy
+++ b/ClassicEAC.spthy
@@ -53,7 +53,7 @@ let
     msg3 = <s, '3', 't'>
 in
     [ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT, 'terminal') ]
-  --[ Computed($T, 'terminal', s) ]->
+  -->
     [ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ]
 
 rule TA_COMPLETE_C:
@@ -100,7 +100,7 @@ let
     sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2>
 in
     [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
-  --[ Eq(pkTe_t, pkTe), Computed($C, 'chip', <k, kMac, kEnc, tag>), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
+  --[ Eq(pkTe_t, pkTe), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
     [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ]
 
 
@@ -116,7 +116,7 @@ let
     sid = <certT, certC, pkTe, pkC, id_c, r2>
 in
     [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT, 'terminal') ]
-  --[ Eq(tag, tag_T), Computed($T, 'terminal', <k, kMac, kEnc, tag_T>), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+  --[ Eq(tag, tag_T), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
     [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(sid, <kEnc, kMac>) ]
 
 
diff --git a/include/lemmas.spthy b/include/lemmas.spthy
index 73ffbba17156908bd2d821c2950f5f18d2303e0a..69b4025d32d076efbc0ca2aaedca9c620fd568a9 100644
--- a/include/lemmas.spthy
+++ b/include/lemmas.spthy
@@ -109,41 +109,8 @@ lemma chip_hiding:
         | (Ex #m . (K(iid) @ #m & #i < #m))
   "
 
-/* This lemma shows that the chip has NOT non-repudiation */
-// We use the exists-trace keyword because it is enough to show the possibility
-// 1.: To exclude an empty trace, we check for a finished protocol run (with the two Completed facts)
-// 2.: We define that the chip is not corrupted
-// 3.: We say that for every data the chip computed (which we manually put into action facts) the adversary could know the value before
-    // We use the adversaries knowledge because it is easy to model and he can simple corrupt the terminal and execute the protocol instead
-// Problems: Some information required so that the other party can compute the data is sent after the Computed fact
-
-/*
-lemma notNonRepudiation: exists-trace
-  "Ex C T k sid #i #j .
-    Completed(k, sid, C, 'chip', T) @ #i            // 1.
-    & Completed(k, sid, T, 'terminal', C) @ #j      // 1.
-    & not(Ex #n . Corrupted(C) @ #n)                // 2.
-    & (All data #m . Computed(C, 'chip', data) @ #m // 3.
-       ==> (Ex #k . K(data) @ #k & #k < #m))        // 3.
-  "
-*/
-
-/* 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
-
-/*
-lemma notNonRepudiation2: exists-trace
-  "Ex C T T2 k k2 sid sid2 #i #i2 #j #j2 .
-    Completed(k, sid, C, 'chip', T) @ #i
-    & Completed(k2, sid2, T, 'chip', T2) @ #i2
-    & Completed(k2, sid2, T2, 'terminal', T) @ #j2
-  "
-*/
 
 /* We simulate a one sided protocol execution */
-
 // The terminal submits a transcript for a valid protocol execution and the chip verifies it
 // 1.: We prohibit any previous protocol executions
 // 2.: The chip should not be corrupted, so that the terminal needs to forge the values