*To*: scott constable <sdconsta at syr.edu>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sat, 8 Jul 2017 19:59:55 +0100*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>*In-reply-to*: <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <5b1c5907-c172-0e3d-6163-c70e0bc884c7@sketis.net> <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com>

To protect against malicious intentions would turn Isabelle into a form of security software. But the guarantees we get from the latter are quite different from what we get from a formal proof. Ultimately security claims depend upon trusting a lot of complicated mechanisms, such as certificate authorities and cryptosystems. We are not a lot better off than when a model checker comes back with nothing. However, we work with formal proofs, which can be examined, even interactively. We do not have to work on the basis that "X has been proved, therefore X is true", but rather "We have been given a proof of X; Is it credible?" Then we can look at any part of this proof where we have doubts. A devious user has many ways to try to fool us, but it's not so easy if he has to supply the full source code and we insist on legibility throughout. The effort we choose to invest in this would depend on how important X is and how much we distrust the person who supplied the proof. Larry Paulson > On 8 Jul 2017, at 18:12, scott constable <sdconsta at syr.edu> wrote: > > Isabelle does not protect against malicious intentions. It would require > a quite different system to do that, one that you won't like to use. > > The other big provers (e.g. Coq) are similar in this respect.

**Follow-Ups**:**Re: [isabelle] Verify the legitimacy of a proof?***From:*Lars Hupel

**Re: [isabelle] Verify the legitimacy of a proof?***From:*OndÅej KunÄar

**[isabelle] Concept of a small logical kernel, preserving logical dependencies, axiomatic type classes vs. type abstraction, Isabelle documentation â Re: Verify the legitimacy of a proof?***From:*Ken Kubota

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Peter Lammich

**References**:**[isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Makarius

**Re: [isabelle] Verify the legitimacy of a proof?***From:*scott constable

- Previous by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Cl-isabelle-users July 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list