Added key commitment constraint

maude/examples/tesla.psl

@@ -13,7 +13,11 @@ Theory
   ops TS TR : -> Nat .
   op TRUE : -> True .
   op FALSE : -> False .
+  
+  // Sender setup
   op DELAY : -> Nat .
+  op KEY_COMMIT : -> Key .
+  op START : -> Key .
 
   op _+_ : Nat Nat -> Nat [assoc comm id: ZERO] .
   op _-_ : Nat Nat -> Nat .
@@ -42,8 +46,8 @@ Theory
 
   eq geq(intSrc(i),+(i,DELAY)) = FALSE .
 
-  eq geq(x,w) = FALSE .
-  eq f(x) = ^(f(w), -(w, x)) .
+  eq geq(w,START) = TRUE .
+  eq KEY_COMMIT = ^(f(w), -(w, START + DELAY)) .
 
 Protocol
   vars SName RName S1Name R1Name : Name .