Re: [isabelle] lexical matters



On 19/01/11 01:23, Makarius wrote:
On Tue, 18 Jan 2011, Tjark Weber wrote:

On Tue, 2011-01-18 at 11:23 +0100, Makarius wrote:
On Tue, 18 Jan 2011, Tjark Weber wrote:
As long as you assume a non-malicious user who wants to create a valid
machine-checked proof, it is not much of an issue.

This does not sound like you are speaking here about Isabelle at all. We
do not assume a "non-malicious" user. You can always inspect internal
certificates, even before embarking on full proof terms.

And a malicious user, by misusing ML in Isabelle theory files, couldn't
replace the functions that you would use to inspect internal
certificates -- or the entire inference kernel; or even the entire
Isabelle process -- with his own implementation?

Yes, depending how much criminal energy you want to invest.

And the auditor failing to spot such malfeasance would be barely worth the name.

Michael





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