GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-29 10:13:29 +03:00
Code Issues Projects Releases Wiki Activity

changed collision properties to require inputs to be different

Browse Source
This commit is contained in:
Joey Dodds 2014-08-06 10:16:14 -07:00
parent 72fefff367
commit 7300f29606
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/maliciousSHA/malicious_SHA1.cry
View File

@ -78,7 +78,7 @@ malicious_k1 = [0x5a827999, 0x88e8ea68, 0x578059de, 0x54324a39]
bad_sha_eve1 = malicious_sha1 eve1 malicious_k1 bad_sha_eve1 = malicious_sha1 eve1 malicious_k1
bad_sha_eve2 = malicious_sha1 eve2 malicious_k1 bad_sha_eve2 = malicious_sha1 eve2 malicious_k1
property malicious_sha1_collision1 = bad_sha_eve1 == bad_sha_eve2 property malicious_sha1_collision1 = eve1 != eve2 && bad_sha_eve1 == bad_sha_eve2
//hexdump malicious/eve1.sh //hexdump malicious/eve1.sh
eve1_galois = [ eve1_galois = [
@ -111,7 +111,7 @@ eve2_galois = [
bad_sha_eve_galois1 = malicious_sha1 eve1_galois malicious_k1 bad_sha_eve_galois1 = malicious_sha1 eve1_galois malicious_k1
bad_sha_eve_galois2 = malicious_sha1 eve2_galois malicious_k1 bad_sha_eve_galois2 = malicious_sha1 eve2_galois malicious_k1
property malicious_sha1_collision2 = bad_sha_eve_galois1 == bad_sha_eve_galois2 property malicious_sha1_collision2 = eve1_galois != eve2_galois && bad_sha_eve_galois1 == bad_sha_eve_galois2
property all_same_hashes = bad_sha_eve_galois1 == bad_sha_eve1 && malicious_sha1_collision1 && malicious_sha1_collision2 property all_same_hashes = bad_sha_eve_galois1 == bad_sha_eve1 && malicious_sha1_collision1 && malicious_sha1_collision2