*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: OndÅej KunÄar <kuncar at in.tum.de>*Date*: Sun, 9 Jul 2017 14:56:56 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>, scott constable <sdconsta at syr.edu>*In-reply-to*: <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <5b1c5907-c172-0e3d-6163-c70e0bc884c7@sketis.net> <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com> <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk>

Regardless of the question whether Isabelle should be a security software or whether there are some malicious users, in my opinion, every theorem prover should be able to answer the following question: âGiven a theorem X, which nondefinitional axioms and/or oracles (e.g., sorry) were used to prove X.â (using Isabelleâs terminology, other provers might use a different terminology). As we saw in this thread, to obtain an answer to this question is in case of Isabelle 1) neither simple (as documented by Simonâs ML code) 2) nor reliable (as pointed out by Manuel). I hope we can improve on this in foreseeable future. Best, OndÅej > On 8. Jul 2017, at 20:59, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > > 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. >

**Attachment:
smime.p7s**

**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

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

- Previous by Date: Re: [isabelle] primrec of datatype containing fset
- Next by Date: Re: [isabelle] primrec of datatype containing fset
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: [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?
- 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