Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] implementation of SSL?


view this post on Zulip Email Gateway (Aug 18 2022 at 14:03):

From: amir mohajeri <amgigi1985@yahoo.com>
Hi

I want to know about implementation of SSL protocol by Isabelle ??
Can you help me about that?

view this post on Zulip Email Gateway (Aug 18 2022 at 14:03):

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

view this post on Zulip Email Gateway (Aug 18 2022 at 14:03):

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: Apr 19 2024 at 04:17 UTC