module Scyther.Protocol (
Id(..)
, Pattern(..)
, Label(..)
, RoleStep(..)
, Role(..)
, Protocol(..)
, RoleStepOrder
, patFMV
, patFAV
, subpatterns
, patternparts
, splitpatterns
, stepPat
, stepLabel
, stepFMV
, stepFAV
, roleFMV
, roleFAV
, lookupRoleStep
, wfRole
, roleOrd
, lookupRole
, stateLocale
, restrictedStateLocale
, weakAtomicityLocale
, weakAtomicityInvariant
, labelOrd
, protoOrd
, ProtoIllformedness
, wfProto
, sptProtoIllformedness
, isaRoleStep
, sptId
, sptLabel
, sptPattern
, sptRoleStep
, sptRole
, sptProtocol
) where
import Safe
import Data.List
import qualified Data.Set as S
import Data.Data
import Control.Monad
import Extension.Prelude
import Text.Isar
newtype Id = Id { getId :: String }
deriving( Eq, Ord, Data, Typeable )
instance Show Id where
show (Id i) = i
data Pattern =
PConst Id
| PFresh Id
| PAVar Id
| PMVar Id
| PHash Pattern
| PTup Pattern Pattern
| PEnc Pattern Pattern
| PSign Pattern Pattern
| PSymK Pattern Pattern
| PShrK Pattern Pattern
| PAsymPK Pattern
| PAsymSK Pattern
deriving( Eq, Ord, Show, Data, Typeable )
newtype Label = Label { getLabel :: String }
deriving( Eq, Ord, Show, Data, Typeable )
data RoleStep =
Send Label Pattern
| Recv Label Pattern
deriving( Eq, Ord, Show, Data, Typeable )
data Role = Role {
roleName :: String
, roleSteps :: [RoleStep]
}
deriving( Eq, Ord, Show, Data, Typeable )
data Protocol = Protocol {
protoName :: String
, protoRoles :: [Role]
}
deriving( Eq, Ord, Show, Data, Typeable )
lookupRole :: String -> Protocol -> Maybe Role
lookupRole name = find ((== name) . roleName) . protoRoles
lookupRoleStep :: String -> Role -> Maybe RoleStep
lookupRoleStep lbl = find ((== lbl) . stepLabel) . roleSteps
stepPat :: RoleStep -> Pattern
stepPat (Send _ pt) = pt
stepPat (Recv _ pt) = pt
stepLabel :: RoleStep -> String
stepLabel (Send l _) = getLabel l
stepLabel (Recv l _) = getLabel l
subpatterns :: Pattern -> S.Set Pattern
subpatterns pt@(PHash pt1) = S.insert pt $ subpatterns pt1
subpatterns pt@(PTup pt1 pt2) = S.insert pt $ subpatterns pt1 `S.union` subpatterns pt2
subpatterns pt@(PEnc pt1 pt2) = S.insert pt $ subpatterns pt1 `S.union` subpatterns pt2
subpatterns pt@(PSign pt1 pt2) = S.insert pt $ subpatterns pt1 `S.union` subpatterns pt2
subpatterns pt@(PSymK pt1 pt2) = S.insert pt $ subpatterns pt1 `S.union` subpatterns pt2
subpatterns pt@(PShrK pt1 pt2) = S.insert pt $ subpatterns pt1 `S.union` subpatterns pt2
subpatterns pt@(PAsymPK pt1) = S.insert pt $ subpatterns pt1
subpatterns pt@(PAsymSK pt1) = S.insert pt $ subpatterns pt1
subpatterns pt = S.singleton pt
patternparts :: Pattern -> S.Set Pattern
patternparts pt@(PTup pt1 pt2) = S.insert pt $ patternparts pt1 `S.union` patternparts pt2
patternparts pt@(PEnc pt1 _) = S.insert pt $ patternparts pt1
patternparts pt@(PSign pt1 _) = S.insert pt $ patternparts pt1
patternparts pt = S.singleton pt
splitpatterns :: Pattern -> S.Set Pattern
splitpatterns (PTup pt1 pt2) = splitpatterns pt1 `S.union` splitpatterns pt2
splitpatterns (PSign pt _ ) = splitpatterns pt
splitpatterns pt = S.singleton pt
patFMV :: Pattern -> S.Set Id
patFMV (PMVar v) = S.singleton v
patFMV (PHash pt) = patFMV pt
patFMV (PTup pt1 pt2) = patFMV pt1 `S.union` patFMV pt2
patFMV (PEnc pt1 pt2) = patFMV pt1 `S.union` patFMV pt2
patFMV (PSign pt1 pt2) = patFMV pt1 `S.union` patFMV pt2
patFMV (PSymK pt1 pt2) = patFMV pt1 `S.union` patFMV pt2
patFMV (PShrK pt1 pt2) = patFMV pt1 `S.union` patFMV pt2
patFMV (PAsymPK pt) = patFMV pt
patFMV (PAsymSK pt) = patFMV pt
patFMV _ = S.empty
stepFMV :: RoleStep -> S.Set Id
stepFMV = patFMV . stepPat
roleFMV :: Role -> S.Set Id
roleFMV = S.unions . map (patFMV . stepPat) . roleSteps
patFAV :: Pattern -> S.Set Id
patFAV (PAVar v) = S.singleton v
patFAV (PHash pt) = patFAV pt
patFAV (PTup pt1 pt2) = patFAV pt1 `S.union` patFAV pt2
patFAV (PEnc pt1 pt2) = patFAV pt1 `S.union` patFAV pt2
patFAV (PSign pt1 pt2) = patFAV pt1 `S.union` patFAV pt2
patFAV (PSymK pt1 pt2) = patFAV pt1 `S.union` patFAV pt2
patFAV (PShrK pt1 pt2) = patFAV pt1 `S.union` patFAV pt2
patFAV (PAsymPK pt) = patFAV pt
patFAV (PAsymSK pt) = patFAV pt
patFAV _ = S.empty
stepFAV :: RoleStep -> S.Set Id
stepFAV = patFAV . stepPat
roleFAV :: Role -> S.Set Id
roleFAV = S.unions . map (patFAV . stepPat) . roleSteps
data ProtoIllformedness =
NonUnique Role
| SendBeforeReceive Role RoleStep Id
| AccessibleLongTermKey Role RoleStep Pattern
deriving( Eq, Ord, Show )
wfRole :: Role -> [ProtoIllformedness]
wfRole role = msum
[ do guard (unique $ roleSteps role)
return $ NonUnique role
, recv_before_send S.empty (roleSteps role)
, msum . map accessibleLongTermKeys $ roleSteps role
]
where
recv_before_send _ [] = mzero
recv_before_send received (step@(Send _ pt) : rs) =
do v <- S.toList $ patFMV pt
guard (v `S.member` received)
return $ SendBeforeReceive role step v
`mplus`
recv_before_send received rs
recv_before_send received (Recv _ pt : rs) =
recv_before_send (patFMV pt `S.union` received) rs
accessibleLongTermKeys step = do
m <- S.toList . patternparts $ stepPat step
key <- case m of
PSymK _ _ -> return m
PAsymSK _ -> return m
_ -> mzero
return $ AccessibleLongTermKey role step key
wfProto :: Protocol -> [ProtoIllformedness]
wfProto = concatMap wfRole . protoRoles
sptProtoIllformedness :: ProtoIllformedness -> Doc
sptProtoIllformedness pif = case pif of
NonUnique role ->
text $ "role '" ++ roleName role ++ "' contains duplicate steps."
SendBeforeReceive role step v ->
text (roleName role) <> colon <->
sptRoleStep Nothing step <> colon <->
text "message variable" <-> quotes (sptId v) <-> text "sent before received."
AccessibleLongTermKey role step _ ->
text (roleName role) <> colon <->
sptRoleStep Nothing step <> colon <->
text "long-term keys must not be accessible."
type RoleStepOrder = [((RoleStep,Role),(RoleStep,Role))]
roleOrd :: Role -> RoleStepOrder
roleOrd role = zip steps (tailDef [] steps)
where
steps = zip (roleSteps role) (repeat role)
labelOrd :: Protocol -> RoleStepOrder
labelOrd proto =
[ (send, recv) | send@(Send l _, _) <- steps,
recv@(Recv l' _, _) <- steps, l == l' ]
where
steps = concat [ zip (roleSteps role) (repeat role) | role <- protoRoles proto ]
protoOrd :: Protocol -> RoleStepOrder
protoOrd proto = labelOrd proto ++ concatMap roleOrd (protoRoles proto)
stateLocale :: Protocol -> String
stateLocale proto = protoName proto ++ "_state"
restrictedStateLocale :: Protocol -> String
restrictedStateLocale proto = "restricted_" ++ protoName proto ++ "_state"
weakAtomicityInvariant :: Protocol -> String
weakAtomicityInvariant proto = "atomic_" ++ protoName proto
weakAtomicityLocale :: Protocol -> String
weakAtomicityLocale proto = "atomic_" ++ stateLocale proto
isaRoleStep :: IsarConf -> Maybe Role -> RoleStep -> Doc
isaRoleStep conf optRole step =
case optRole of
Just role | step `elem` roleSteps role ->
text $ roleName role ++ "_" ++ stepLabel step
_ ->
text name <-> isar conf (Label $ stepLabel step) <-> ppPat (stepPat step)
where
name = case step of Send _ _ -> "Send"; Recv _ _ -> "Recv"
ppPat pt@(PTup _ _) = isar conf pt
ppPat pt = nestShort' "(" ")" (isar conf pt)
instance Isar Id where
isar _ (Id i) = text $ "''"++i++"''"
instance Isar Label where
isar _ (Label l) = text $ "''"++l++"''"
instance Isar Pattern where
isar conf x = case x of
(PConst i) -> text "sC" <-> isar conf i
(PFresh i) -> text "sN" <-> isar conf i
(PAVar i) -> text "sAV" <-> isar conf i
(PMVar i) -> text "sMV" <-> isar conf i
(PHash pt) -> text "PHash" <-> ppTup pt
pt@(PTup _ _) -> ppTup pt
(PEnc m k) -> text "PEnc" <-> sep [ppTup m, ppTup k]
(PSign m k) -> text "PSign" <-> sep [ppTup m, ppTup k]
(PSymK (PAVar a) (PAVar b)) -> text "sK" <-> isar conf a <-> isar conf b
(PSymK a b) -> text "PSymK" <-> sep [ppTup a, ppTup b]
(PShrK a b) -> text "sKbd" <-> keyVar a <-> keyVar b
(PAsymPK (PAVar a)) -> text "sPK" <-> isar conf a
(PAsymPK a) -> text "PAsymPK" <-> ppTup a
(PAsymSK (PAVar a)) -> text "sSK" <-> isar conf a
(PAsymSK a) -> text "PAsymSK" <-> ppTup a
where
ppTup pt@(PTup _ _) = nestShort n left right (fsep $ punctuate comma $ map (isar conf) $ split pt)
ppTup pt = nestShort' "(" ")" (isar conf pt)
split (PTup pt1 pt2) = pt1 : split pt2
split pt = [pt]
(n,left,right)
| isPlainStyle conf = (3, text "<|", text "|>")
| otherwise = (2, symbol "\\<langle>", symbol "\\<rangle>")
keyVar (PAVar v) = parens $ text "AVar" <-> isar conf v
keyVar (PMVar v) = parens $ text "MVar" <-> isar conf v
keyVar _ = error $ "bi-directional key '" ++ show x ++ "' not supported."
instance Isar RoleStep where
isar conf = isaRoleStep conf Nothing
instance Isar Role where
isar conf (Role name steps) =
text "role" <-> text name $-$
text "where" <-> text "\"" <> text name <-> text "=" $-$
nest 2 (
(vcat $ zipWith (<->) separators (map (isar conf) steps)) $-$
text "]\""
)
where
separators = map text ("[" : replicate (length steps 1) ",")
instance Isar Protocol where
isar conf (Protocol name roles) =
vcat (map (($-$ text "") . isar conf) roles) $-$
text "protocol" <-> text name $-$
sep [text "where" <-> text "\"" <> text name <-> text "=", roleSet]
where
roleSet = nestShort' "{" "}\""
(fsep $ punctuate comma $ map (text . roleName) roles)
sptId :: Id -> Doc
sptId = text . getId
sptLabel :: Label -> Doc
sptLabel = text . getLabel
sptPattern :: Pattern -> Doc
sptPattern x = case x of
(PConst i) -> char '\'' <> sptId i <> char '\''
(PFresh i) -> char '~' <> sptId i
(PAVar i) -> sptId i
(PMVar i) -> char '?' <> sptId i
(PHash m) -> text "h" <> ppBetween 3 "(" ")" m
pt@(PTup _ _) -> ppBetween 1 "(" ")" pt
(PEnc m k) -> fcat [ppBetween 1 "{" "}" m, sptPattern k]
(PSign m k) -> fcat [ppBetween 1 "sign{" "}" m, sptPattern k]
(PSymK a b) -> fcat [text "k(", sptPattern a, comma, sptPattern b, text ")"]
(PShrK a b) -> fcat [text "k[", sptPattern a, comma, sptPattern b, text "]"]
(PAsymPK a) -> text "pk" <> ppBetween 1 "(" ")" a
(PAsymSK a) -> text "sk" <> ppBetween 1 "(" ")" a
where
ppBetween n lead finish pt@(PTup _ _) =
fcat . (text lead :) . (++[text finish]) . map (nest n) . punctuate (text ", ") . map sptPattern $ split pt
ppBetween _ lead finish pt = text lead <> sptPattern pt <> text finish
split (PTup pt1 pt2) = pt1 : split pt2
split pt = [pt]
sptRoleStep :: Maybe Role -> RoleStep -> Doc
sptRoleStep optRole step =
case optRole of
Just role | step `elem` roleSteps role ->
text $ roleName role ++ "_" ++ stepLabel step
_ ->
(text $ name ++ "_" ++ stepLabel step) <> ppPat (stepPat step)
where
name = case step of Send _ _ -> "Send"; Recv _ _ -> "Recv"
ppPat pt@(PTup _ _) = sptPattern pt
ppPat pt = nestShort' "(" ")" (sptPattern pt)
sptRole :: Role -> Doc
sptRole(Role name steps) =
text "role" <-> text name $-$
nestBetween 2 lbrace rbrace (
(vcat $ map (sptRoleStep Nothing) steps)
)
sptProtocol :: Protocol -> Doc
sptProtocol (Protocol name roles) =
text "protocol" <-> text name $-$
nestBetween 2 lbrace rbrace (
vcat (intersperse (text "") $ map sptRole roles)
)