scyther-proof-0.3.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.

Scyther.Equalities

Synopsis

# Single Equalities

type TIDEq = (TID, TID)Source

Logically these are equalities between logical thread identifier variables.

type TIDRoleEq = (TID, Role)Source

type RoleEq = (Role, Role)Source

The role equalities serve a double function:

type AVarEq = (AVar, AVar)Source

Equalities between different agent variables.

We do not have to reason about equalities between an agent variable and some other message because our semantics guarantees that agent variables are only instantiated with agent names. Hence, they can only be equal to other agent variables or message variables. In the latter case, we store the equality the other way round; assigning the agent variable to the message variable.

type MVarEq = (MVar, Message)Source

Equalities between message variables and arbitrary messages.

type MsgEq = (Message, Message)Source

Equalities between messages.

data AnyEq Source

Some representable equality.

Constructors

 TIDEq !TIDEq TIDRoleEq !TIDRoleEq RoleEq !RoleEq AgentEq !AgentEq AVarEq !AVarEq MVarEq !MVarEq MsgEq !MsgEq

Instances

 Eq AnyEq Data AnyEq Ord AnyEq Show AnyEq Typeable AnyEq Isar AnyEq

Convert an agent equality to a message equality.

Convert a message variable equallity to a message equality.

# Compound Equalities

data Equalities Source

A conjunction of equality facts.

Invariants for a value `eqs = Equalities tideqs roleeqs avareqs mvareqs agnteqs`:

1. Domain and range normalized with respect to equalities. Note that this implies substitution must always consider TID substitution first.

forall tid : ran(tideqs). substTID eqs tid = tid forall tid : dom(roleeqs). substTID eqs tid = tid forall (lid, lid') : avareqs. substLocalId eqs lid = lid & substAVar eqs lid' = lid' forall (lid, m) : mvareqs. substLocalId eqs lid = lid & substMsg eqs m = m

TODO: Complete properties for Agent ID's

forall aid : dom(agnteqs). substAgentId eqs aid = Just (Left aid) forall : dom(agnteqs). substAgentId eqs aid = Just (Left aid)

1. Origin always greater than image for symmetric eqs.

forall (tid, tid') : tideqs. tid > tid' forall (lid, lid') : avareqs. lid > lid'

1. Range of message variable equalities normalized with respect to key inversion.

forall m : ran(mvareqs). normMsg m = m

1. All thread identifiers are in the domain of roleeqs.
2. All agent identifiers are in the domain of agnteqs.
3. No cycles.

Instances

 Eq Equalities Data Equalities Ord Equalities Show Equalities Typeable Equalities

## Construction

Empty equality premises.

solve :: Monad m => [AnyEq] -> Equalities -> m EqualitiesSource

Solve a list of unification equations.

The unification is performed modulo key inversion and thread identifier equalities. Additional thread identifier equalities may result from equalities over fresh messages. Bidirectional keys are handled by delaying their solution until only one solution is possible.

Arguments

 :: Equalities -> ([TID], Equalities) Dropped TIDs plus updated equalities

Remove the thread identifier equalities. This is logically safe iff there is no fact outside the equalities that still refers to the dropped thread identifiers.

Arguments

 :: Equalities -> ([AgentId], Equalities) Dropped AgentIds plus updated equalities

Remove the agent identifiers equalities. This is logically safe iff there is no fact outside the equalities that still refers to the dropped agent identifiers.

## Destruction

The list of thread identifier equalities.

The list of role equalities.

The list of agent variable equalities.

The list of agent variable equalities.

The list of message variable equalities.

The list of postponed message equalities.

Convert a set of equalities to a list of equalities.

POST: Order of equalities equal to order in result of `toLists`.

anyEqTIDs :: AnyEq -> [TID]Source

The threads occurring in an equality.

## Substitution

Substitute a local identifier according to thread identifier equalities.

Substitute a local identifier belonging to an agent variable.

Substitute a local identifier belonging to a message variable.

Substitute an agent id representing an arbitrary agent name.

Substitute the right-hand-side of an agent id equality.

Substitute message constituents according to equalities.

POST: Message normalized w.r.t. `normMsg`.

Substitute both sides of a representable equality.

Retrieve the role of a thread.

The maximal mapped agent identifier.

Check if an equality is reflexive.

True if no equalities are present.

# Mapping Logical Variables

newtype Mapping Source

Constructors

 Mapping FieldsgetMappingEqs :: Equalities

Instances

 Eq Mapping Data Mapping Ord Mapping Show Mapping Typeable Mapping

An empty mapping.

A mapping of logical variables and the corresponding substitution can be represented as an abstract Equalities value. However, it violates the invariant that the domain of the equalities must be invariant under substitution. This is OK, as domain and range of a mapping are from different logical contexts.

Add a mapping from one thread identifier to another one, possibly overriding an existing mapping.

Add a mapping from one thread identifier to another one, possibly overriding an existing mapping.

Add a mapping from one thread identifier to an other role, possibly overriding an existing mapping.

Delete the mapping of the given thread identifier.

Delete the mapping of the given agent identifier.