cookies

process_complete_with_cookie/__scripts__/compute_proof.py

@@ -23,13 +23,14 @@ def update_files(file_to_read, file_to_write):
 		#filedata = filedata.replace("new messageI1_1:bitstring;", "new messageI1_1[]:bitstring;")
 
 		#filedata = filedata.replace("new sidR_1:bitstring;", "new sidR_1[]:bitstring;")
-		filedata = filedata.replace("new stp1_1:bitstring;", "new stp1_1[]:bitstring;")
+		filedata = filedata.replace("new stp_1:bitstring;", "new stp_1[]:bitstring;")
 
 		#filedata = filedata.replace("new rm_1:bitstring;", "new rm_1[]:bitstring;")
 		filedata = filedata.replace("new nonce_1:bitstring;", "new nonce_1[]:bitstring;")
 
 		filedata = filedata.replace("new messageR0_1:bitstring;", "new messageR0_1[]:bitstring;")
-		filedata = filedata.replace("process", "axiom x: bitstring, y: bitstring, z: bitstring; event(eTest(x, y)) && event(eTest(x, z)) ==> y = z."+"\n\n"+"noselect x:bitstring; mess(new chi_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; mess(new chr_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; attacker(exp(g,x))."+'\n\n'+"process")
+		filedata = filedata.replace("process", "noselect x:bitstring; mess(new chi_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; mess(new chr_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; attacker(exp(g,x))."+'\n\n'+"process")
+		#filedata = filedata.replace("process", "axiom x: bitstring, y: bitstring, z: bitstring; event(eTest(x, y)) && event(eTest(x, z)) ==> y = z."+"\n\n"+"noselect x:bitstring; mess(new chi_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; mess(new chr_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; attacker(exp(g,x))."+'\n\n'+"process")
 		#filedata = filedata.replace("process", "axiom x: bitstring, y: bitstring, z: bitstring; event(eTest1(x, y)) && event(eTest1(x, z)) ==> y = z."+"\n\n"+"axiom x: bitstring, y: bitstring, z: bitstring; event(eTest2(x, y)) && event(eTest2(x, z)) ==> y = z."+"\n\n"+"noselect x:bitstring; mess(new chi_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; mess(new chr_1,*x)[ignoreAFewTimes]."+"\n\n"+"noselect x:bitstring; attacker(exp(g,x))."+'\n\n'+"process")
 
 	with open(file_to_write, 'w') as outfile:

process_complete_with_cookie/wireguard_peer_initiator_reference.spthy

@@ -45,7 +45,7 @@ let Initiator_Receive_Cookie(~ltkI, pkI, pkR, zero_1, chi:channel) =
     (
       let macI2n = mac(cookie, previous_msg) in
       out(chi, macI2n)
-    )) | (RevealEki(~ekI0))
+    )) | (RevealEkin(~ekI0))
 
 let Initiator(~ltkI, pkI, pkR, ~psk, empty, zero_1, chi:channel) =