Modeling and Verification of a secure protocol supporting the
group-management services of Enclaves. The developments are based on
PVS theories developed by Harald Rueß and Jon Millen.
dump
(gzipped).
Modeling and Verification of a secure protocol supporting the
group-management services of Enclaves. The developments are based on
PVS theories developed by Harald Rueß and Jon Millen.
dump
(gzipped).
Priority Ceiling Protocol.
dump
(gzipped).
Embedding CSP's trace model in PVS with application to authentication
protocols. This is joint work with Steve
Schneider.
Roots, square roots and various lemmas about exponentiation.
dump
(gzipped).
Real analysis: Continuous functions, derivatives, limits, etc.
dump
(gzipped).
Some extensions of the finite set library: powersets, cartesian
product, pigeon-hole principle.
dump
(gzipped).
Gcd, prime numbers, prime factorization, etc.:
dump
(gzipped) .
RSA (The PVS dump includes part of the previous one.)
dump
(gzipped).
Well-Ordering Principle and Zorn's lemma:
dump
(gzipped).
The theories below may not be compatible with PVS2.2 (some use the new syntax and judgements). The proofs have been done using the old decision procedures but, with a few exceptions, everything also works with the new ones. When available, the 2.4 versions contain minor modifications.
Modeling and verification of the Enclaves group-management protocol.
2.4 dump
(gzipped)
or
2.3 dump,
(gzipped).
Priority Ceiling Protocol.
2.4 dump
(gzipped) or
2.3 dump
(gzipped).
Embedding CSP's trace model in PVS with application to authentication
protocols. This is joint work with Steve
Schneider.
Roots, square roots and various lemmas about exponentiation.
2.4 dump
(gzipped) or
2.3 dump
(gzipped).
Real analysis: Continuous functions, derivatives, limits, etc.
2.4 dump
(gzipped) or
2.3 dump
(gzipped).
Some extensions of the finite set library: powersets, cartesian
product, pigeon-hole principle.
2.4 dump
(gzipped) or
2.3 dump
(gzipped).
A little number theory: gcd, prime numbers, prime factorization, etc.:
2.4 dump
(gzipped) or
2.3 dump
(gzipped).
RSA (The PVS dump includes part of the previous one.)
2.4 dump
(gzipped) or
2.3 dump
(gzipped).
Definition of fixed points for monotonic functions of type
[set[T] -> set[T]]:
2.4 dump
(gzipped)
or
2.3 dump
(gzipped).
Well-Ordering Principle and Zorn's lemma:
2.4 dump
(gzipped) or
2.3 dump
(gzipped).
Most of the things below are (gzipped) dump files produced with PVS
version 2.414 or older.
The proofs should work with newer versions but some
adjustments may be necessary.
Well-Ordering Principle and Zorn's lemma:
dump file
or compressed dump file.
Definition of fixed points for monotonic functions of type
[set[T] -> set[T]]:
dump file
or compressed dump file.
A little number theory: gcd, prime numbers, prime factorization, etc.:
dump file
or compressed dump file.
RSA (The PVS dump
includes part of the previous one.)
dump file or
compressed dump file.
Illustration of inductive definitions using CTL modal operators:
dump file or
compressed dump file.
A little real analysis: Continuous functions, derivatives, limits, etc.
dump file or
compressed dump file.
Roots, square roots and various lemmas about exponentiation.
dump file or
compressed dump file.