cpsa-4.4.7: src/CPSA/Protocol.hs
-- Protocol data structures.
-- Copyright (c) 2009 The MITRE Corporation
--
-- This program is free software: you can redistribute it and/or
-- modify it under the terms of the BSD License as published by the
-- University of California.
module CPSA.Protocol (Event (..), evtCm, evtTerm, evtChan, evtMap, evt,
inbnd, outbnd, evtIsLoad, evtIsStor, evtIsState,
Trace, tterms, originates, originationPos,
generates, generationPos, firstOccursPos,
acquiredPos, gainedPos, genGainedPos, usedPos, insPrecedeOuts,
Role, rname, rvars, rtrace, rnon, rpnon, runique, runiqgen, rabsent,
rconf, rauth, rcomment, rsearch, rnorig, rpnorig, ruorig, rugen, rabs,
rpconf, rpauth, rpriority, mkRole, tchans, varSubset, varsInTerms,
addVars, firstOccurs, paramOfName, envsRoleParams,
AForm (..), NodeTerm, Goal (..), Conj, fvsAForm, fvsConj, fvsAntec, fvsConsq,
aFormOrder, aFreeVars, instantiateAForm, instantiateConj, Rule (..),
Prot, mkProt, pname, alg, pgen, psig, roles, checkForDivergenceInStoreSegments,
nullaryrules, unaryrules, generalrules, rules, userrules, generatedrules,
listenerRole, varsAllAtoms, pcomment) where
import qualified Data.List as L
import qualified Data.Maybe as M
import qualified Data.Set as S
import CPSA.Lib.Utilities
import CPSA.Lib.SExpr
import CPSA.Algebra
import CPSA.Channel
import CPSA.Signature (Sig)
{--
import System.IO.Unsafe
-- import Control.Exception (try)
-- import System.IO.Error (ioeGetErrorString)
z :: Show a => a -> b -> b
z x y = unsafePerformIO (print x >> return y)
zz :: Show a => a -> a
zz x = z x x
zb :: Show a => a -> Bool -> Bool
zb a False = z a False
zb _ b = b
zn :: Show a => a -> Maybe b -> Maybe b
zn x Nothing = z x Nothing
zn _ y = y
zf :: Show a => a -> Bool -> Bool
zf x False = z x False
zf _ y = y
zt :: Show a => a -> Bool -> Bool
zt x True = z x True
zt _ y = y
zl :: Show a => [a] -> [a]
zl a = z (length a) a
-- Also see showst
--}
-- Useful operations on variables
-- Are the vars in ts a subset of the ones in ts'?
varSubset :: [Term] -> [Term] -> Bool
varSubset ts ts' =
all (flip elem (varsInTerms ts')) (varsInTerms ts)
varsInTerms :: [Term] -> [Term]
varsInTerms ts =
foldl addVars [] ts
addVars :: [Term] -> Term -> [Term]
addVars ts t = foldVars (flip adjoin) ts t
-- Message events and traces
data Event
= In !ChMsg -- Inbound message
| Out !ChMsg -- Outbound message
deriving (Show, Eq, Ord)
-- Extract the channel message
evtCm :: Event -> ChMsg
evtCm (In t) = t
evtCm (Out t) = t
-- Dispatch to function based on direction.
evt :: (Term -> a) -> (Term -> a) -> Event -> a
evt inDir outDir evt =
case evt of
In t -> inDir $ cmTerm t
Out t -> outDir $ cmTerm t
-- Extract the term in an event (evt id id).
evtTerm :: Event -> Term
evtTerm (In t) = cmTerm t
evtTerm (Out t) = cmTerm t
-- Extract the channel in an event.
evtChan :: Event -> Maybe Term
evtChan (In t) = cmChan t
evtChan (Out t) = cmChan t
-- Map the term in an event.
evtMap :: (Term -> Term) -> Event -> Event
evtMap f (In t) = In (cmMap f t)
evtMap f (Out t) = Out (cmMap f t)
-- Extract the channel message in an inbound event.
inbnd :: Event -> Maybe ChMsg
inbnd (In t) = Just t
inbnd _ = Nothing
-- Extract the channel message in an outbound event.
outbnd :: Event -> Maybe ChMsg
outbnd (Out t) = Just t
outbnd _ = Nothing
evtIsLoad :: Event -> Bool
evtIsLoad (In (ChMsg ch _)) = isLocn ch
evtIsLoad _ = False
evtIsStor :: Event -> Bool
evtIsStor (Out (ChMsg ch _)) = isLocn ch
evtIsStor _ = False
evtIsState :: Event -> Bool
evtIsState evt = evtIsLoad evt || evtIsStor evt
-- A trace is a list of events. The terms in the trace are
-- stored in causal order.
type Trace = [Event]
-- The set of terms in a trace.
tterms :: Trace -> [Term]
tterms c =
foldl (\ts evt -> adjoin (evtTerm evt) ts) [] c
-- The set of channels in a term
tchans :: Trace -> [Term]
tchans c =
L.nub $ M.catMaybes (map evtChan c)
-- Is the term carried by an event, and is the first one outgoing?
originates :: Term -> Trace -> Bool
originates _ [] = False -- Term is not carried
originates t (Out t' : c) = t `carriedBy` cmTerm t' || originates t c
originates t (In t' : c) = not (t `carriedBy` cmTerm t') && originates t c
-- At what position does a term originate in a trace?
originationPos :: Term -> Trace -> Maybe Int
originationPos t c =
loop 0 c
where
loop _ [] = Nothing -- Term is not carried
loop pos (Out t' : c)
| t `carriedBy` cmTerm t' = Just pos -- Found it
| otherwise = loop (pos + 1) c
loop pos (In t' : c)
| t `carriedBy` cmTerm t' = Nothing -- Term does not originate
| otherwise = loop (pos + 1) c
-- Does the term occur in an event, and is the first one outgoing?
generates :: Term -> Trace -> Bool
generates _ [] = False -- Term does not occur
generates t (Out t' : c) = t `constituent` cmTerm t' || generates t c
generates t (In t' : c) = not (t `constituent` cmTerm t') && generates t c
-- At what position does a term generate in a trace?
generationPos :: Term -> Trace -> Maybe Int
generationPos t c =
loop 0 c
where
maybeInv = invertKey t
testMaybe Nothing _ = False
testMaybe (Just tInv) ct = tInv `constituent` ct
test t ct = t `constituent` ct
loop _ [] = Nothing -- Term does not occur
loop pos (Out t' : c)
| test t (cmTerm t') ||
testMaybe maybeInv (cmTerm t') = Just pos -- Found it
| otherwise = loop (pos + 1) c
loop pos (In t' : c)
| test t (cmTerm t') ||
testMaybe maybeInv (cmTerm t') = Nothing -- Term does not generate
| otherwise = loop (pos + 1) c
firstOccursPos :: Term -> Trace -> Maybe Int
firstOccursPos t c =
loop 0 c
where
maybeInv = invertKey t
testMaybe Nothing _ = False
testMaybe (Just tInv) ct = tInv `occursIn` ct
test t ct = t `occursIn` ct
loop _ [] = Nothing -- Term does not occur
loop pos (Out t' : c)
| test t (cmTerm t') ||
testMaybe maybeInv (cmTerm t') = Just pos -- Found it
| otherwise = loop (pos + 1) c
loop pos (In t' : c)
| test t (cmTerm t') ||
testMaybe maybeInv (cmTerm t') = Just pos -- Found it
-- incoming
| otherwise = loop (pos + 1) c
-- At what position is a term acquired in a trace?
acquiredPos :: Term -> Trace -> Maybe Int
acquiredPos t c =
loop 0 c
where
loop _ [] = Nothing -- Term does not occur
loop pos (In t' : c)
| t `carriedBy` cmTerm t' = Just pos -- Found it
| t `occursIn` cmTerm t' = Nothing -- Occurs but is not carried
| otherwise = loop (pos + 1) c
loop pos (Out t' : c)
| t `occursIn` cmTerm t' = Nothing -- Term occurs in outbound term
| otherwise = loop (pos + 1) c
-- At what position is a term gained in a trace?
gainedPos :: Term -> Trace -> Maybe Int
gainedPos t c =
loop 0 c
where
loop _ [] = Nothing -- Term is not carried
loop pos (Out t' : c)
| t `carriedBy` cmTerm t' = Nothing -- Term is not gained
| otherwise = loop (pos + 1) c
loop pos (In t' : c)
| t `carriedBy` cmTerm t' = Just pos -- Found it
| otherwise = loop (pos + 1) c
-- At what position is a term gained in a trace?
genGainedPos :: Term -> Trace -> Maybe Int
genGainedPos t c =
loop 0 c
where
loop _ [] = Nothing -- Term does not occur
loop pos (Out t' : c)
| t `constituent` cmTerm t' = Nothing -- Term is not gained
| otherwise = loop (pos + 1) c
loop pos (In t' : c)
| t `constituent` cmTerm t' = Just pos -- Found it
| otherwise = loop (pos + 1) c
-- At what position do all of the variables in a term occur in a trace?
usedPos :: Term -> Trace -> Maybe Int
usedPos t c =
loop 0 (varsInTerms [t]) c
where
loop _ _ [] = Nothing
loop pos vars (e : c) =
let vars' = [ x | x <- vars, notElem x (varsInTerms [evtTerm e]) ] in
case vars' of
[] -> Just pos
_ -> loop (pos + 1) vars' c
-- At what position is a channel in a trace?
chanPos :: Term -> Trace -> Maybe Int
chanPos t c =
loop 0 c
where
loop _ [] = Nothing -- Channel is not in trace
loop pos (Out t' : c)
| Just t == cmChan t' = Just pos
| otherwise = loop (pos + 1) c
loop pos (In t' : c)
| Just t == cmChan t' = Just pos
| otherwise = loop (pos + 1) c
insPrecedeOuts :: Int -> Int -> Trace -> Bool
insPrecedeOuts lower upper c =
loopIns (upper-lower) (drop lower c)
where
loopIns _ [] = False -- Ran out too soon
loopIns u (In _ : c)
| u==0 = True -- Safely completed
| otherwise =
loopIns (u-1) c
loopIns u (Out _ : c)
| u==0 = True -- Safely completed
| otherwise =
loopOuts (u-1) c
loopOuts _ [] = False -- Ran out too soon
loopOuts _ (In _ : _) =
False -- Whoa: Went back to Ins
loopOuts u (Out _ : c)
| u==0 = True -- Safely completed
| otherwise =
loopOuts (u-1) c
data Role = Role
{ rname :: !String,
rvars :: ![Term], -- Set of role variables
-- Events in causal order
rtrace :: ![Event],
-- Set of non-originating atoms, possibly with a trace length
rnon :: ![(Maybe Int, Term)], -- that says when to inherit the atom
rpnon :: ![(Maybe Int, Term)], -- that says when to inherit the atom
runique :: ![Term], -- Set of uniquely originating atoms
runiqgen :: ![Term], -- Set of uniquely generated atoms
rabsent :: ![(Term, Term)], -- Role absence
rconf :: ![Term], -- Confidential channels
rauth :: ![Term], -- Authenticated channels
rcomment :: [SExpr ()], -- Comments from the input
rsearch :: Bool, -- True when suggesting reverse test node search
rnorig :: [(Term, Int)], -- Nons plus origination position
rpnorig :: [(Term, Int)], -- Penetrator nons plus origination position
ruorig :: [(Term, Int)], -- Uniques plus origination position
rugen :: [(Term, Int)], -- Uniq gens plus generation position
rabs :: [(Term, Term, Int)], -- Absent plus position
rpconf :: [(Term, Int)], -- Confidentials plus origination position
rpauth :: [(Term, Int)], -- Authenticated plus origination position
rpriority :: [Int] } -- List of all priorities
deriving Show
defaultPriority :: Int
defaultPriority = 5
-- | Compute the index of the first event at which the given variable
-- occurs in a trace.
firstOccursAt :: Term -> Trace -> Maybe Int
firstOccursAt t c =
loop 0 c
where
loop _ [] = Nothing
loop i (e : c)
| any (occursIn t) (cmTerms $ evtCm e) = Just i
| otherwise = loop (i + 1) c
-- The empty role name is used with listener strands. All roles in a
-- protocol must have a name with more than one character.
-- The lists vars, non, pnon, and unique are sets and should never
-- contain duplicate terms.
-- Create a role
mkRole :: String -> [Term] -> Trace ->
[(Maybe Int, Term)] -> [(Maybe Int, Term)] -> [Term] -> [Term] ->
[(Term, Term)] -> [Term] -> [Term] ->
[SExpr ()] -> [(Int, Int)] -> Bool -> Role
mkRole name vars trace non pnon unique uniqgen absent
conf auth comment priority rev =
Role { rname = name,
rvars = L.nub vars, -- Every variable here must
rtrace = trace, -- occur in the trace.
rnon = non,
rpnon = pnon,
runique = L.nub unique,
runiqgen = uniqgen',
rconf = L.nub conf,
rauth = L.nub auth,
rcomment = comment,
rnorig = map addNonOrig $ nonNub non,
rpnorig = map addNonOrig $ nonNub pnon,
ruorig = map addUniqueOrig $ L.nub unique,
rugen = map addUniqueGen uniqgen',
rabs = map addAbsentPos absent',
rpconf = map addChanPos $ L.nub conf,
rpauth = map addChanPos $ L.nub auth,
rpriority = addDefaultPrio priority,
rsearch = rev,
rabsent = absent'
}
where
uniqgen' = L.nub uniqgen
absent' = L.nub (traceAbsent trace uniqgen' ++ absent)
addUniqueOrig t =
case originationPos t trace of
Just p -> (t, p)
Nothing -> error "Protocol.mkRole: Atom does not uniquely originate"
addUniqueGen t =
case generationPos t trace of
Just p -> (t, p)
Nothing -> error "Protocol.mkRole: Atom does not uniquely generate"
addNonOrig (len, t) =
case usedPos t trace of
Nothing -> error "Protocol.mkRole: Atom variables not in trace"
Just p ->
case len of
Nothing -> (t, p)
Just len | len >= p -> (t, len)
| otherwise -> error msg
where
msg = "Protocol.mkRole: Position for atom too early in trace"
addAbsentPos (x, y) =
case (usedPos x trace, usedPos y trace) of
(Just xp, Just yp) -> (x, y, max xp yp)
_ -> error msg
where
msg = "Protocol.mkRole: Absence variable not in trace"
addChanPos t =
case chanPos t trace of
Just p -> (t, p)
Nothing -> error "Protocol.mkRole: Channel not in trace"
-- Drop non-origination assumptions for the same atom.
nonNub nons =
reverse $ foldl f [] nons
where
f acc non@(_, t)
| any (\(_, t') -> t == t') acc = acc
| otherwise = non : acc
addDefaultPrio priority =
map f (nats $ length trace)
where
f n =
case lookup n priority of
Nothing -> defaultPriority
Just p -> p
{--
error
("Protocol.mkRole: Atom " ++ (show v) ++
" does not generate")
--}
traceAbsent :: Trace -> [Term] -> [(Term, Term)]
traceAbsent trace ugens =
concatMap indz_ininsts $ filter isNum ugens
where
indz_ininsts v =
case generationPos v trace of
Nothing -> indz_ininsts_var v 0
Just p -> indz_ininsts_var v p
-- ind-zero instances for a specific variable v that generates at height p
indz_ininsts_var v p =
map (\t -> (v, t)) (numsUpTo p)
-- returns a list of numeric subterms of all messages prior to height p.
numsUpTo p =
S.toList $ foldl f S.empty $ take p trace
where
f ts evt = S.union ts $ subNums $ evtTerm evt
-- Return just the index of the first occurrence of v in the trace, or
-- nothing.
firstOccurs :: Term -> Role -> Maybe Int
firstOccurs v r = firstOccursAt v (rtrace r)
paramOfName :: String -> Role -> Maybe Term
paramOfName name rl =
seek (rvars rl)
where
seek [] = Nothing
seek (v : rest)
| name == varName v = Just v -- $ z v v
| otherwise = seek rest
paramVarPairs :: Role -> [Term] -> [(Term,Term)]
paramVarPairs rl =
foldl
(\soFar v ->
case paramOfName (varName v) rl of
Nothing -> soFar
Just p -> (p,v) : soFar)
[]
envsRoleParams :: Role -> [Term] -> Env
envsRoleParams rl vars =
envOfParamVarPairs $ paramVarPairs rl vars
-- For two events, determine if, ignoring the msg contents, they could
-- possibly unify. If so, determine if they are both non-store
-- events, if only one is, or if both are.
data AgreeData = Disagree
| NonStore
| HalfStore
| FullStore
divergeAgreeStore :: Event -> AgreeData
divergeAgreeStore (Out (ChMsg ch2 _))
| isLocn ch2 = FullStore
| otherwise = HalfStore
divergeAgreeStore _ = HalfStore
divergeAgreeOutChan :: Event -> AgreeData
divergeAgreeOutChan (Out (ChMsg ch2 _))
| isLocn ch2 = HalfStore
| otherwise = NonStore
divergeAgreeOutChan _ = Disagree
divergeAgreeOutPlain :: Event -> AgreeData
divergeAgreeOutPlain (Out (ChMsg ch2 _))
| isLocn ch2 = HalfStore
| otherwise = Disagree
divergeAgreeOutPlain (Out (Plain _)) = NonStore
divergeAgreeOutPlain _ = Disagree
divergeAgreeInChan :: Event -> AgreeData
divergeAgreeInChan (Out (ChMsg ch2 _))
| isLocn ch2 = HalfStore
| otherwise = Disagree
divergeAgreeInChan (Out (Plain _)) = Disagree
divergeAgreeInChan (In (ChMsg _ _)) = NonStore
divergeAgreeInChan _ = Disagree
divergeAgreeInPlain :: Event -> AgreeData
divergeAgreeInPlain (Out (ChMsg ch2 _))
| isLocn ch2 = HalfStore
| otherwise = Disagree
divergeAgreeInPlain (In (Plain _)) = NonStore
divergeAgreeInPlain _ = Disagree
--
divergeEventsAgree :: Event -> Event -> AgreeData
divergeEventsAgree (Out (ChMsg ch1 _))
| isLocn ch1 = divergeAgreeStore
| otherwise = divergeAgreeOutChan
divergeEventsAgree (Out _) = divergeAgreeOutPlain
divergeEventsAgree (In (ChMsg _ _)) = divergeAgreeInChan
divergeEventsAgree (In _) = divergeAgreeInPlain
-- By a varTrail, we mean a list of terms without repetitions
-- consisting only of sorted variables, and we want to apply
-- substitutions to them, assuring that the subst is acting as a
-- renaming on them. This means that it should be convertible, and it
-- not yield repeated entries, i.e. it should be injective on these
-- variables.
type VarTrail = [Term]
substVarTrail :: Gen -> Subst -> VarTrail -> Maybe VarTrail
substVarTrail gen subst varList =
case mapM (substInvertibly gen subst) varList of
Nothing -> Nothing
Just image ->
if repeatedEntries image then Nothing
else if any (not . isVar) image then Nothing
else Just image
where
repeatedEntries [] = False
repeatedEntries (a : rest) =
a `elem` rest ||
repeatedEntries rest
eventVars :: Event -> [Term]
eventVars e =
foldr (\t soFar -> union (sortedVarsIn t) soFar)
[]
(cmTerms $ evtCm e)
data DivergeOutcome = Safe | Unsafe Int
combineOutcomes :: [DivergeOutcome] -> DivergeOutcome
combineOutcomes [] = Safe
combineOutcomes (Unsafe i : _) = Unsafe i
combineOutcomes (Safe : rest) = combineOutcomes rest
type DivergeRest = VarTrail -> Gen -> Bool -> Int -> DivergeOutcome
divergeDescendSensitive :: Event -> Event -> [Event] -> [Event] -> DivergeRest
divergeDescendSensitive e1 e2 rest1 rest2 vars g _ i =
let gsubsts = cmUnify (evtCm e1) (evtCm e2) (g,emptySubst) in
case mapM (\(g,subst) -> substVarTrail g subst vars) gsubsts of
Nothing -> Unsafe i
Just varLists ->
combineOutcomes
(map
(\((g,s),vars) -> -- vars are already substituted above
let sub = substitute s in
let newVars = union (eVars sub e1)
(union (eVars sub e2) vars) in
(divergeLoop
(map (evtMap $ sub) rest1)
(map (evtMap $ sub) rest2)
newVars g True (i+1)))
$ zip gsubsts varLists)
where
eVars f e = L.nub $ map f $ eventVars e
divergeDescend :: Event -> Event -> [Event] -> [Event] -> DivergeRest
divergeDescend e1 e2 rest1 rest2 vars g inStore i =
let gsubsts = cmUnify (evtCm e1) (evtCm e2) (g,emptySubst) in
combineOutcomes
(map
(\((g,s)) -> -- vars are not yet substituted
let sub = substitute s in
let newVars = union (eVars sub e1)
$ union (eVars sub e2) $ map sub vars in
(divergeLoop
(map (evtMap sub) rest1)
(map (evtMap sub) rest2)
newVars g inStore (i+1)))
gsubsts)
where
eVars f e = L.nub $ map f $ eventVars e
divergeLoop :: [Event] -> [Event] -> DivergeRest
divergeLoop [] [] _ _ _ _ = Safe
divergeLoop [] _ _ _ inStore i = if inStore then Unsafe i else Safe
divergeLoop _ [] _ _ inStore i = if inStore then Unsafe i else Safe
divergeLoop (e1 : rest1) (e2 : rest2) vars g inStore i =
case divergeEventsAgree e1 e2 of
HalfStore -> if inStore then Unsafe i else Safe
Disagree -> Safe
-- A NonStore makes inStore false the *next* time through
NonStore -> divergeDescend e1 e2 rest1 rest2 vars g False i
-- A FullStore makes inStore true the *next* time through
FullStore ->
if inStore
then divergeDescendSensitive
e1 e2 rest1 rest2 vars g True i
else divergeDescend
e1 e2 rest1 rest2 vars g True i
{--
divergeLoop :: [Event] -> [Event] -> DivergeRest
divergeLoop tr1 tr2 vars g inStore i
| i == L.length tr1 && i == L.length tr2 = Safe
| i == L.length tr1 || i == L.length tr2 =
if inStore then Unsafe i else Safe
| otherwise =
let e1 = tr1 !! i in
let e2 = tr2 !! i in
--}
rolesDivergeInStoreSeg :: Role -> Role -> Gen -> DivergeOutcome
rolesDivergeInStoreSeg r1 r2 g =
divergeLoop (rtrace r1) (rtrace r2) []
g False 0
checkForDivergenceInStoreSegments :: Prot -> Maybe (String, String, Int)
checkForDivergenceInStoreSegments p =
loop $ L.reverse $ roles p
where
loop [] = Nothing
loop (r : rest) =
case subloop r rest of
Nothing -> loop rest
Just (name, name', i) -> Just (name, name', i)
subloop _ [] = Nothing
subloop r (r' : rest) =
case rolesDivergeInStoreSeg r r' (pgen p) of
Unsafe i -> Just (rname r, rname r', i)
Safe -> subloop r rest
-- Security Goals
-- Syntax for the atomic formulas
data AForm
= Length Role Term Term
| Param Role Term Int Term Term -- role param first-height strand value
| Prec NodeTerm NodeTerm
| Non Term
| Pnon Term
| Uniq Term
| UniqAt Term NodeTerm
| Ugen Term
| UgenAt Term NodeTerm
| GenStV Term
| Conf Term
| Auth Term
| Commpair NodeTerm NodeTerm
| SameLocn NodeTerm NodeTerm
| StateNode NodeTerm
| Trans NodeTerm
| LeadsTo NodeTerm NodeTerm
| AFact String [Term]
| Equals Term Term
| Component Term Term
deriving Show
type NodeTerm = (Term, Term)
data Goal =
Goal { uvars :: [Term], -- Universally quantified variables
antec :: [AForm], -- Antecedent
-- Consequent with existentially quantified variables
consq :: [([Term], [AForm])],
concl :: [[AForm]] } -- Conclusion
deriving Show
type Conj = [(Pos, AForm)]
-- -- A HornRule has at most one disjunct, no existential
-- data HornRule =
-- HornRule { hruvars :: [Term], -- Universally quantified variables
-- hrantec :: [AForm], -- Antecedent
-- -- Consequent has no existentially quantified variables
-- hrconsq :: [AForm], -- Conjunction of atomic
-- -- formulas
-- hrname :: !String,
-- hrcomment :: [SExpr ()] }
-- deriving Show
--
-- -- A general rule has more than one disjunct in conclusion,
-- -- or else existentially bound vars
--
-- data GenRule =
-- GenRule { gruvars :: [Term], -- Universally quantified variables
-- grantec :: [AForm], -- Antecedent
-- -- Consequent with existentially quantified variables
-- -- Outer list is disjuncts, each w existential bindings
-- grconsq :: [([Term], [AForm])],
-- grname :: !String,
-- grcomment :: [SExpr ()] }
-- deriving Show
--
--
-- -- data Rule
-- -- = Rule { rlname :: String, -- Name of rule
-- -- rlgoal :: Goal, -- Sentence
-- -- rlcomment :: [SExpr ()] }
-- -- deriving Show
indexOfAForm :: AForm -> Int
indexOfAForm (Length _ _ _) = 0
indexOfAForm (Param _ _ _ _ _) = 1
indexOfAForm (Prec _ _) = 2
indexOfAForm (Non _) = 3
indexOfAForm (Pnon _) = 4
indexOfAForm (Uniq _) = 5
indexOfAForm (UniqAt _ _) = 6
indexOfAForm (GenStV _) = 7
indexOfAForm (Conf _) = 8
indexOfAForm (Auth _) = 9
indexOfAForm (Commpair _ _) = 10
indexOfAForm (SameLocn _ _) = 11
indexOfAForm (StateNode _) = 12
indexOfAForm (Trans _) = 13
indexOfAForm (LeadsTo _ _) = 14
indexOfAForm (AFact _ _) = 15
indexOfAForm (Equals _ _) = 16
indexOfAForm (Component _ _) = 17
indexOfAForm (Ugen _) = 18
indexOfAForm (UgenAt _ _) = 19
aFormOrder :: AForm -> AForm -> Ordering
aFormOrder f f' = compare (indexOfAForm f) (indexOfAForm f')
--
-- let i' = in
-- case i == i' of
-- True -> EQ
-- False ->
-- (case i < i' of
-- True -> LT
-- False -> GT)
{-- -- Unmaintainable version that we had before!
-- Ordering used to sort by constructor order.
aFormOrder :: AForm -> AForm -> Ordering
aFormOrder (Length _ _ _) (Length _ _ _) = EQ
aFormOrder (Length _ _ _) (Param _ _ _ _ _) = LT
aFormOrder (Length _ _ _) (Prec _ _) = LT
aFormOrder (Length _ _ _) (Non _) = LT
aFormOrder (Length _ _ _) (Pnon _) = LT
aFormOrder (Length _ _ _) (Uniq _) = LT
aFormOrder (Length _ _ _) (UniqAt _ _) = LT
aFormOrder (Length _ _ _) (GenStV _) = LT
aFormOrder (Length _ _ _) (Conf _ ) = LT
aFormOrder (Length _ _ _) (Auth _) = LT
aFormOrder (Length _ _ _) (AFact _ _) = LT
aFormOrder (Length _ _ _) (Equals _ _) = LT
aFormOrder (Param _ _ _ _ _) (Length _ _ _) = GT
aFormOrder (Param _ _ _ _ _) (Param _ _ _ _ _) = EQ
aFormOrder (Param _ _ _ _ _) (Prec _ _) = LT
aFormOrder (Param _ _ _ _ _) (Non _) = LT
aFormOrder (Param _ _ _ _ _) (Pnon _) = LT
aFormOrder (Param _ _ _ _ _) (Uniq _) = LT
aFormOrder (Param _ _ _ _ _) (UniqAt _ _) = LT
aFormOrder (Param _ _ _ _ _) (GenStV _) = LT
aFormOrder (Param _ _ _ _ _) (Conf _ ) = LT
aFormOrder (Param _ _ _ _ _) (Auth _) = LT
aFormOrder (Param _ _ _ _ _) (AFact _ _) = LT
aFormOrder (Param _ _ _ _ _) (Equals _ _) = LT
aFormOrder (Prec _ _) (Length _ _ _) = GT
aFormOrder (Prec _ _) (Param _ _ _ _ _) = GT
aFormOrder (Prec _ _) (Prec _ _) = EQ
aFormOrder (Prec _ _) (Non _) = LT
aFormOrder (Prec _ _) (Pnon _) = LT
aFormOrder (Prec _ _) (Uniq _) = LT
aFormOrder (Prec _ _) (UniqAt _ _) = LT
aFormOrder (Prec _ _) (GenStV _) = LT
aFormOrder (Prec _ _) (Conf _ ) = LT
aFormOrder (Prec _ _) (Auth _) = LT
aFormOrder (Prec _ _) (AFact _ _) = LT
aFormOrder (Prec _ _) (Equals _ _) = LT
aFormOrder (Non _) (Length _ _ _) = GT
aFormOrder (Non _) (Param _ _ _ _ _) = GT
aFormOrder (Non _) (Prec _ _) = GT
aFormOrder (Non _) (Non _) = EQ
aFormOrder (Non _) (Pnon _) = LT
aFormOrder (Non _) (Uniq _) = LT
aFormOrder (Non _) (UniqAt _ _) = LT
aFormOrder (Non _) (GenStV _) = LT
aFormOrder (Non _) (Conf _ ) = LT
aFormOrder (Non _) (Auth _) = LT
aFormOrder (Non _) (AFact _ _) = LT
aFormOrder (Non _) (Equals _ _) = LT
aFormOrder (Pnon _) (Length _ _ _) = GT
aFormOrder (Pnon _) (Param _ _ _ _ _) = GT
aFormOrder (Pnon _) (Prec _ _) = GT
aFormOrder (Pnon _) (Non _) = GT
aFormOrder (Pnon _) (Pnon _) = EQ
aFormOrder (Pnon _) (Uniq _) = LT
aFormOrder (Pnon _) (UniqAt _ _) = LT
aFormOrder (Pnon _) (GenStV _) = LT
aFormOrder (Pnon _) (Conf _ ) = LT
aFormOrder (Pnon _) (Auth _) = LT
aFormOrder (Pnon _) (AFact _ _) = LT
aFormOrder (Pnon _) (Equals _ _) = LT
aFormOrder (Uniq _) (Length _ _ _) = GT
aFormOrder (Uniq _) (Param _ _ _ _ _) = GT
aFormOrder (Uniq _) (Prec _ _) = GT
aFormOrder (Uniq _) (Non _) = GT
aFormOrder (Uniq _) (Pnon _) = GT
aFormOrder (Uniq _) (Uniq _) = EQ
aFormOrder (Uniq _) (UniqAt _ _) = LT
aFormOrder (Uniq _) (GenStV _) = LT
aFormOrder (Uniq _) (Conf _ ) = LT
aFormOrder (Uniq _) (Auth _) = LT
aFormOrder (Uniq _) (AFact _ _) = LT
aFormOrder (Uniq _) (Equals _ _) = LT
aFormOrder (UniqAt _ _) (Length _ _ _) = GT
aFormOrder (UniqAt _ _) (Param _ _ _ _ _) = GT
aFormOrder (UniqAt _ _) (Prec _ _) = GT
aFormOrder (UniqAt _ _) (Non _) = GT
aFormOrder (UniqAt _ _) (Pnon _) = GT
aFormOrder (UniqAt _ _) (Uniq _) = GT
aFormOrder (UniqAt _ _) (UniqAt _ _) = EQ
aFormOrder (UniqAt _ _) (GenStV _ ) = LT
aFormOrder (UniqAt _ _) (Conf _ ) = LT
aFormOrder (UniqAt _ _) (Auth _) = LT
aFormOrder (UniqAt _ _) (AFact _ _) = LT
aFormOrder (UniqAt _ _) (Equals _ _) = LT
aFormOrder (GenStV _) (Length _ _ _) = GT
aFormOrder (GenStV _) (Param _ _ _ _ _) = GT
aFormOrder (GenStV _) (Prec _ _) = GT
aFormOrder (GenStV _) (Non _) = GT
aFormOrder (GenStV _) (Pnon _) = GT
aFormOrder (GenStV _) (Uniq _) = GT
aFormOrder (GenStV _) (UniqAt _ _) = GT
aFormOrder (GenStV _) (GenStV _ ) = EQ
aFormOrder (GenStV _) (Conf _ ) = LT
aFormOrder (GenStV _) (Auth _) = LT
aFormOrder (GenStV _) (AFact _ _) = LT
aFormOrder (GenStV _) (Equals _ _) = LT
aFormOrder (Conf _ ) (Length _ _ _) = GT
aFormOrder (Conf _ ) (Param _ _ _ _ _) = GT
aFormOrder (Conf _ ) (Prec _ _) = GT
aFormOrder (Conf _ ) (Non _) = GT
aFormOrder (Conf _ ) (Pnon _) = GT
aFormOrder (Conf _ ) (Uniq _) = GT
aFormOrder (Conf _ ) (UniqAt _ _) = GT
aFormOrder (Conf _ ) (GenStV _) = GT
aFormOrder (Conf _ ) (Conf _ ) = EQ
aFormOrder (Conf _ ) (Auth _) = LT
aFormOrder (Conf _ ) (AFact _ _) = LT
aFormOrder (Conf _ ) (Equals _ _) = LT
aFormOrder (Auth _) (Length _ _ _) = GT
aFormOrder (Auth _) (Param _ _ _ _ _) = GT
aFormOrder (Auth _) (Prec _ _) = GT
aFormOrder (Auth _) (Non _) = GT
aFormOrder (Auth _) (Pnon _) = GT
aFormOrder (Auth _) (Uniq _) = GT
aFormOrder (Auth _) (UniqAt _ _) = GT
aFormOrder (Auth _) (GenStV _) = GT
aFormOrder (Auth _) (Conf _ ) = GT
aFormOrder (Auth _) (Auth _) = EQ
aFormOrder (Auth _) (AFact _ _) = LT
aFormOrder (Auth _) (Equals _ _) = LT
aFormOrder (AFact _ _) (Length _ _ _) = GT
aFormOrder (AFact _ _) (Param _ _ _ _ _) = GT
aFormOrder (AFact _ _) (Prec _ _) = GT
aFormOrder (AFact _ _) (Non _) = GT
aFormOrder (AFact _ _) (Pnon _) = GT
aFormOrder (AFact _ _) (Uniq _) = GT
aFormOrder (AFact _ _) (UniqAt _ _) = GT
aFormOrder (AFact _ _) (GenStV _) = GT
aFormOrder (AFact _ _) (Conf _ ) = GT
aFormOrder (AFact _ _) (Auth _) = GT
aFormOrder (AFact _ _) (AFact _ _) = EQ
aFormOrder (AFact _ _) (Equals _ _) = LT
aFormOrder (Equals _ _) (Length _ _ _) = GT
aFormOrder (Equals _ _) (Param _ _ _ _ _) = GT
aFormOrder (Equals _ _) (Prec _ _) = GT
aFormOrder (Equals _ _) (Non _) = GT
aFormOrder (Equals _ _) (Pnon _) = GT
aFormOrder (Equals _ _) (Uniq _) = GT
aFormOrder (Equals _ _) (UniqAt _ _) = GT
aFormOrder (Equals _ _) (GenStV _) = GT
aFormOrder (Equals _ _) (Conf _ ) = GT
aFormOrder (Equals _ _) (Auth _) = GT
aFormOrder (Equals _ _) (AFact _ _) = GT
aFormOrder (Equals _ _) (Equals _ _) = EQ
--}
aFreeVars :: [Term] -> AForm -> [Term]
aFreeVars vars (Length _ z _) = addVars vars z
aFreeVars vars (Param _ _ _ z t) = addVars (addVars vars z) t
aFreeVars vars (Prec (x, i) (y, j)) = addVars (addVars (addVars (addVars vars x) y) i) j
aFreeVars vars (Non t) = addVars vars t
aFreeVars vars (Pnon t) = addVars vars t
aFreeVars vars (Uniq t) = addVars vars t
aFreeVars vars (UniqAt t (z, i)) = addVars (addVars (addVars vars t) z) i
aFreeVars vars (Ugen t) = addVars vars t
aFreeVars vars (UgenAt t (z, i)) = addVars (addVars (addVars vars t) z) i
aFreeVars vars (GenStV t) = addVars vars t
aFreeVars vars (Conf t) = addVars vars t
aFreeVars vars (Auth t) = addVars vars t
aFreeVars vars (AFact _ ft) = foldl addVars vars ft
aFreeVars vars (Equals x y) = addVars (addVars vars x) y
aFreeVars vars (Component x y) = addVars (addVars vars x) y
aFreeVars vars (Commpair (s,t) (s',t')) = addVars (addVars (addVars (addVars vars s) t) s') t'
aFreeVars vars (SameLocn (s,t) (s',t')) = addVars (addVars (addVars (addVars vars s) t) s') t'
aFreeVars vars (StateNode (s,t)) = addVars (addVars vars s) t
aFreeVars vars (Trans (s,t)) = addVars (addVars vars s) t
aFreeVars vars (LeadsTo (s,t) (s',t')) = addVars (addVars (addVars (addVars vars s) t) s') t'
instantiateAForm :: Env -> AForm -> AForm
instantiateAForm e (Length rl z v) =
(Length rl (instantiate e z) (instantiate e v))
instantiateAForm e (Param rl p i z t) =
(Param rl p i (instantiate e z) (instantiate e t))
instantiateAForm e (Prec (x, i) (y, j)) =
(Prec
((instantiate e x), (instantiate e i))
((instantiate e y), (instantiate e j)))
instantiateAForm e (Non t) =
(Non (instantiate e t))
instantiateAForm e (Pnon t) =
(Pnon (instantiate e t))
instantiateAForm e (Uniq t) =
(Uniq (instantiate e t))
instantiateAForm e (UniqAt t (z, i)) =
(UniqAt
(instantiate e t)
((instantiate e z), (instantiate e i)))
instantiateAForm e (Ugen t) =
(Ugen (instantiate e t))
instantiateAForm e (UgenAt t (z, i)) =
(UgenAt
(instantiate e t)
((instantiate e z), (instantiate e i)))
instantiateAForm e (GenStV t) =
(GenStV (instantiate e t))
instantiateAForm e (Conf t) =
(Conf (instantiate e t))
instantiateAForm e (Auth t) =
(Auth (instantiate e t))
instantiateAForm e (AFact pred ft) =
(AFact pred (map (instantiate e) ft))
instantiateAForm e (Equals x y) =
(Equals
(instantiate e x)
(instantiate e y))
instantiateAForm e (Component x y) =
(Component
(instantiate e x)
(instantiate e y))
instantiateAForm e (Commpair (s,t) (s',t')) =
(Commpair
((instantiate e s), (instantiate e t))
((instantiate e s'), (instantiate e t')))
instantiateAForm e (SameLocn (s,t) (s',t')) =
(SameLocn
((instantiate e s), (instantiate e t))
((instantiate e s'), (instantiate e t')))
instantiateAForm e (StateNode (s,t)) =
(StateNode
((instantiate e s), (instantiate e t)))
instantiateAForm e (Trans (s,t)) =
(Trans
((instantiate e s), (instantiate e t)))
instantiateAForm e (LeadsTo (s,t) (s',t')) =
(LeadsTo
((instantiate e s), (instantiate e t))
((instantiate e s'), (instantiate e t')))
instantiateConj :: Env -> Conj -> Conj
instantiateConj e =
map (\(p,a) -> (p, instantiateAForm e a))
fvsAForm :: AForm -> [Term]
fvsAForm (Length _ z l) = L.nub $ sortedVarsIn z ++ sortedVarsIn l
fvsAForm (Param _ _ _ z v) = L.nub $ sortedVarsIn z ++ sortedVarsIn v
fvsAForm (Prec (z1,i1) (z2,i2)) =
L.nub $ sortedVarsIn z1 ++ sortedVarsIn i1 ++
sortedVarsIn z2 ++ sortedVarsIn i2
fvsAForm (Non t) = L.nub $ sortedVarsIn t
fvsAForm (Pnon t) = L.nub $ sortedVarsIn t
fvsAForm (Uniq t) = L.nub $ sortedVarsIn t
fvsAForm (Ugen t) = L.nub $ sortedVarsIn t
fvsAForm (UniqAt t (z1,i1)) =
L.nub $ sortedVarsIn t ++ sortedVarsIn z1 ++ sortedVarsIn i1
fvsAForm (UgenAt t (z1,i1)) =
L.nub $ sortedVarsIn t ++ sortedVarsIn z1 ++ sortedVarsIn i1
fvsAForm (GenStV t) = L.nub $ sortedVarsIn t
fvsAForm (Conf t) = L.nub $ sortedVarsIn t
fvsAForm (Auth t) = L.nub $ sortedVarsIn t
fvsAForm (Commpair (z1,i1) (z2,i2)) =
L.nub $ sortedVarsIn z1 ++ sortedVarsIn i1 ++
sortedVarsIn z2 ++ sortedVarsIn i2
fvsAForm (SameLocn (z1,i1) (z2,i2)) =
L.nub $ sortedVarsIn z1 ++ sortedVarsIn i1 ++
sortedVarsIn z2 ++ sortedVarsIn i2
fvsAForm (LeadsTo (z1,i1) (z2,i2)) =
L.nub $ sortedVarsIn z1 ++ sortedVarsIn i1 ++
sortedVarsIn z2 ++ sortedVarsIn i2
fvsAForm (StateNode (z1,i1)) =
L.nub $ sortedVarsIn z1 ++ sortedVarsIn i1
fvsAForm (Trans (z1,i1)) =
L.nub $ sortedVarsIn z1 ++ sortedVarsIn i1
fvsAForm (Equals t1 t2) = L.nub $ sortedVarsIn t1 ++ sortedVarsIn t2
fvsAForm (Component t1 t2) = L.nub $ sortedVarsIn t1 ++ sortedVarsIn t2
fvsAForm (AFact _ ts) = L.nub $ concatMap sortedVarsIn ts
fvsConj :: Conj -> [Term]
fvsConj c = L.nub $ concatMap fvsAForm $ map snd c
fvsAntec :: [AForm] -> [Term]
fvsAntec afs = L.nub $ concatMap fvsAForm afs
fvsConsq :: [([Term], [AForm])] -> [Term]
fvsConsq exs = L.nub $ concatMap (\(evs,c) -> (fvsAntec c) L.\\ evs) exs
data Rule
= Rule { rlname :: String, -- Name of rule
rlgoal :: Goal, -- Sentence
rlcomment :: [SExpr ()] }
deriving Show
-- data HGRule = H HornRule
-- | G GenRule
data RuleKind = NullaryRule | UnaryRule | GeneralRule
classifyRule :: Rule -> RuleKind
classifyRule r =
let gl = rlgoal r in
case consq gl of
[] -> NullaryRule -- null disjunction = false
[([],_)] -> UnaryRule -- single disjunct, no existentials
_ -> GeneralRule -- multiple branches or any existentials
-- partition the rules given into three lists,
-- containing resp.
-- (i) those with empty (false) conclusion;
-- (ii) those with unary, existential-free conclusion;
-- (iii) those with multiple disjuncts or existential quantifiers
classifyRules :: [Rule] -> ([Rule],[Rule],[Rule])
classifyRules =
foldl
(\(nullSoFar,unarySoFar,genSoFar) rl ->
case classifyRule rl of
NullaryRule -> (rl : nullSoFar, unarySoFar, genSoFar)
UnaryRule -> (nullSoFar, rl : unarySoFar, genSoFar)
GeneralRule -> (nullSoFar, unarySoFar, rl : genSoFar))
([],[],[])
-- Protocols
data Prot
= Prot { pname :: !String, -- Name of the protocol
alg :: !String, -- Name of the algebra
pgen :: !Gen, -- Initial variable generator
psig :: !Sig, -- The signature
roles :: ![Role], -- Non-listener roles of a protocol
listenerRole :: Role,
nullaryrules :: ![Rule], -- Protocol rules: False conclusion
unaryrules :: ![Rule], -- Protocol rules: no branching
-- or existential
generalrules :: ![Rule], -- Protocol rules: may branch
-- and introduce ex. bound vars
userrules :: ![Rule], -- those rules explicitly
-- written by the user
generatedrules :: ![Rule], -- those rules created by
-- the loader
varsAllAtoms :: !Bool, -- Are all role variables atoms?
pcomment :: [SExpr ()] } -- Comments from the input
deriving Show
-- Callers should ensure every role has a distinct name.
mkProt :: String -> String -> Gen -> Sig ->
[Role] -> Role -> [Rule] -> [Rule] -> [Rule] -> [SExpr ()] -> Prot
mkProt name alg gen sig roles lrole rules written generated comment =
let (nrs,urs,grs) = classifyRules rules in
Prot { pname = name, alg = alg, pgen = gen, psig = sig, roles = roles,
listenerRole = lrole,
nullaryrules = nrs, unaryrules = urs, generalrules = grs,
userrules = written, generatedrules = generated,
pcomment = comment,
varsAllAtoms = all roleVarsAllAtoms roles }
where
roleVarsAllAtoms role = all isAtom (rvars role)
rules :: Prot -> [Rule]
rules p = nullaryrules p ++ unaryrules p ++ generalrules p
{- aFormOrder generator
-- Generate the aFormOrder relation from a list of constructors
module Main (main) where
main :: IO ()
main =
mapM_ putStrLn $ map output comps
-- Format output
output :: (String, String, String) -> String
output (x, y, c) =
"aFormOrder (" ++ x ++ ") (" ++ y ++ ") = " ++ c
-- Compute comparisons
comps :: [(String, String, String)]
comps = [ (x, y, show $ compare i j) |
(x, i) <- pairs,
(y, j) <- pairs ]
-- Add in list position
pairs :: [(String, Int)]
pairs = zip constrs [0..]
-- Constructors
constrs :: [String]
constrs = [
"Length _ _ _",
"Param _ _ _ _ _",
"Prec _ _",
"Non _",
"Pnon _",
"Uniq _",
"UniqAt _ _",
"Conf _ ",
"Auth _",
"AFact _ _",
"Equals _ _" ]
-}