vst-crypto

SHA-256 and HMAC specs and lemmas. Compiled Coq modules are included in the folder, so SHA256.v, sha_lemmas.v, and the various HMAC specs should be usable on their own.

From:

https://svn.princeton.edu/appel/vst/sha/

http://vst.cs.princeton.edu/

Credit for code: L. Beringer, A. Petcher, A. Appel, and collaborators

Name		Name	Last commit message	Last commit date
Latest commit History 93 Commits
.svn		.svn
old		old
other		other
paper		paper
#Axioms.v#		#Axioms.v#
#Coqlib.v#		#Coqlib.v#
#HMAC_functional_prog.v#		#HMAC_functional_prog.v#
#HMAC_functional_prog_new.v#		#HMAC_functional_prog_new.v#
#README.md#		#README.md#
.#Axioms.v		.#Axioms.v
.#HMAC_functional_prog_new.v		.#HMAC_functional_prog_new.v
Axioms.glob		Axioms.glob
Axioms.v		Axioms.v
Axioms.vo		Axioms.vo
Bruteforce.glob		Bruteforce.glob
Bruteforce.v		Bruteforce.v
Bruteforce.vo		Bruteforce.vo
Bruteforce.v~		Bruteforce.v~
ByteBitRelations.v		ByteBitRelations.v
Clightdefs.glob		Clightdefs.glob
Clightdefs.vo		Clightdefs.vo
Coqlib.glob		Coqlib.glob
Coqlib.v		Coqlib.v
Coqlib.vo		Coqlib.vo
Coqlib2.glob		Coqlib2.glob
Coqlib2.v		Coqlib2.v
Coqlib2.vo		Coqlib2.vo
Coqlib2.v~		Coqlib2.v~
Extensionality.glob		Extensionality.glob
Extensionality.v		Extensionality.v
Extensionality.vo		Extensionality.vo
Extensionality.v~		Extensionality.v~
HMAC_common_defs.v		HMAC_common_defs.v
HMAC_definitions.v		HMAC_definitions.v
HMAC_functional_prog.glob		HMAC_functional_prog.glob
HMAC_functional_prog.v		HMAC_functional_prog.v
HMAC_functional_prog.vo		HMAC_functional_prog.vo
HMAC_functional_prog_Z.v		HMAC_functional_prog_Z.v
HMAC_functional_prog_Z.v~		HMAC_functional_prog_Z.v~
HMAC_lemmas.glob		HMAC_lemmas.glob
HMAC_lemmas.v		HMAC_lemmas.v
HMAC_lemmas.v~		HMAC_lemmas.v~
HMAC_lemmas_pure.v		HMAC_lemmas_pure.v
HMAC_lemmas_pure.v~		HMAC_lemmas_pure.v~
HMAC_spec_abstract.v		HMAC_spec_abstract.v
HMAC_spec_concat.v		HMAC_spec_concat.v
HMAC_spec_harvard.v		HMAC_spec_harvard.v
HMAC_spec_harvard_concat.glob		HMAC_spec_harvard_concat.glob
HMAC_spec_harvard_concat.v		HMAC_spec_harvard_concat.v
HMAC_spec_harvard_concat.vo		HMAC_spec_harvard_concat.vo
HMAC_spec_harvard_concat.v~		HMAC_spec_harvard_concat.v~
HMAC_spec_harvard_fpad.v		HMAC_spec_harvard_fpad.v
HMAC_spec_harvard_fpad.v~		HMAC_spec_harvard_fpad.v~
HMAC_spec_harvard_list.v		HMAC_spec_harvard_list.v
HMAC_spec_harvard_list.v~		HMAC_spec_harvard_list.v~
HMAC_spec_harvard_padding.v		HMAC_spec_harvard_padding.v
HMAC_spec_harvard_padding.v~		HMAC_spec_harvard_padding.v~
HMAC_spec_list.v		HMAC_spec_list.v
HMAC_spec_pad.v		HMAC_spec_pad.v
HMAC_spec_parameters.v		HMAC_spec_parameters.v
Integers.glob		Integers.glob
Integers.v		Integers.v
Integers.vo		Integers.vo
Makefile		Makefile
README.md		README.md
SHA256.glob		SHA256.glob
SHA256.v		SHA256.v
SHA256.vo		SHA256.vo
XorCorrespondence.glob		XorCorrespondence.glob
XorCorrespondence.v		XorCorrespondence.v
XorCorrespondence.vo		XorCorrespondence.vo
base.glob		base.glob
base.v		base.v
base.vo		base.vo
base.v~		base.v~
bdo_lemmas.v		bdo_lemmas.v
bn_pure_lemmas.glob		bn_pure_lemmas.glob
bn_pure_lemmas.v		bn_pure_lemmas.v
bn_pure_lemmas.vo		bn_pure_lemmas.vo
bn_pure_lemmas.v~		bn_pure_lemmas.v~
byte.hs		byte.hs
byte.hs~		byte.hs~
common_lemmas.glob		common_lemmas.glob
common_lemmas.v		common_lemmas.v
common_lemmas.vo		common_lemmas.vo
entail_examples2.v		entail_examples2.v
functional_prog.glob		functional_prog.glob
functional_prog.v		functional_prog.v
functional_prog.vo		functional_prog.vo
hmac091c.c		hmac091c.c
hmac091c.v		hmac091c.v
hmac_common_lemmas.glob		hmac_common_lemmas.glob
hmac_common_lemmas.v		hmac_common_lemmas.v
hmac_common_lemmas.vo		hmac_common_lemmas.vo
hmac_common_lemmas.v~		hmac_common_lemmas.v~
hmac_functional_prog_Z.glob		hmac_functional_prog_Z.glob
hmac_functional_prog_Z.vo		hmac_functional_prog_Z.vo
hmac_pure_lemmas.glob		hmac_pure_lemmas.glob
hmac_pure_lemmas.v		hmac_pure_lemmas.v
hmac_pure_lemmas.vo		hmac_pure_lemmas.vo

kai-qu/vst-crypto

Folders and files

Latest commit

History