*To*: Larry Paulson <lp15 at cam.ac.uk>, Peter Lammich <lammich at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle Foundation & Certification*From*: Holger Blasum <hbl at sysgo.com>*Date*: Thu, 17 Sep 2015 08:16:18 +0200*In-reply-to*: <20150917061427.GA18936@hbl-laptop.sysgo.com>*References*: <A3211BFC-696D-4616-AAD4-1E916B859A78@lri.fr> <1442414316.21093.50.camel@lapnipkow10> <9FDB3389-19DA-4B4D-9BAE-D3D9F51E2C8F@cam.ac.uk> <1442417943.21093.75.camel@lapnipkow10> <6F85EB11-F2CC-47EE-924E-ED0A603E4A11@cam.ac.uk> <20150917061427.GA18936@hbl-laptop.sysgo.com>

Same posting as parent, this time with attachment attached. On 09-17, Holger Blasum wrote: > Hello Larry, list, > > On 09-16, Larry Paulson wrote: > > It would be interesting to find out how these problems were identified: whether they were looked for out of curiosity, or whether on the other hand they manifested themselves in the course of an actual proof. > > I can give more detail for the case of EURO-MILS: We were made aware of > "Isabelle Isar-Reference Manual (Version 2013-2, pp. 103): "It is at > the discretion of the user to avoid malformed theory specifications!"[1] > Hence first attempt was to rule out use of "consts"[2]. > This resulted in people even becoming more curious and playing > with Kuncar/Popescu. > Moreover, it has been pointed out that even if we rule out "consts" and "defs" in our theories then it is still used e.g. in HOL.thy[3] (probably without > overloading, but it is hard to judge for me). > > The task at hand is not only convincing ourselves (arguably when proving some > property oneself one usually/sometimes gets a feeling for what is correct > and what not) but also others (who have limited resources). > > To give an example: in attached System_Is_Secure.thy the first > derivation of "System_Is_Secure" (theorem System_Is_Secure_1) > forces to make the assumptions of "A" and "~A" obvious. This makes > it harder to cheat ourselves or others. > > The second derivation of "System_Is_Secure" (theorem System_Is_Secure_2) > hides the assumptions and could be more easy be overlooked. > > My working understanding is (correct if that is wrong!) that fixing > Isabelle would rule out hidden derivations such as System_Is_Secure_2. > > [1] http://isabelle.in.tum.de/doc/isar-ref.pdf p 121 > The (unchecked) option disables global dependency checks for this def- > inition, which is occasionally useful for exotic overloading. It is at > the discretion of the user to avoid malformed theory specifications! > [2] http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf Section 3.1 "Constants. The Isabelle consts command is not used." > [3] http://afp.sourceforge.net/browser_info/current/HOL/HOL/HOL.html > search for "defs" > > ---------(inlined: System_Is_Secure.thy, also attached) > theory System_Is_Secure > imports Main > begin > > consts A :: bool > consts System_Is_Secure :: bool > > (* formulation with explicit assumptions, easy for reviewer to spot that user made too strong assumptions *) > theorem System_Is_Secure_1: > assumes "A" > and "~ A" > shows System_Is_Secure > proof- > from assms show ?thesis by simp > qed > > (* Kuncar/Popescu: A Consistent Foundation for Isabelle/HOL, ITP 2015 *) > consts c :: bool > typedef T = "{True, c}" by blast > defs c_bool_def: "c::bool == ~ (ALL(x::T) y. x = y)" > lemma L: "(ALL(x::T) y. x = y) <-> c" > using Rep_T Rep_T_inject Abs_T_inject by blast > lemma MyFalse: False > using L unfolding c_bool_def by auto > > theorem MySystem_Is_Secure [simp]: System_Is_Secure > using MyFalse by simp > > (* formulation with implicit assumptions, not that easy for reviewer to spot that user made too strong assumptions *) > theorem System_Is_Secure_2: System_Is_Secure by simp > > end > > > best, > > -- > Holger -- Holger Blasum SYSGO AG Office Mainz Am Pfaffenstein 14 / D-55270 Klein-Winternheim / Germany Phone: +49-6136-9948-425 / Fax: +49-6136-9948-10 / SIP:hbl at sysgo.com E-mail: holger.blasum at sysgo.com / Web: http://www.sysgo.com Handelsregister/Commercial Registry: HRB Mainz 90 HRB 8066 Vorstand/Executive Board: Knut Degen (CEO), Kai Sablotny (COO) Aufsichtsratsvorsitzender/Supervisory Board Chairman: Pascal Bouchiat USt-Id-Nr./VAT-Id-No.: DE 149062328 Meet us at our next events: http://www.sysgo.com/news-events/events/showsconferences/ Designing with Freescale Seminar October 1, 2015, Paris - France MedConf October 13-16, 2015, Munich - Germany TRANSRAIL October 14-15, 2015, Paris - France

theory System_Is_Secure imports Main begin consts A :: bool consts System_Is_Secure :: bool (* formulation with explicit assumptions, easy for reviewer to spot that user made too strong assumptions *) theorem System_Is_Secure_1: assumes "A" and "~ A" shows System_Is_Secure proof- from assms show ?thesis by simp qed (* Kuncar/Popescu: A Consistent Foundation for Isabelle/HOL, ITP 2015 *) consts c :: bool typedef T = "{True, c}" by blast defs c_bool_def: "c::bool == ~ (ALL(x::T) y. x = y)" lemma L: "(ALL(x::T) y. x = y) <-> c" using Rep_T Rep_T_inject Abs_T_inject by blast lemma MyFalse: False using L unfolding c_bool_def by auto theorem MySystem_Is_Secure [simp]: System_Is_Secure using MyFalse by simp (* formulation with implicit assumptions, not that easy for reviewer to spot that user made too strong assumptions *) theorem System_Is_Secure_2: System_Is_Secure by simp end

**References**:**[isabelle] Isabelle Foundation & Certification***From:*Burkhart Wolff

**Re: [isabelle] Isabelle Foundation & Certification***From:*Peter Lammich

**Re: [isabelle] Isabelle Foundation & Certification***From:*Larry Paulson

**Re: [isabelle] Isabelle Foundation & Certification***From:*Peter Lammich

**Re: [isabelle] Isabelle Foundation & Certification***From:*Larry Paulson

**Re: [isabelle] Isabelle Foundation & Certification***From:*Holger Blasum

- Previous by Date: Re: [isabelle] Isabelle Foundation & Certification
- Next by Date: Re: [isabelle] Isabelle Foundation & Certification
- Previous by Thread: Re: [isabelle] Isabelle Foundation & Certification
- Next by Thread: Re: [isabelle] Isabelle Foundation & Certification
- Cl-isabelle-users September 2015 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