Email Gateway (Aug 18 2022 at 16:16): Email Gateway (Aug 18 2022 at 16:16):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi all,
This is just a reminder that we are all encouraged to let the mailing list know about your Isabelle-based work on the mailing list. This is especially important if you publish your work elsewhere than at the ITP conference or on the Archive of Formal Proof. Other people on the mailing list might be doing something similar without knowing. (This happened recently with an Isabelle-related paper presented at LPAR.)
Immodest example:
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
w/ Lawrence C. Paulson
IWIL 2010 (Yogyakarta, Indonesia)
Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.
http://www4.in.tum.de/~blanchet/iwil2010-sledgehammer.pdf
Now it's your turn!
Jasmin
Email Gateway (Aug 18 2022 at 16:16):From: Timothy McKenzie <tjm1983@gmail.com>
I'm working on establishing that "Euclid's Axiom" in Tarski's
axiomatization of the plane is independent of the other axioms.
I've already provided a (real, Cartesian) model for all of
Tarski's axioms, thus establishing that they are consistent
(relative to Isabelle/HOL).
My independence proof involves building the Beltrami-Klein model
of the hyperbolic plane and then establishing that Euclid's Axiom
is false in that model, but all the other axioms are true.
Timothy
<><
signature.asc
Email Gateway (Aug 18 2022 at 16:17):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Hi all,
Now it's your turn!
here is another one:
Developing Security Protocols by Refinement
Christoph Sprenger and David Basin
Proceedings of the 17th ACM Conference on Computer and Communications
Security (CCS)
Chicago, IL, USA, October 4-8, 2010, pp. 361--374
Abstract--- We propose a development method for security protocols
based on stepwise refinement. Our refinement strategy guides the
transformation of abstract security goals into protocols that are
secure when operating over an insecure channel controlled by a Dolev-
Yao-style intruder. The refinement steps successively introduce local
states, an intruder, communication channels with security properties,
and cryptographic operations realizing these channels. The
abstractions used provide insights on how the protocols work and
foster the development of families of protocols sharing a common
structure and properties. In contrast to post-hoc verification
methods, protocols are developed together with their correctness
proofs. We have implemented our method in Isabelle/HOL and used it to
develop different entity authentication and key transport protocols.
http://people.inf.ethz.ch/csprenge/Publications_files/ccs10-sprenger-basin.pdf
http://portal.acm.org/citation.cfm?id=1866307.1866349
Best wishes,
Christoph
Email Gateway (Aug 18 2022 at 16:17):From: Simon Meier <iridcode@gmail.com>
Hi all,
Now it's your turn!
at CSF 2010, we published the following results stemming from our ongoing
effort to provide a simple framework for developing machine-checked protocol
security proofs.
*Meier, Cremers, Basin, "Strong Invariants for the Efficient Construction of
Machine-Checked Protocol Security Proofs", in CSF, 2010, pp. 231-245.*
Abstract: We embed an operational semantics for security protocols in the
interactive theorem prover Isabelle/HOL and derive two strong
protocol-independent invariants. These invariants allow us to reason about
the possible origin of messages and justify a local typing assumption for
the otherwise untyped protocol variables. The two rules form the core of a
theory that is well-suited for interactively constructing natural,
human-readable, correctness proofs. Moreover, we develop an algorithm that
automatically generates proof scripts based on these invariants. Both
interactive and automatic proof construction are faster than competing
approaches. Moreover, we have strong correctness guarantees since all
proofs, including those deriving the underlying theory from the semantics,
are machine checked.
A pre-release of the our Isabelle theories and the proof generation tool
implemented in Haskell can be found on Simon's homepage.
http://people.inf.ethz.ch/meiersi/espl/index.html
Many of you know Paulson's inductive approach to security protocol
verification [1]. Hence, we provide a short *comparison between the
Inductive Approach and our approach.*
In the Inductive Approach both the formalization of the intruder
capabilities as well as the protocol specification are shallowly embedded in
the definition of the inductive set of traces describing the protocol
execution. The advantage of such a shallow embedding is that the
expressivity for the protocol specification is limited by HOL only. However,
the price one pays is that one has to come up with and prove more inductive
invariants.
In our approach, we use a deep embedding of a protocol specification
language that represents protocols as a set of roles where a role is a
linear sequence of send and receive steps. We formalize a protocol
independent semantics as an inductive set of traces parametrized over the
protocol being executed. This construction allows us to provide a set of
protocol independent invariants strong enough for proving secrecy and
authentication properties for "classical authentication protocols" (e.g.
Kerberos or TLS or the protocols in the SPORE [2]) without resorting to
induction over the traces.
Due to our protocol independent invariants, security proof construction
becomes (quite) mechanical. For secrecy and non-injective authentication
properties, proof search is even that simple that we can automatically find
their proofs and output them as Isabelle proof scripts. Based on these
automatically proven properties, more complex properties can then be proven
interactively.
Note that our invariants were inspired by the theory underlying the security
protocol model checker Scyther [3]. Hence, our capability for automatic
proof generation comes to no surprise. The suprising fact is that a theory
developed for automatic verification is also that well-suited for
interactive use.
The executive summary is the following: If the protocol you are verifying
can be specified as a set of linear roles and your security property can be
expressed as a predicate on traces, then our approach might provide an
elegant way to construct your security proofs. If not, then Paulson's
approach might suit your problem better. Nevertheless, we would still like
to hear about your problem, as it may be that one of the extensions we are
working on applies.
best regards,
Simon, Cas, David
[1] Paulson, "The Inductive Approach to Verifying Cryptographic Protocols",
Journal of Computer Security, vol. 6, pp. 85-128, 1998.
[2] http://www.lsv.ens-cachan.fr/Software/spore/index.html
[3] http://people.inf.ethz.ch/cremersc/scyther/index.html
Email Gateway (Aug 18 2022 at 16:17):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
signature.asc
Email Gateway (Aug 18 2022 at 16:18):From: Peter Lammich <peter.lammich@uni-muenster.de>
Jasmin Christian Blanchette wrote:
This is just a reminder that we are all encouraged to let the mailing
list know about your Isabelle-based work on the mailing list. This is
especially important if you publish your work elsewhere than at the ITP
conference or on the Archive of Formal Proof. Other people on the mailing
list might be doing something similar without knowing. (This happened
recently with an Isabelle-related paper presented at LPAR.)
Hi all,
Apart from what we published on AFP and/or ITP (ProgramConflictAnalysis,
Isabelle Collection Framework, Tree Automata, BinomialQueues, FingerTrees)
\+ in Preparation: Dijkstra's algorithm as an example for using ICF and
PriorityQueues in a complex algorithm,
we work on program analysis for concurrent programs, and verify many of our
techniques in Isabelle/HOL.
The document: Formalization of pre* for DPNs (<http://cs.uni-
muenster.de/sev/staff/lammich/isabelle/#dpn_prestar>) formalizes an automata-
based model-checking algorithm for dynamic pushdown networks, and generates
(very inefficient) executable code.
The technical report: *Isabelle Formalization of Hedge-Constrained pre and
DPNs with Locks** (<http://cs.uni-
muenster.de/sev/staff/lammich/isabelle/#pca>) formalizes an analysis of
Dynamic Pushdown Networks with Locks, an abstract model for parallel programs.
We are currently extending the results there. On the Isabelle/HOL side, the
long-term goal is to derive an executable analyser, that is specified as a
datalog-like logical program, that can be efficiently solved with BDD-based
techniques (cf. eg. the bddbddb - project)
Moreover, we are exploring how to combine approaches from separation logic
with the ImperativeHOL framework. The motivation is to develop a library
of efficient imperative datastructures for ImperativeHOL, that allows for
nice, modular proofs (An ImperativeHOL-analogon of the Isabelle Collection
Framework).
Best,
Peter
Email Gateway (Aug 18 2022 at 16:18):From: Tjark Weber <webertj@in.tum.de>
Mathematizing C++ Concurrency (POPL 2011, joint work with Mark Batty,
Scott Owens, Susmit Sarkar, and Peter Sewell, Cambridge University)
Abstract (provisional):
Shared-memory concurrency in C and C++ is pervasive in systems
programming, but has long been poorly defined. This motivated an ongoing
shared effort by the standards committees to specify concurrent
behaviour in the next versions of both languages. They aim to provide
strong guarantees for race-free programs, together with new (but subtle)
relaxed-memory atomic primitives for high-performance concurrent code.
However, the current draft standards, while the result of careful
deliberation, are still rather far from clear and rigorous definitions.
In this paper we establish a mathematical (yet readable) semantics for
C++ concurrency. We aim to capture the intent of the current draft as
closely as possible, but discuss a number of points where this is not
straightforward. We prove that a proposed x86 implementation of the
concurrency primitives is correct with respect to the x86-TSO model, and
describe our Cppmem tool for exploring the semantics of examples, using
code generated from our Isabelle/HOL definitions.
This will aid discussion of any further changes to the draft standard,
provide a correctness condition for compilers, and give a much-needed
basis for analysis and verification of concurrent C and C++ programs.
Special thanks to Jasmin Blanchette for his extensive help in getting
Nitpick to work for us!
Regards,
Tjark
Email Gateway (Aug 18 2022 at 16:24):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hi,
Some stuff I'm involved with in Edinburgh...
Automated theory exploration:
We have two systems based on Isabelle/IsaPlanner which carry out
automated theory exploration (IsaScheme and IsaCoSy). The idea is to see
how much of in inductive theory can be generated automatically. It turns
out by using counter example finding and generating only irreducible
terms you get some cool stuff:
http://dream.inf.ed.ac.uk/projects/lemmadiscovery/
http://dream.inf.ed.ac.uk/projects/isascheme/
The IsaCoSy papers to read for this stuff are:
http://www.springerlink.com/content/bk711q2u247mr967/
(preprint available at:
http://dream.inf.ed.ac.uk/projects/isaplanner/papers/synth-ind-theories-draft-2010.pdf
)
and the IsaScheme stuff is described here:
http://dream.inf.ed.ac.uk/projects/isaplanner/papers/eswa10.pdf
An experiment using Isabelle by a working mathematician:
This has resulted in two things. 1) a formalization of convex analysis,
(I'll let Bogdan say more about this) and 2) an "Isabelle Primer for
Mathematicians" which is a quick introduction to Isabelle, highlighting
some of the common difficulties and how to get around them. :)
The Isabelle primer can be downloaded from:
http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf
The formalisation will be released in due course.
Proof Planning/Inductive Theorem Proving in Isabelle:
we've been developing an automated inductive theorem prover
(IsaPlanner). This is based on Rippling, and is primarily a research
tool for exploring extensions to the technique. We've also been
experimenting with proof-plan/tactic languages a bit too, and with
synthesis techniques based on Isabelle's schematic variables (and
machinery to manage working with them). Some info and papers are
available here:
http://dream.inf.ed.ac.uk/projects/isaplanner/
Formalisation of Intuitionistic Linear Logic in Isabelle.
We've carried out various formalisations of fragments of
(Intuitionistic) Linear Logic, with proof terms, in Isabelle using the
nominal package, and also experimented with some other forms of handling
binding (Randy Pollack can say more about this perhaps?) We really ought
to tidy the linear logic stuff up and submit it to the AFP... (suddenly
feeling guilty)
In the pipeline: we're hoping to provide some re-factoring tools for
(Isar) proof scripts... still early days on that.
best,
lucas
Last updated: Nov 21 2024 at 12:39 UTC