Scyther.Message
Description
The actual messages being sent and received over the network are always ground. Here we develop a representation of the denotations of actual messages that may occur during a security proof. This involves symbolically instantiated variables and symbolically inverted keys.
- newtype TID = TID {}
- newtype LocalId = LocalId {
- getLocalId :: (Id, TID)
- newtype Fresh = Fresh {}
- newtype AVar = AVar {}
- newtype MVar = MVar {}
- newtype AgentId = AgentId {}
- data Message
- lidId :: LocalId -> Id
- lidTID :: LocalId -> TID
- avarTID :: AVar -> TID
- mvarTID :: MVar -> TID
- msgFMV :: Message -> [MVar]
- msgFresh :: Message -> [Fresh]
- msgAgentIds :: Message -> [AgentId]
- msgTIDs :: Message -> [TID]
- trivial :: Message -> Bool
- submessages :: Message -> Set Message
- messageparts :: Message -> Set Message
- mapFresh :: (LocalId -> LocalId) -> Fresh -> Fresh
- mapAVar :: (LocalId -> LocalId) -> AVar -> AVar
- mapMVar :: (LocalId -> LocalId) -> MVar -> MVar
- inst :: TID -> Pattern -> Message
- normMsg :: Message -> Message
- splitNonTrivial :: Message -> [Message]
- sptTID :: TID -> Doc
- sptAgentId :: AgentId -> Doc
- sptFresh :: Fresh -> Doc
- sptAVar :: AVar -> Doc
- sptMVar :: MVar -> Doc
- sptMessage :: Message -> Doc
Messages
A logical variable for a thread identifier. Note that these are the only free logical variables being used during proofs. Depending on their context they are either universally or existentially quantified.
A local identifier.
Constructors
| LocalId | |
Fields
| |
A fresh message.
An agent variable.
A message variable.
An agent name identifier
Denotations of messages as they occurr during reasoning. Note that we do not model agents, as in the proofs that we want to do no actual agent reference will be needed.
Note: This is no free algebra due to the nested equalities on thread identifiers and the key-inversion function. However, there is still a most general unifier. The easiest way to understand these messages is to map them to the corresponding Isabelle proof states.
Constructors
| MConst Id | A global constant. |
| MFresh Fresh | A freshly generated message. |
| MAVar AVar | A symbolically instantiated agent variable. |
| MMVar MVar | A symbolically instantiated message variable; |
| MAgent AgentId | Some agent name
|
| MHash Message | Hashing |
| MTup Message Message | Pairing |
| MEnc Message Message | Encryption or signing depending on the key (the second argument) |
| MSymK Message Message | A long-term uni-directional symmetric key |
| MShrK Message Message | A long-term bi-directional symmetric key. |
| MAsymPK Message | A long-term asymmetric public key. |
| MAsymSK Message | A long-term asymmetric private key. |
| MInvKey Message | An application of the key inversion function. |
Queries
msgAgentIds :: Message -> [AgentId]Source
Agent identifiers of a message.
trivial :: Message -> BoolSource
A message is trivial iff it is a tuple or it is guaranteed to be in the initial intruder knowledge (i.e., global constants and agent variables).
PRE: Message must be normalized.
submessages :: Message -> Set MessageSource
The submessages of message.
messageparts :: Message -> Set MessageSource
The accessible submessages of message.
Construction/Transformation
inst :: TID -> Pattern -> MessageSource
Instantiate a pattern to a message. Variables are instantiated
symbolically. The resulting message is guaranteed to be normalized w.r.t
normMsg.
normMsg :: Message -> MessageSource
Normalize a message; i.e., apply key-inversion if possible and swap shared key arguments, if required.
splitNonTrivial :: Message -> [Message]Source
Output
sptAgentId :: AgentId -> DocSource
sptMessage :: Message -> DocSource