Commit 3ee21ac7 authored by uiekn's avatar uiekn

Specify Hashes.uniformHash using a constant array

parent 355cbdea
......@@ -223,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);
@
......@@ -235,6 +236,9 @@ 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'));
@
@ requires Hashes.currentIndex < Hashes.VALUES.length;
@
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 1;
@ ensures \invariant_for(\result);
@ ensures print != null;
@ ensures \fresh(\result) && \fresh(\result.hashedPassword) && \fresh(\result.publicSigningKey)
......
......@@ -4,6 +4,7 @@ import java.security.SecureRandom;
import org.bouncycastle.math.ec.ECPoint;
import de.polyas.core3.open.crypto.basic.Hashes;
import de.polyas.core3.open.crypto.basic.Utils;
import de.polyas.core3.open.crypto.groups.ECGroup;
......@@ -34,6 +35,9 @@ public final class CredentialGenerator {
/*@ public normal_behavior
@ requires \static_invariant_for(Crypto);
@ requires \static_invariant_for(java.math.BigInteger);
@ requires \static_invariant_for(Hashes);
@ 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);
......
......@@ -77,10 +77,14 @@ public final class Crypto {
/*@ public normal_behavior
@ requires \static_invariant_for(BigInteger);
@ requires \invariant_for(group);
@ requires \static_invariant_for(Hashes);
@ requires Hashes.currentIndex < Hashes.VALUES.length;
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 1;
@ ensures \fresh(\result) && \fresh(\result.*) && \typeof(\result) == \type(ECPoint);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@ determines \result.value \by group.group.generator.value, group.curve.order;
@ 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);
@*/
public static /*@helper@*/ ECPoint publicCredentialFromPIN(ECGroup group, String password, String voterId) {
final BigInteger sk = Hashes.uniformHash(group.order(), password, voterId, null);
......@@ -99,10 +103,12 @@ public final class Crypto {
/*@ public normal_behavior
@ requires \static_invariant_for(java.math.BigInteger);
@ requires \invariant_for(group);
@ requires \static_invariant_for(Hashes);
@ requires Hashes.currentIndex < Hashes.VALUES.length;
@ ensures Hashes.currentIndex == \old(Hashes.currentIndex) + 1;
@ ensures \fresh(\result) && \typeof(\result) == \type(String);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
//@ determines \dl_strContent(\result) \by group.group.generator.value, group.curve.order;
@*/
public static /*@helper@*/ String loginPasswordFromMasterPIN(ECGroup group, String voterId,
String password) {
......@@ -119,7 +125,6 @@ public final class Crypto {
@ ensures \fresh(\result) && \typeof(\result) == \type(String);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
//@ determines \dl_strContent(\result) \by \nothing;
@*/
public static String hashPasswordWithSHA256(String password, String salt) {
return sha256(salt + password);
......@@ -129,7 +134,6 @@ public final class Crypto {
@ ensures \fresh(\result) && \typeof(\result) == \type(String);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
//@ determines \dl_strContent(\result) \by \nothing;
@*/
private static String sha256(String input) {
return Utils.asHexString(SHA_256_DIGEST.digest(input.getBytes()));
......
......@@ -39,6 +39,17 @@ public final class Hashes {
return ctx.digest.digest();
}
private /*@spec_public@*/ static int currentIndex;
private /*@spec_public@*/ static final BigInteger[] VALUES = {
BigInteger.valueOf(3),
BigInteger.valueOf(1),
BigInteger.valueOf(4),
BigInteger.valueOf(1),
BigInteger.valueOf(5),
BigInteger.valueOf(9)
};
/**
* Computes the uniform hash of the provided data.
*
......@@ -59,11 +70,13 @@ public final class Hashes {
*/
/*@ public normal_behavior
@ requires \static_invariant_for(BigInteger);
@ assignable \strictly_nothing;
@ determines \result.value \by \nothing;
@ 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);
@*/
public static BigInteger uniformHash(final BigInteger upperBound, final String /*@nullable@*/ s1,
final /*@nullable@*/ String s2, final /*@nullable@*/ String s3) {
return BigInteger.ZERO; // XXX: TODO: later change to constant array of big integers
return VALUES[currentIndex++];
}
}
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