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



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
Description: S/MIME cryptographic signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.