Commit 66d2e4f4 authored by uiekn's avatar uiekn

Revert "Fix mistakes in Hash specification"

This reverts commit b426c107
parent b426c107
......@@ -209,10 +209,6 @@ public final class CredTool {
@ ==> (\exists \bigint j; 0 <= j && j < \dl_strContent((String)record.value_seq[i]).length;
@ ((char)(\dl_strContent((String)record.value_seq[i])[j])) > '\u0020'));
@
@ // Hash oracle preconditions
@ requires \static_invariant_for(Hashes);
@ requires 0 <= Hashes.currentIndex && Hashes.currentIndex < Hashes.VALUES.length - 1;
@
@ determines polyasVals.seq \by record.key_seq, record.value_seq,
@ inputColsForPolyas.seq,
@ (\seq_def int i; 0; inputColsForPolyas.seq.length; \dl_strContent(((String)inputColsForPolyas.seq[i])));
......@@ -227,6 +223,7 @@ public final class CredTool {
@ requires \static_invariant_for(java.math.BigInteger);
@ requires \static_invariant_for(CredentialGenerator);
@ requires \static_invariant_for(Crypto);
@ requires \static_invariant_for(Hashes);
@ requires \invariant_for(record);
@ requires \invariant_for(this);
@
......@@ -239,17 +236,15 @@ public final class CredTool {
@ ==> (\exists \bigint j; 0 <= j && j < \dl_strContent((String)record.value_seq[i]).length;
@ ((char)(\dl_strContent((String)record.value_seq[i])[j])) > '\u0020'));
@
@ // Hash oracle preconditions
@ requires \static_invariant_for(Hashes);
@ requires 0 <= Hashes.currentIndex && Hashes.currentIndex < Hashes.VALUES.length - 1;
@ requires Hashes.currentIndex < Hashes.VALUES.length;
@
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 2;
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 1;
@ ensures \invariant_for(\result);
@ ensures print != null;
@ ensures \fresh(\result) && \fresh(\result.hashedPassword) && \fresh(\result.publicSigningKey)
@ && \typeof(\result) == \type(GeneratedDataForVoter)
@ && \typeof(\result.hashedPassword) == \type(String) && \typeof(\result.publicSigningKey) == \type(String);
@ assignable print, Hashes.currentIndex;
@ assignable print;
@
@ determines \result.hashedPassword, \result.publicSigningKey \by \nothing \new_objects \result.hashedPassword, \result.publicSigningKey;
@ determines polyasVals.seq \by \itself;
......
......@@ -36,12 +36,12 @@ public final class CredentialGenerator {
@ requires \static_invariant_for(Crypto);
@ requires \static_invariant_for(java.math.BigInteger);
@ requires \static_invariant_for(Hashes);
@ requires 0 <= Hashes.currentIndex && Hashes.currentIndex < Hashes.VALUES.length - 1;
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 2;
@ requires Hashes.currentIndex < Hashes.VALUES.length;
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 1;
@ ensures \invariant_for(\result);
@ ensures \fresh(\result) && \fresh(\result.hashedPassword) && \fresh(\result.publicSigningKey)
@ && \typeof(\result) == \type(GeneratedDataForVoter) && \typeof(\result.hashedPassword) == \type(String) && \typeof(\result.publicSigningKey) == \type(String);
@ assignable Hashes.currentIndex;
@ assignable \nothing;
@ determines \result.hashedPassword, \result.publicSigningKey \by \nothing \new_objects \result.hashedPassword, \result.publicSigningKey;
@*/
public static GeneratedDataForVoter generateDataForVoter(String voterId,
......
......@@ -78,10 +78,10 @@ public final class Crypto {
@ requires \static_invariant_for(BigInteger);
@ requires \invariant_for(group);
@ requires \static_invariant_for(Hashes);
@ requires 0 <= Hashes.currentIndex && Hashes.currentIndex < Hashes.VALUES.length;
@ requires Hashes.currentIndex < Hashes.VALUES.length;
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 1;
@ ensures \fresh(\result) && \fresh(\result.*) && \typeof(\result) == \type(ECPoint);
@ assignable Hashes.currentIndex;
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@ determines \result.value \by group.group.generator.value, group.curve.order,
@ Hashes.currentIndex, (\seq_def int i; 0; Hashes.VALUES.length; Hashes.VALUES[i].value);
......@@ -104,10 +104,10 @@ public final class Crypto {
@ requires \static_invariant_for(java.math.BigInteger);
@ requires \invariant_for(group);
@ requires \static_invariant_for(Hashes);
@ requires 0 <= Hashes.currentIndex && Hashes.currentIndex < Hashes.VALUES.length;
@ requires Hashes.currentIndex < Hashes.VALUES.length;
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 1;
@ ensures \fresh(\result) && \typeof(\result) == \type(String);
@ assignable Hashes.currentIndex;
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@*/
public static /*@helper@*/ String loginPasswordFromMasterPIN(ECGroup group, String voterId,
......
......@@ -70,7 +70,7 @@ public final class Hashes {
*/
/*@ public normal_behavior
@ requires \static_invariant_for(BigInteger);
@ requires 0 <= currentIndex && currentIndex < VALUES.length;
@ requires currentIndex < VALUES.length;
@ ensures currentIndex == \old(currentIndex) + 1;
@ assignable currentIndex;
@ determines \result.value \by currentIndex, (\seq_def int i; 0; VALUES.length; VALUES[i].value);
......
......@@ -44,4 +44,4 @@
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::toList(java.lang.String,java.util.ArrayList)].JML normal_behavior operation contract.0";
\proofScript "script 'toList.script';"
\proofScript "script 'toList1.script';"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment