{-

Open Source Fixedpoint Model-Checker version 2009c

(C) Copyright IBM Corp. 2009

All Rights Reserved.

-}

-------- Msg Patterns ------------------------------------

module MsgPat(MsgPat,ProtocolState,mkname,initialState,receiveMsg,sendMsg,receiveMsgPat,lversion,synthesisPattern,reshapePat) where
import Msg
import LMsg
import Ast
import Data.List
import Data.Maybe
import AnBOnP

type MsgPat = (Msg,Msg)
type ProtocolState = [MsgPat]

ppMsgPat ot (Atom x,Atom y) = (ppId x)++"%"++(ppId y)
ppMsgPat ot (m, Atom y) = (ppMsg ot m)++"%"++(ppId y)
ppMsgPat ot (Comp f xs, Comp g ys) = 
  let zs = zipl xs ys in
  case f of 
  Cat -> ppMsgPatList ot zs
  Apply -> ((ppMsgPat ot) (head zs))++"("++(ppMsgPatList ot (tail zs))++")"
  Crypt -> "{"++(((ppMsgPat ot) . head . tail) zs)++"}"++(ppMsgPat ot (head zs))
  Scrypt ->  "{|"++(((ppMsgPat ot) . head . tail) zs)++"|}"++(ppMsgPat ot (head zs))
  _ -> (show f)++"("++(ppMsgPatList ot zs)++")"

ppMsgPatList Pretty = ppXList (ppMsgPat Pretty) "\n"
ppMsgPatList ot = ppXList (ppMsgPat ot) ","


lversion = False 

mklabel :: Msg -> LMsg
mklabel = (\x -> (x,mkname x))

initialState :: [Msg] -> ProtocolState
initialState ik0 =
 if lversion then ((\ (x,y)->x++y) . lanalysis . (map mklabel)) ik0 else
 let ik = analysis ik0 in
 map (\ x -> (x,reshape ik x)) ik

receiveMsg :: Msg -> ProtocolState -> ProtocolState
receiveMsg msg state =
  if lversion then
   let (m':ik0,new) = lanalysis ((msg,(reshape (map fst state) msg)):state)
   in ik0++new++[m']
 else
  let ik0 = map fst state
      ik  = analysis (msg:ik0)
      nik = ik \\ (msg:ik0)
  in 
  (map (\(m,p) -> (m,reshapePat ("In receiveMsg\n"++(show msg)++"\n"++(show state)) ik (m,p))) state)
  ++ (map (\ msg -> (msg, reshape ik msg)) nik)
  ++ [(msg,reshape ik msg)]


--- possible improvement: only the incoming message is stored, not
--- all the other messages from NIK. Note that some functions rely
--- on an analyzed intruder knowledge.

reshape :: [Msg] -> Msg -> Msg
reshape ik (Atom a)=Atom a
reshape ik (msg@(Comp f xs)) =
 if f==Exp || f==Xor then 
  case 
   [(f',xs') |
   (Comp f' xs') <- eqMod  eqModBound stdTheo [msg], f==f',
   all (indy ik) xs']
  of
  [] -> mkname msg
  ((f',xs'):_) -> Comp f' (map (reshape ik) xs')
 else
  case (opening msg) of
  Nothing ->  error "Invariant violation (Nothing in reshape)" 
  Just list -> if all (indy ik) list 
	       then Comp f (map (reshape ik) xs)
	       else mkname msg

showik = ppXList (ppMsg IF) "\n"

reshapePat :: String -> [Msg] -> MsgPat -> Msg

reshapePat str ik m =  
 case m of
 (Comp Apply _,Comp Cat _) -> error ("Incompatible reshape pattern: "++str) 
 _ -> 
  case (reshapePat0 ik m) of
  Nothing -> error ("Pattern Problem:\n"++(showik ik)++"\n->\n"++(ppMsgPat Pretty m)++" ")
  Just p -> p


reshapePat0 :: [Msg] -> MsgPat -> Maybe Msg
reshapePat0 ik (Atom a,Atom b)=
  if a==b then Just (Atom a) else Nothing 
reshapePat0 ik (Atom a,Comp f xs) =
  error ("Pattern "++(show (Comp f xs))++" more concrete than actual msg "++a)
reshapePat0 ik (msg@(Comp f xs),pat@(Atom a)) =
 if f==Xor then if all (indy ik) xs then Just (Comp Xor (map (reshape ik) xs)) else Just (Atom a) else
  case (opening msg) of
  Nothing -> error "Invariant violated: Nothing in reshape" 
  Just list -> if all (indy ik) list 
	       then Just (Comp f (map (reshape ik) xs))
	       --- here we need to go into classical reshape as
	       --- further pattern is not yet available
	       else Just (Atom a) 
	       --- get the old pattern
reshapePat0 ik (msg@(Comp Apply xs),pat@(Comp Cat ys)) = error ("Incompatible patterns:\n"++(show ik)++"\n"++(show msg)++"\n"++(show pat))
reshapePat0 ik (msg@(Comp f xs),pat@(Comp g ys)) 
 |f==Apply && g==Cat = error "Super duper strange."
 |otherwise =
  if msg==pat then (Just pat) else
  if f==Exp || f==Xor then 
    (listToMaybe
     [ Comp g xs''
         |
         (Comp f' xs') <- eqMod eqModBound stdTheo [msg], f==f', 
         (xs''::[ Msg]) <- [catMaybes (map (reshapePat0 ik) (zipl xs' ys))],
         (length xs'')==(length xs)])
  else
   if f==g then 
    let test = zipl xs ys in
    if null (filter (\ x -> case x of 
       	    	            (Comp Apply _, Comp Cat _) -> True 
		  	    _ -> False) test) then
      deJust f (mapM (reshapePat0 ik) (zipl xs ys))
    else error ("Show :\n"++(show msg)++"\n"++(show msg))
   else if f==Apply && g==Cat then error "It is apply and Cat" 
   else error ("Patterns do not completely agree:\n\n"++(show msg)++"\n\nvs.\n\n"++(show pat))

deJust f (Just ms) = Just (Comp f ms)
deJust f Nothing = Nothing

opening :: Msg -> Maybe [Msg]
opening msg = 
  case msg of
  Comp Crypt [Comp Inv [k],m] -> Just [k]
  Comp Crypt [k,m] -> Just [Comp Inv [k]]
  Comp Scrypt [k,m]-> Just [k]
  Comp Cat _ -> Just []
  Comp Inv [k] -> Just []
  Comp Apply ms -> Just ms
  Comp Exp ms -> Just ms
  Comp Xor ms -> error "Opening: didn't cach XOR"
  _ -> error ("Opening: Not yet supported: "++(show msg))

--- Note: when using probabilistic encryption, we actually  cannot check that
--- {M}K has form {.}. even if we know M and K, but not inv(K).
--- We leave it, though, as probabilistic encryption must be modeled
--- by explicit nonces (introduced by AnBParser).

-----------------------

sendMsg :: Msg -> ProtocolState -> ProtocolState
sendMsg msg state =
  case synthesisPattern state msg of
  Nothing -> error ("Protocol not executable:\n\n"++
  	     	    "At the following state of the knowledge:\n"++
		    (ppMsgPatList Pretty state)++"\n\n"++
		    "...one cannot compose the following message:\n"++
  	     	    (ppMsg Pretty msg)++"\n"++
		    (getProblem state msg "")
		   )
  Just p -> state++[(msg,p)]

getProblem :: ProtocolState -> Msg -> String -> String
getProblem ik (Atom a) ind = ""
getProblem ik (Comp f xs) ind =
  concat [ ind++(ppMsg Pretty x)++"\n"++
  	   (getProblem ik x (ind++"|")) 
	 | x <- xs, isNothing (synthesisPattern ik x) ]
    


synthesisPattern :: ProtocolState -> Msg -> (Maybe Msg)
synthesisPattern ik =
  listToMaybe . 
  catMaybes .
  (map (synthesisPattern0 ik)) .
  (eqMod 3 stdTheo) .
  return

synthesisPattern0 :: ProtocolState -> Msg -> (Maybe Msg)
synthesisPattern0 ik m =
  case getElem m ik of
  Just p -> Just p
  Nothing ->
   case m of
    Atom _             -> Nothing
    Comp Inv _         -> Nothing
    Comp (Userdef _) _ -> error ("Not yet supported: "++(show m))
    Comp Xor list      -> 
     let ik0=map fst ik in
     if synthesizable ik0 m then 
      if (all (synthesizable ik0) list) then
        Just (Comp Xor (map (fromJust . (synthesisPattern0 ik)) list))
      else
        head
        [ Just (normalizeXor (mkxor d1 d2))
	| (Comp Xor l1,d1) <- ik,
	  (Comp Xor l2,d2) <- ik,
	  l1/=l2, 
	  m==normalizeXor (Comp Xor (l1++l2))
	]
     else Nothing
    Comp f ms          -> 
     let mps = map (synthesisPattern0 ik) ms
     in if Nothing `elem` mps then Nothing
        else Just (Comp f (map fromJust mps))

mkxor (Comp Xor l1) (Comp Xor l2) = Comp Xor (l1++l2)
mkxor (Comp Xor l1) b = Comp Xor (b:l1)
mkxor a (Comp Xor l2) = Comp Xor (a:l2)
mkxor a b = Comp Xor [a,b]

getElem x [] = Nothing
getElem x ((m,p):mps) = if x==m then Just p else getElem x mps

-------------------

enlabel ((Atom a),(Atom b)) = (Atom a,Atom b)
enlabel ((Comp f xs), (Comp g ys)) = 
  if f/=g || (length xs)/=(length ys) then error "error in function enlabel" else
  let (xs',ys') = unzip (map enlabel (zipl xs ys))
  in (Comp f xs', Comp g ys')
enlabel ((Comp f xs),(Atom b)) = ((Comp f xs),mkname (Atom b))

receiveMsgPat :: MsgPat -> ProtocolState -> ProtocolState
receiveMsgPat (msg,msgp) state =
 if lversion then
   let (m':ik0,new) = lanalysis ((enlabel (msg,msgp)):state)
   in (ik0++new++[m'])
 else 
  let ik0  = map fst state
      ik   = analysis (msg:ik0)
      nik  = ik \\ ik0
  in 
  (map (\ (m,p) -> (m,reshapePat "" ik (m,p))) state)
  ++ (reshapePatAna (msg,msgp) (nik\\[msg]))
  ++ [(msg,reshapePat "" ik (msg,msgp))]

reshapePatAna :: LMsg -> [Msg] -> [LMsg]
reshapePatAna (msg,msgp) ik =
  let mmap = allposL (msg,msgp) 
      lookup m = let mp = [ p | (m',p) <- mmap, m==m'] in 
      	       	 if null mp then error ("did not find "++(ppMsg Pretty m)) else head mp
  in map (\m -> (m,lookup m)) ik

allposL :: LMsg -> [LMsg]
allposL (mp@(Comp f xs, Comp g ys)) = 
 if f==g then mp:(concatMap allposL (zipl xs ys))
 else error ("Pattern problem:\n"++(show f)++"\nvs\n"++(show g))
allposL mp = [mp]

getKnowPat :: MsgPat -> [Msg]
getKnowPat (m,p) = nub (m:(getKnow0 (m,p)))

getKnow0 (Atom x,Atom _) = [Atom x]
getKnow0 (Atom x,_) = error "Pattern more precise than term!"
getKnow0 (Comp f xs,Atom y) = [Atom y] 
getKnow0 m@(Comp Apply (f:xs),Comp Apply (g:ys)) = 
  if f/=g then error ("Message Pattern!"++(show m)) else
  (Comp Apply (f:xs)):(concatMap getKnow0 (zipl xs ys))
getKnow0 m@(Comp f xs,Comp g ys) = 
  if f/=g then error ("Message Pattern!"++(show m)) else
  (Comp f xs):(concatMap getKnow0 (zipl xs ys))

