Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: Gerwin Klein <gerwin.klein@nicta.com.au>
We are pleased to announce two new entires in the Archive of Formal Proofs
[http://afp.sf.net]:
Benjamin Porter:
Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality
[http://afp.sf.net/entries/ClockSynchInst.shtml]
Abstract:
This document presents the mechanised proofs of two popular theorems
attributed to Augustin Louis Cauchy - Cauchy's Mean Theorem and the
Cauchy-Schwarz Inequality.
and
Damián Barsotti:
Instances of Schneider's generalized protocol of clock synchronization.
[http://afp.sf.net/entries/ClockSynchInst.shtml]
Abstract:
F. B. Schneider ("Understanding protocols for Byzantine clock
synchronization'') generalizes a number of protocols for Byzantine
fault-tolerant clock synchronization and presents a uniform proof
for their correctness. In Schneider's schema, each processor
maintains a local clock by periodically adjusting each value to one
computed by a convergence function applied to the readings of all
the clocks. Then, correctness of an algorithm, i.e. that the
readings of two clocks at any time are within a fixed bound of each
other, is based upon some conditions on the convergence function. To
prove that a particular clock synchronization algorithm is correct
it suffices to show that the convergence function used by the
algorithm meets Schneider's conditions.
Using the theorem prover Isabelle, we formalize the proofs that the
convergence functions of two algorithms, namely, the Interactive
Convergence Algorithm (ICA) of Lamport and Melliar-Smith and the
Fault-tolerant Midpoint algorithm of Lundelius-Lynch , meet
Schneider's conditions. Furthermore, we experiment on handling some
parts of the proofs with fully automatic tools like ICS and
CVC-lite.
These theories are part of a joint work with Alwen Tiu and Leonor
P. Nieto "Verification of Clock Synchronization Algorithms:
Experiments on a combination of deductive tools'' in proceedings of
AVOCS 2005 (http://users.rsise.anu.edu.au/~tiu/clocksync.pdf). In this
work the correctness of Schneider schema was also verified using
Isabelle (available at http://afp.sourceforge.net/entries/GenClock.shtml).
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 09:11):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
There are two new AFP entries available by Andreas V. Hess, Sebastian Mödersheim and Achim D. Brucker
Stateful Protocol Composition and Typing
https://www.isa-afp.org/entries/Stateful_Protocol_Composition_and_Typing.html
We provide in this AFP entry several relative soundness results for security protocols. In particular, we prove typing and compositionality results for stateful protocols (i.e., protocols with mutable state that may span several sessions), and that focuses on reachability properties. Such results are useful to simplify protocol verification by reducing it to a simpler problem: Typing results give conditions under which it is safe to verify a protocol in a typed model where only "well-typed" attacks can occur whereas compositionality results allow us to verify a composed protocol by only verifying the component protocols in isolation. The conditions on the protocols under which the results hold are furthermore syntactic in nature allowing for full automation. The foundation presented here is used in another entry to provide fully automated and formalized security proofs of stateful protocols.
Automated Stateful Protocol Verification
https://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html
In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. In this AFP entry, we present a fully-automated approach for verifying stateful security protocols, i.e., protocols with mutable state that may span several sessions. The approach supports reachability goals like secrecy and authentication. We also include a simple user-friendly transaction-based protocol specification language that is embedded into Isabelle.
Enjoy!
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC