java.security
Class Signature

java.lang.Object
  java.security.SignatureSpi
      java.security.Signature

public abstract class Signature

extends SignatureSpi

JML's specification of Signaure.

Author:

Yoonsik Cheon

Class Specifications

initially this.data.isEmpty(); initially java.security.Signature.UNINITIALIZED == 0; initially java.security.Signature.SIGN == 2; initially java.security.Signature.VERIFY == 3; initially this.state == java.security.Signature.UNINITIALIZED;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
JMLValueSequence	data
Key	key

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
[spec_public] private  String	algorithm
[spec_public] private  Provider	provider
[spec_public] protected static int	SIGN
[spec_public] protected  int	state
[spec_public] protected static int	UNINITIALIZED
[spec_public] protected static int	VERIFY

 

Fields inherited from class java.security.SignatureSpi

appRandom

 

Constructor Summary
protected	Signature(non_null String algorithm)

 

Model Method Summary
boolean	isPristine()
static JMLValueSequence	toSeq(byte[] bytes)
static JMLValueSequence	toSeq(byte[] bytes, int offset, int length)

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	clone()
String	getAlgorithm()
static Signature	getInstance(non_null String algorithm)
static Signature	getInstance(non_null String algorithm, String provider)
static Signature	getInstance(String algorithm, non_null Provider provider)
Object	getParameter(String param)           Deprecated. use getParameters()
AlgorithmParameters	getParameters()
Provider	getProvider()
void	initSign(non_null PrivateKey privateKey)
void	initSign(non_null PrivateKey privateKey, non_null SecureRandom random)
void	initVerify(non_null Certificate certificate)
void	initVerify(non_null PublicKey publicKey)
void	setParameter(String param, Object value)           Deprecated. use setParameter(AlgorithmParameterSpec)
void	setParameter(non_null AlgorithmParameterSpec params)
byte[]	sign()
int	sign(byte[] outbuf, int offset, int len)
String	toString()
void	update(byte b)
void	update(non_null byte[] data)
void	update(non_null byte[] data, int off, int len)
boolean	verify(byte[] signature)
boolean	verify(byte[] signature, int offset, int length)

 

Methods inherited from class java.security.SignatureSpi

engineGetParameter, engineGetParameters, engineInitSign, engineInitSign, engineInitVerify, engineSetParameter, engineSetParameter, engineSign, engineSign, engineUpdate, engineUpdate, engineVerify, engineVerify

 

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Model Field Detail

data

public JMLValueSequence data

Specifications: non_null

key

public Key key

UNINITIALIZED

protected static final int UNINITIALIZED

Specifications: spec_public

SIGN

protected static final int SIGN

Specifications: spec_public

VERIFY

protected static final int VERIFY

Specifications: spec_public

state

protected int state

Specifications: spec_public

algorithm

private String algorithm

Specifications: spec_public

provider

private Provider provider

Specifications: spec_public

Signature

protected Signature(non_null String algorithm)

Specifications:

protected normal_behavior
requires (* algorithm is available *);
assignable this.algorithm;
ensures this.algorithm == algorithm;
ensures_redundantly this.state == java.security.Signature.UNINITIALIZED;

toSeq

public static JMLValueSequence toSeq(byte[] bytes)

Specifications: pure

requires bytes != null;

toSeq

public static JMLValueSequence toSeq(byte[] bytes,
                                     int offset,
                                     int length)

Specifications: pure

requires bytes != null&&offset >= 0&&length > 0&&(offset+length) <= bytes.length;

isPristine

public boolean isPristine()

Specifications: pure

getInstance

public static Signature getInstance(non_null String algorithm)
                             throws NoSuchAlgorithmException

Throws:

NoSuchAlgorithmException

Specifications:

public normal_behavior
requires (* algorithm is available *);
assignable \nothing;
ensures \fresh(\result )&&\result .isPristine()&&\result .algorithm == algorithm;

     also

public exceptional_behavior
requires (* algorithm is not available *);
assignable \nothing;
signals (java.security.NoSuchAlgorithmException e) true;

getInstance

public static Signature getInstance(non_null String algorithm,
                                    String provider)
                             throws NoSuchAlgorithmException,
                                    NoSuchProviderException

Throws:

NoSuchAlgorithmException

NoSuchProviderException

Specifications:

public normal_behavior
requires !provider.equals("");
requires (* algorithm is available from provider *);
assignable \nothing;
ensures \fresh(\result )&&\result .isPristine()&&\result .algorithm == algorithm&&\result .provider.getName().equals(provider);

     also

public exceptional_behavior
requires (* provider is not available *);
assignable \nothing;
signals (java.security.NoSuchProviderException e) true;

     also

public exceptional_behavior
requires (* algorithm is not available from provider*);
assignable \nothing;
signals (java.security.NoSuchAlgorithmException e) true;

getInstance

public static Signature getInstance(String algorithm,
                                    non_null Provider provider)
                             throws NoSuchAlgorithmException

Throws:

NoSuchAlgorithmException

Specifications:

public normal_behavior
requires (* algorithm is available from provider *);
assignable \nothing;
ensures \fresh(\result )&&\result .isPristine()&&\result .algorithm == algorithm&&\result .provider == provider;

     also

public exceptional_behavior
requires (* algorithm is not available from provider*);
assignable \nothing;
signals (java.security.NoSuchAlgorithmException e) true;

getProvider

public final Provider getProvider()

Specifications: pure

public normal_behavior
ensures \result == this.provider;

initVerify

public final void initVerify(non_null PublicKey publicKey)
                      throws InvalidKeyException

Throws:

InvalidKeyException

Specifications:

public normal_behavior
requires (* publicKey is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == publicKey&&this.state == java.security.Signature.VERIFY;

     also

public exceptional_behavior
requires (* publicKey is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

initVerify

public final void initVerify(non_null Certificate certificate)
                      throws InvalidKeyException

Throws:

InvalidKeyException

Specifications:

public normal_behavior
requires (* certificate.getPublicKey() is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == certificate.getPublicKey()&&this.state == java.security.Signature.VERIFY;

     also

public exceptional_behavior
requires (* certificate.getPublicKey() is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

initSign

public final void initSign(non_null PrivateKey privateKey)
                    throws InvalidKeyException

Throws:

InvalidKeyException

Specifications:

public normal_behavior
requires (* privateKey is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == privateKey&&this.state == java.security.Signature.SIGN;

     also

public exceptional_behavior
requires (* privateKey is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

initSign

public final void initSign(non_null PrivateKey privateKey,
                           non_null SecureRandom random)
                    throws InvalidKeyException

Throws:

InvalidKeyException

Specifications:

public normal_behavior
requires (* privateKey is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == privateKey&&this.state == java.security.Signature.SIGN;

     also

public exceptional_behavior
requires (* privateKey is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

sign

public final byte[] sign()
                  throws SignatureException

Throws:

SignatureException

Specifications: non_null

public normal_behavior
requires this.state == java.security.Signature.SIGN;
assignable data;
ensures this.data.isEmpty()&&(* \result is signature of \old(data) *);

     also

public exceptional_behavior
requires this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException) true;

sign

public final int sign(byte[] outbuf,
                      int offset,
                      int len)
               throws SignatureException

Throws:

SignatureException

Specifications:

public normal_behavior
requires this.state == java.security.Signature.SIGN;
assignable data;
ensures this.data.isEmpty()&&(* outbuf[offset..] contains signature of size \result *);

     also

public exceptional_behavior
requires this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException) true;

verify

public final boolean verify(byte[] signature)
                     throws SignatureException

Throws:

SignatureException

Specifications:

public normal_behavior
requires this.state == java.security.Signature.VERIFY&&(* signature improperly encoded *);
assignable data;
ensures this.data.isEmpty()&&\result <==> (* singature is authentic w.r.t. \old(data) *);

     also

public exceptional_behavior
requires this.state != java.security.Signature.VERIFY||(* signature improperly encoded *);
assignable \nothing;
signals (java.security.SignatureException e) true;

verify

public final boolean verify(byte[] signature,
                            int offset,
                            int length)
                     throws SignatureException

Throws:

SignatureException

Specifications:

public normal_behavior
requires offset >= 0&&length > 1&&(offset+length) <= signature.length&&(* signature improperly encoded *);
requires this.state == java.security.Signature.VERIFY;
assignable data;
ensures this.data.isEmpty()&&\result <==> (* singature[offset..offset+length-1] is authentic *);

     also

public exceptional_behavior
requires this.state != java.security.Signature.VERIFY||(* signature improperly encoded *);
assignable \nothing;
signals (java.security.SignatureException e) true;

update

public final void update(byte b)
                  throws SignatureException

Throws:

SignatureException

Specifications:

public normal_behavior
requires this.state == java.security.Signature.VERIFY||this.state == java.security.Signature.SIGN;
assignable data;
ensures this.data.equals(\old(this.data.insertBack(new org.jmlspecs.models.JMLByte(b))));

     also

public exceptional_behavior
requires this.state != java.security.Signature.VERIFY&&this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException e) true;

update

public final void update(non_null byte[] data)
                  throws SignatureException

Throws:

SignatureException

Specifications:

public normal_behavior
requires data.length > 0;
requires this.state == java.security.Signature.VERIFY||this.state == java.security.Signature.SIGN;
assignable this.data;
ensures this.data.equals(\old(this.data.concat(toSeq(data))));

     also

public exceptional_behavior
requires this.state != java.security.Signature.VERIFY&&this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException e) true;

update

public final void update(non_null byte[] data,
                         int off,
                         int len)
                  throws SignatureException

Throws:

SignatureException

Specifications:

public normal_behavior
requires off >= 0&&len > 1&&(off+len) <= data.length;
requires this.state == java.security.Signature.VERIFY||this.state == java.security.Signature.SIGN;
assignable this.data;
ensures this.data.equals(\old(this.data.concat(toSeq(data,off,len))));

     also

public exceptional_behavior
requires this.state != java.security.Signature.VERIFY&&this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException e) true;

getAlgorithm

public final String getAlgorithm()

Specifications: pure

public normal_behavior
ensures \result == this.algorithm;

toString

public String toString()

Overrides:

toString in class Object

Specifications: non_null

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;

setParameter

public final void setParameter(non_null AlgorithmParameterSpec params)
                        throws InvalidAlgorithmParameterException

Throws:

InvalidAlgorithmParameterException

getParameters

public final AlgorithmParameters getParameters()

Specifications: pure

clone

public Object clone()
             throws CloneNotSupportedException

Overrides:

clone in class SignatureSpi

Throws:

CloneNotSupportedException

Specifications: pure non_null

     also

public normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures (* \result is a clone of this *);

     also

public exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
signals (java.lang.CloneNotSupportedException e) true;

Specifications inherited from overridden method in class Object:
       non_null

protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);

     also

protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));

     also

protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;

     also

protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);

getParameter

public final Object getParameter(String param)
                          throws InvalidParameterException

Deprecated. use getParameters()

Throws:

InvalidParameterException

setParameter

public final void setParameter(String param,
                               Object value)
                        throws InvalidParameterException

Deprecated. use setParameter(AlgorithmParameterSpec)

Throws:

InvalidParameterException