Software
- A CLP prototype for Symbolic Backward Analysis
written in Sicstus Prolog and with the clp(Q,R) library (gzipped-tar-file)
Please contact giorgio@disi.unige.it for instructions
Applications
- The Ticket mutual exclusion protocol
- MSR specification (see [4])
The Li-Hudak's Broadcast Distributed Manager for Systems with Virtual Shared Memory (see [4])
- Cache coherence protocols (see [4])
- M.S.I. Protocol [AB86] MSR specification
- Synapse Protocol [AB86] MSR specification
- M.E.S.I. [AB86] MSR specification
- Mobility of Processes
- A challenge-response protocol
MSR encoding of the protocol described in [5]
Result of the analysis: fixpoint and test for initial state
(after execution with the CLP prototype)
- Security Protocols
- The application of MSR to Security Protocols is described in the
technical report [6].
- The CLP prototype used for the experiments with support for
verification of secrecy and authentication
Brief summary:
What does the prototype do? How does it work?
- Authentication and Key establishment protocols
(unbound sessions, principals and names see example [6])
- NSLPK: Typed Needham-Schroeder-Lowe public key
Commented MSR spec with the intruder
Values are typed using term constructor
- Secrecy
Results of the analysis: no "secrecy" attacks found
The protocol is proved correct for any number of principals,
generated nonces, and parallel sessions- Authentication
Description and Results of the analysis
- <#a href="http://www.disi.unige.it/person/DelzannoG/MSR/ns">NSPK: Untyped Needham-Schroeder public key
Commented MSR spec with the intruder
Subject to several possible attacks- Detailed results of the analysis againts "secrecy" (Type flaws and Lowe's attack found)
- NSPK: Typed Needham-Schroeder public key
Commented MSR spec with the intruder
Differently from the previous one values are "typed", i.e.,
wrapped into terms like pk(.), nonce(.), etc.
Detailed results of the analysis (Lowe attack found)
#
- NSLPK (II): Needham-Schroeder-Lowe public key (with more specialized intruder)
Commented MSR spec with the intruder
Results of the analysis: no "secrecy" attacks found
The protocol is proved correct for any number of principals,
generated nonces, and parallel sessions
- NSSK: Needham-Schroeder symmetric key
Commented MSR spec with the intruder
MSR spec in the prototype input format
Subject to a possible attack
Detailed results of the analysis againts "secrecy"
- NSSK: Typed Needham-Schroeder symmetric key
Commented MSR spec with the intruder
MSR spec in the prototype input format
Values are typed with term constructors
Subject to a possible attack
Detailed results of the analysis againts "secrecy"
- OR: Otway-Rees
Commented MSR spec with the intruder
MSR spec in the prototype input format
Subject to a type flaw
- OR: Typed Otway-Rees (without type-flaw)
Commented MSR spec with the intruder
Proven correct
- October 2003: Symbolic confdigurations with extended terms
The experiments on Wide Mouth Frog have been carried over using an extended prototype with the special term operator "sup".
The extended prototype: extended checker and library
- Original WMF: Wide Mouth Frog
Commented MSR spec with the intruder
- WMF-Fix: Fixed Wide Mouth without intruder (with seeds for structural analysis)
- WMF-Fix: Fixed Wide Mouth Frog (messages are tagged to distinguish initiator/server messages)
(with seeds for (timed) authentication: non-injective agreement, uniqueness)
Software
- A CLP prototype for Symbolic Forward Analysis
written in Sicstus Prolog and with the clp(Q,R) library (gzipped-tar-file)- Instructions
- Please contact giorgio@disi.unige.it for instructions
Applications
- Time Dependent Security Properties
- WMF protocol with constant validity period
- WMF protocol with parametric validity period
- Fixed WMF protocol