From: amir mohajeri <amgigi1985@yahoo.com>
Hi
I want to know about implementation of SSL protocol by Isabelle ??
Can you help me about that?
From: Lawrence Paulson <lp15@cam.ac.uk>
I think you are confusing formal proofs about the TLS protocol (which
is closely related to SSL). See
http://www.cl.cam.ac.uk/~lp15/papers/Auth/tls.pdf
However, there is no actual implementation of SSL in Isabelle.
Larry Paulson
From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
In fact Isabelle does not 'implement' SSL. What is available is a
verification of TLS available on the Library under HOL/Auth.
It can help you, since it is very similar to SSL 3.0 (read the
disclaimer in the .thy file). A modification to fit your request
should be reasonably easy to obtain by modifying this previous
verification
Jean
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (Darwin)
iEYEARECAAYFAkqpIBAACgkQQN0Max56WidOsACdGG4/P+VafjPwdCekF+76MkOy
xyMAnjMA5KgPK8+61WFHXg8SYh41H4ua
=woOK
-----END PGP SIGNATURE-----
Last updated: Nov 21 2024 at 12:39 UTC