{-

Open Source Fixedpoint Model-Checker version 2011c

(C) Copyright IBM Corp. 2009
(C) Copyright ETH Zurich (Swiss Federal Institute of Technology) 2003,2007

All Rights Reserved.

-}

import AnBmain
import AnBOnP
import System
import CPUTime
import Constants
import IntsOnly
import Decomposition
import Remola
import Symbolic
import NewIfParser
import PrettyUgly
import Search
import Data.Maybe
import Data.Char
import Data.List
import System.Exit
import TheoLoad
import FiniteMap 
import Control.Concurrent
import If2Horn
import FPTranslator
import Control.Exception

productname = "Open Source Fixedpoint Model-Checker version 2011c"

usage =    "usage: ofmc <INPUT FILE> [<OPTIONS>]   \n"
	++ "Options:\n"
        ++ "  -numSess <INT>  specify the number of sessions (for an AnB spec)\n"
        ++ "  -ot IF          do not check, but produce only AVISPA IF\n"
	++ "  -ot Isa         generate a fixedpoint proof for Isabelle-OFMC\n" 
	++ "  -fp             run only in fixedpoint module\n"
	++ "  -classic        run only in classic mode\n"
	++ "Options for classic mode:\n"
        ++ "  -theory <TheoryFile>   use a custom algebraic theory\n"
        ++ "  -sessco <INT>   performs an executability check and session compilation\n"
	++ "  -untyped        ignores all type-declarations\n"
        ++ "  -d <DEPTH>      specify maximum search depth/depth first search\n"
        ++ "  -p <PATH>       (PATH is white-space separated list of ints)\n"
        ++ "                  specify a path in the search tree to visit\n"
        ++ "                  by the indices of the successors to follow.\n"

data Decision = SAFE | UNSAFE | INCONCLUSIVE 
     	      deriving (Eq,Show)

data Result = Report { decision :: Decision,
     	      	       details  :: String,
		       protocol :: String,
		       goal     :: String,
		       comments :: String,
		       statistics::String,
		       attack   :: String }

dummyresult = Report {decision = INCONCLUSIVE, 
	      	      details = "",
		      protocol = "",
		      goal = "",
		      comments = "",
		      statistics = "",
		      attack = ""}

verified wauth protocolname
         = Report    {decision = SAFE, 
	      	      details = "unbounded number of sessions, typed model, free algebra",
		      protocol = protocolname,
		      goal = (if wauth then "" else "honest-")++
		      	      "weak authentication and secrecy",
		      comments = "It is recommended to run with -classic option as well (see manual).",
		      statistics = "",
		      attack = ""}

showresult result =
  let optional str f = if (f result)=="" then "" else str++"\n  "++(f result)++"\n" in
  "\nSUMMARY\n  "++
  (show (decision result))++"\n"++
  (optional "DETAILS" details)++
  (optional "PROTOCOL" protocol)++
  (optional "GOAL" goal)++
  "BACKEND\n  OFMC 2011c\n"++
  (optional "COMMENTS" comments)++
  (optional "STATISTICS" statistics)++
  (if (decision result)==UNSAFE 
   then "ATTACK TRACE\n"++
   	(attack result)++"\n"
   else "")

showresults results =
  let unsafe = filter (((==) UNSAFE) . decision) results
      conclusive = filter (((/=) INCONCLUSIVE) . decision) results
  in showresult (head (unsafe++conclusive++results))


data OptsAndPars = OnP { filename :: String,
			 output   :: Maybe String,
			 depth    :: Maybe Int,
			 sesrep   :: Int,
			 path     :: Maybe [Int],
			 typing   :: Typing,
			 sessco   :: Bool,
			 por      :: Bool, 
			 must_step :: Bool,
			 normalize :: Bool,
			 showrules :: Bool,
                         theofile :: Maybe String,
                         isAnB :: Bool
                       }

parseArgs  :: [String] -> (OptsAndPars,AnBOptsAndPars)
parseArgs [] = error ("No input file specified.\n"++usage)
parseArgs ("--help":xs) = error usage
parseArgs (x:xs) = 
  parseArgs0 xs (OnP { filename = x , 
		       output   = Nothing,
		       depth    = Nothing, 
		       sesrep   = 1,
		       path     = Nothing, 
		       sessco   = False,
		       typing   = AsGiven,
		       must_step = False,
		       por      = True,
		       normalize = True,
                       showrules = False,
		       theofile  = Nothing,
		       isAnB = isSuffixOf ".ANB" (map toUpper x)},
	         AnBOnP{ 
       		   anbfilename = "",
      		   theory   = Nothing,
       		   anboutput   = Nothing,
       		   numSess  = Nothing,
       		   outt     = Amphibian,
       		   typed    = True,
		   iterateFP = 0,
		   authlevel = HWeak
     		 })

parseArgs0 :: [String] -> (OptsAndPars,AnBOptsAndPars) -> (OptsAndPars,AnBOptsAndPars)
parseArgs0 [] (onp,anbonp) = (onp,anbonp)
parseArgs0 ("-nonorm":xs) (onp,anbonp) = parseArgs0 xs (onp {normalize = False},anbonp)
parseArgs0 ("-theory":xs) (onp,anbonp) = parseArgs0 (tail xs) (onp {theofile = Just (head xs)},anbonp)
parseArgs0 ("-showrules":xs) (onp,anbonp) = parseArgs0 xs (onp {showrules = True},anbonp)
parseArgs0 ("-nocd":xs) (onp,anbonp) = parseArgs0 xs (onp { por = False },anbonp )
parseArgs0 ("--typed_model=yes":xs) (onp,anbonp) = parseArgs0 xs (onp { typing= AsGiven },anbonp )
parseArgs0 ("--typed_model=no":xs) (onp,anbonp) = parseArgs0 xs (onp { typing= Untyped },anbonp)
parseArgs0 ("--typed_model=strongly":xs) (onp,anbonp) = error ("  The strongly typed model is currently not supported\n")
parseArgs0 (('-':'-':opt):xs) (onp,anbonp) = 
  if (isPrefixOf "output" opt) then 
    parseArgs0 xs (onp,anbonp)
  else if (isPrefixOf "redirect" opt) then
    parseArgs0 xs (onp {output = Just (drop 9 opt)},anbonp)
  else error ("unrecognized option '"++('-':'-':opt)++"'")
parseArgs0 ("-r":v:xs) (onp,anbonp) = parseArgs0 xs (onp { sesrep = (0+(read v)) },anbonp)
parseArgs0 ("-p":xs) (onp,anbonp) = 
  let (xs',xs'') = span (\ x -> (x/="") && (isDigit (head x))) xs
  in parseArgs0 xs'' (onp { path = Just (map read xs'), por = True },anbonp)
parseArgs0 ("-d":v:xs) (onp,anbonp) = parseArgs0 xs (onp { depth = Just (read v)},anbonp)
parseArgs0 ("-sessco":xs) (onp,anbonp) = parseArgs0 xs (onp { sessco = True },anbonp)
parseArgs0 ("-untyped":xs) (onp,anbonp) = if (typing onp) /= AsGiven 
			         then error ("Error parsing typing arguments.")
				 else parseArgs0 xs (onp { typing=Untyped},anbonp)
parseArgs0 ("-strongly-typed":xs) (onp,anbonp) = if (typing onp) /= AsGiven 
			         then error ("Error parsing typing arguments.")
				 else parseArgs0 xs (onp { typing=StronglyTyped},anbonp)
---- AnB options:
parseArgs0 ("-numSess":n:xs) (onp,anbonp) =
  if not (isAnB onp) then error "option -numSess only supported for .AnB input files\n" else
  if (numSess anbonp)==Nothing 
  then parseArgs0 xs (onp,anbonp {numSess=Just (read n)})
  else error "Multiple Declarations of \"numSess\" on command line"
parseArgs0 ("-typed":xs) (onp,anbonp) = 
  parseArgs0 xs (onp,anbonp{typed=True})
parseArgs0 ("-ot":"FP":xs) (onp,anbonp) =
  parseArgs0 xs (onp,anbonp{outt=FP})
parseArgs0 ("-ot":"FPI":file:xs) (onp,anbonp) = --- for debugging: iterative
  parseArgs0 xs (onp,anbonp{outt=FPI,anboutput=Just file})
parseArgs0 ("-ot":"IF":xs) (onp,anbonp)=
  if not (isAnB onp) then error "option '-ot IF' only supported for .AnB input files\n" 
  else parseArgs0 xs (onp,anbonp{outt=IF})
parseArgs0 ("-ot":"Isa":xs) (onp,anbonp)=
  parseArgs0 xs (onp,anbonp{outt=Isa})
parseArgs0 ("-ot":"AMPHI":xs) (onp,anbonp) = 
  parseArgs0 xs (onp,anbonp{outt=Amphibian})
parseArgs0 ("-ot":other:xs) (onp,anbonp)  = error ("Unknown output format: "++other)
parseArgs0 ("-fp":xs) (onp,anbonp) =   
  parseArgs0 xs (onp,anbonp{outt=FP})
parseArgs0 ("-classic":xs) (onp,anbonp) = parseArgs0 xs (onp,anbonp{outt=Internal})
parseArgs0 ("-dfs":xs) (onp,anbonp) = parseArgs0 xs (onp{depth=Just (fromMaybe 10000000  (depth onp))},anbonp)
parseArgs0 ("-bfs":xs) (onp,anbonp) = parseArgs0 xs (onp{depth=Nothing},anbonp)
parseArgs0 ("-ids":xs) (onp,anbonp) = parseArgs0 xs (onp{depth=Nothing},anbonp)
parseArgs0 ("-wauth":xs) (onp,anbonp) = parseArgs0 xs (onp,anbonp{authlevel=Weak})
parseArgs0 str (onp,anbonp) = error ("Error parsing arguments: "++(foldr (++) "" str))


main 
 = do args <- System.getArgs
      (onp,anbonp) <- return (parseArgs args)
      putStr (let brandname = "Open-Source Fixedpoint Model-Checker version 2011c" in
      	      if (outt anbonp)==IF then "% Generated by "++brandname++"\n" else
      	      if (outt anbonp)==Isa then "Backend: "++brandname++" \n" else
	      brandname++"\n")
      if ((outt anbonp)==Amphibian) 
       then do mtid <- myThreadId
       	       classicResult <- newEmptyMVar
	       fpResult <- newEmptyMVar
	       forkIO (mainWithArgs (onp,anbonp{outt=FP}) (Just (classicResult,fpResult)) False)
	       forkIO (mainWithArgs (onp,anbonp{outt=Internal, numSess=(Just 1)}) (Just (classicResult,fpResult)) (isAnB onp))
	       classicresult <- takeMVar classicResult
	       fpresult <- takeMVar fpResult
	       (case (decision classicresult, decision fpresult) of
	        (UNSAFE,_) -> do putStr (showresult classicresult)
		(_,SAFE) -> do putStr (showresult fpresult)
		_ -> do  classicresult2 <- takeMVar classicResult
	       		 fpresult2 <- takeMVar fpResult
			 (case (decision classicresult2, decision fpresult2) of
			  (_,SAFE) -> do putStr (showresult fpresult2)
	        	  _ -> do putStr (showresult classicresult2)))
       else 
        if (outt anbonp)==Isa then 
	  if (isAnB onp) then 
	    do str <- readFile (filename onp)
	       putStr (newanbmain str anbonp)
	  else do str <- readFile (filename onp)
	          putStr (hornFP [] True anbonp 
       	    	           (aslan2horn str))
	else
	    if (isAnB onp) && ((outt anbonp)==FPI)
       	    then do iterativeFP (onp,anbonp{iterateFP=7})
	    else if (isAnB onp) && ((numSess anbonp)==Nothing)
	    	 then do mainWithArgs (onp,anbonp{numSess=(Just 1)}) Nothing True
		 else do mainWithArgs (onp,anbonp) Nothing False

iterativeFP (onp,anbonp)  =
 	    do str <- readFile (filename onp)
	       writeFile ((fromJust (anboutput anbonp))++(show (iterateFP anbonp)))
       	       		 (newanbmain str anbonp)
       	       iterativeFP (onp,anbonp{iterateFP=((iterateFP anbonp)+1)})


mainWithArgs (onp,anbonp) (brothers::Maybe ((MVar Result,MVar Result))) iterative =
   do file <- if isAnB onp then 
              	 if (outt anbonp)==Internal then
		    do str <- readFile (filename onp)
		       return (newanbmain str (anbonp {outt=IF}))
		 else
		    do str <- readFile (filename onp)
		       verify <- return(newanbmain str anbonp)
		       (if isSafe verify
		        then let result = verified ((authlevel anbonp)==Weak) (filename onp)
			     in if isJust brothers then
			     	do putMVar (fst (fromJust brothers)) dummyresult
			     	   putMVar (snd (fromJust brothers)) result
				   x <- newEmptyMVar
				   takeMVar x
				   return ""
				else do putStr (showresult result)
				     	exitSuccess
					return ""
		        else if (outt anbonp)==IF then do putStr verify
			     	      		       	  exitSuccess
			     else if (outt anbonp)==Isa then error "??"
			     	  else error ("***"++verify++"***\n"))
               else
	         readFile (filename onp)
      t0 <- getCPUTime 
      tfile <-  case theofile onp of 
                   Nothing -> return ""
                   Just f  -> readFile f
      (algTheo,tab) 
           <- if tfile == "" then return ((fecStd,(decanaStd,cancellationStd)),emptyFM)
                 else return (theoparse tfile)
      (case file of
       'P':'r':'o':'t':'o':'c':'o':'l':_ -> 
         error "Appears to be AnB file, please use filename with extension .AnB\n"
       _ -> return ())
      (if ((outt anbonp)==FP) || ((outt anbonp)==FPI) || ((outt anbonp)==Isa) 
       then let verify = ( (hornFP [] True anbonp 
       	    	           (aslan2horn file))) 
	        result = verified ((authlevel anbonp)==Weak) (filename onp)
	    in 
            if isSafe verify
	     then
	       if isJust brothers
	        then do putMVar (fst (fromJust brothers)) dummyresult
			putMVar (snd (fromJust brothers)) result
			x <- newEmptyMVar
			takeMVar x
	        else do putStr (showresult result) 
		     	exitSuccess
             else
	      if isJust brothers then
	       do putMVar (fst (fromJust brothers)) dummyresult
		  putMVar (snd (fromJust brothers)) dummyresult
		  x <- newEmptyMVar
		  takeMVar x
              else do putStr  verify
	      	      exitSuccess
       else return ())
      trans_sys <- (return . ipp . (ifparser (algTheo,tab) (typing onp) (por onp) (normalize onp))) file
      _ <- case trans_sys of
           (_,rules,_,_) ->
            if (showrules onp) then 
             error ((show (length rules))++
                    (concatMap 
                     (\ (lhs,neg,cond,rhs,rtype) ->
                      ((show lhs)++"\n"++
                       (show neg)++"\n"++
                       (concatMap show_inequality cond)++"\n"++
                       (show rhs)++"\n--------\n")) (map (\ x -> x 17) rules)))
            else return 42
      t1 <- getCPUTime
      (str,stats) <- return ( (core algTheo onp trans_sys) True)
      a <- return (($!) (\x -> if 0<(length x) then x else "") str)
      t2 <- if a/="" then getCPUTime else error "lazy eval"
      if iterative && str==nothing_found 
       then let cns = fromJust (numSess anbonp) in
       	    do putStr ("Verified for "++(show cns)++" sessions\n")
	       mainWithArgs (onp,anbonp{numSess=Just (cns+1)}) brothers iterative 
	       exitSuccess
       else do return ()
      (let result=
            (case (path onp) of
	     Just p -> dummyresult
	     	       { comments=str }
             Nothing ->   
	      (if str==nothing_found then
		   dummyresult
		   {decision=SAFE,
		    details="Bounded number of sessions",
		    protocol=filename onp,
		    goal="as specified",
		    statistics="parseTime: "++(showtime t0 t1)++"\n  searchTime: "++(showtime t1 t2)++"\n"++(show_stats stats)}
       	       else
	           dummyresult
		   {decision=UNSAFE,
		    protocol=filename onp,
		    goal=(takeWhile ((/=) '*') str),
		    statistics="parseTime: "++(showtime t0 t1)++"\n  searchTime: "++(showtime t1 t2)++"\n"++(show_stats stats),
		    attack=(tail . (dropWhile ((/=) '*'))) str}))
       in case output onp of
	  Nothing ->  if isJust brothers 
	   	       then do putMVar (fst (fromJust brothers)) result
			       putMVar (snd (fromJust brothers)) dummyresult
			       return ()
	  	      else putStr (showresult result)
          Just outfile -> writeFile 
				(outfile++"/"++(reverse (takeWhile ((/=) '/') 
						    (reverse (filename onp))))++".of")
                                (showresult result))    



showtime t1 t2 
 = let cents = (mod (div (t2-t1) (10^10)) (100))
   in (show (div (t2-t1) (10^12)))++"."
      ++(if cents<10 then "0" else "")++(show cents)++"s"


ipp (init0,rules0,secr,goals) = 
 (init0,rules0,secr,goals)

core algTheo onp 
          (init,rules,secr,goals) isNewIF
 = let fname = filename onp
       sfb   = sesrep onp
       pth   = path onp
       depthb = depth onp
       cd    = por onp
       must  = must_step onp
       (i,bool) = getmaxstep rules [] False 
       newstate=
 	     if sessco onp then
	       let (bool,mfacts) = xexec_check algTheo cd rules i (varstart,init_init algTheo init) in 
	       if not bool then 
	          error ("Cannot see how the protocol can be executed.\nSee manual for more information.")
               else 
		let (mfacts',newfacts) = partition isMTerm (map uniquizef ( mfacts))
		    newmsg = map (\ (M _ _ _ _ m _) -> m) mfacts' 
                    uniquizing (Var i) = Var (-i) 
                    uniquizing m = m
                    uniquize = mapmsg uniquizing
                    uniquizef = mapfact uniquize 
                    (cs',sub',ik') 
                      = head (analz algTheo (cs init) (getallIK (ik init)) newmsg)
		    davars = map (\ i -> Var i) (concatMap msg_vars newmsg)
	            constraint0 = mkDFromState davars ik' 
                    cs'' = if davars==[] then cs' else ((fst cs')++[constraint0], snd cs') in
                (init{facts=(facts init)++newfacts,
		      ik=undiffIKstate ik', 
		      cs=cs''})
             else init_init algTheo init 
   in 
   if isNewIF && bool && (sessco onp) then error "The protocol description has loops.\nPlease try without option -sessco\n"
   else
   (if isNewIF && bool then (\ (x,y) -> ("% ********************************************\n% Warning: The protocol description has loops.\n% ********************************************\n"++x,y))
    else (\ x -> x))
   (case (pth,depthb) of
      (Nothing,Nothing) -> 
	  let (str,stats) =
	         (neusuch algTheo must cd rules (general_attack_check algTheo cd goals) 
                  nodemax depthbound 
	          sfb ([(varstart,newstate)],[]) init_stats) in
          if (str==reached_balance) then  
	      let maxdepth = if isJust depthb then fromJust depthb else depthbound
	          (a,b) = core algTheo (onp {depth=Just maxdepth}) (init,rules,secr,goals) isNewIF in
                (a,b)
          else (str,stats)
      (Just list,Nothing) 
          -> (shn2 (general_attack_check algTheo cd goals)
		   (\ depth -> treeconstruct algTheo must cd sfb depth (newstate,rules)) list
              ,init_stats)
      (Just [], Just ply) ->
         (sprintTree (treeconstruct algTheo must cd sfb ply (newstate,rules)),init_stats)
      (_,Just ply) -> let (c,n)=(wrids2 ply (general_attack_check algTheo cd goals) 
		  	      (treeconstruct algTheo must cd sfb ply (newstate, rules)))
                      in case c of
	                  '*':c' -> (c',(n,ply) )
                          _      -> (nothing_found,(n,ply)))


-------------------------
--- The standard algebraic theory. Note that defining it here 
--- underlines the independence of all algos from this example theory.

algStd = (fecStd,(decanaStd,cancellationStd))

ttXOR::TopdecTheo
ttXOR op 
 | op == opXor =
  [((opXor,[0,1]),
   [Unconditional [[Var 0,Var 1],
	 	   [Var 1,Var 0]],
    Conditional (0,(opXor,[2,3]))
                [Unconditional [[Var 2,BinOp opXor (Var 3) (Var 1)],
                                [BinOp opXor (Var 2) (Var 1),Var 3]],
                 Conditional (1,(opXor,[4,5]))
                             [Unconditional [[BinOp opXor (Var 2) (Var 4), BinOp opXor (Var 3) (Var 5)]]]],
    Conditional (1,(opXor,[2,3]))
                [Unconditional [[BinOp opXor (Var 0) (Var 2),Var 3],
                                [Var 2,BinOp opXor (Var 0) (Var 3)]]]])]
 | otherwise = []

ttEXP::TopdecTheo
ttEXP op 
 | op == opExp =
   [((opExp,[0,1]),
     [Unconditional [[Var 0,Var 1]],
      Conditional (0,(opExp,[2,3]))
                  [Unconditional [[BinOp opExp (Var 2) (Var 1),Var 3]]]])]
 | otherwise = []

fecStd :: FECTheo
fecStd = (topdecSubtheory,subtheory)
  where topdecSubtheory op
          | op == opExp = ttEXP
          | op == opXor = ttXOR
          | otherwise   = error ("No theory for "++(show op))
        subtheory op
          | op == opExp = [opExp]
          | op == opXor = [opXor]
          | otherwise   = []

x1 = -1001
x2 = -1002

decanaStd :: DecanaTheo
decanaStd = 
 [ ---Extend  
   (BinOp opCrypt (UnOp opInv (Var x1)) (Var x2), [Tauto],
    (Var x1), (Var x2)),
   ---Extend  
   (BinOp opCrypt (Var x1) (Var x2), [Negsub [(-1)] [(Var x1,UnOp opInv (Var (-1)))]],
    UnOp opInv (Var x1), (Var x2)),
   --- Replace 
   (BinOp opScrypt (Var x1) (Var x2),[Tauto],(Var x1),(Var x2)),
   --- Replace 
   (BinOp opExp (Var x1) (Var x2),[Tauto],(Var x2),(Var x1)),
   --- Replace 
   (BinOp opXor (Var x1) (Var x2),[Tauto],(Var x1),(Var x2)) ]

cancellationStd :: NormalizationRules
cancellationStd = 
  (concatMap ((\ (Just x) -> x) . f) [opInv,opCrypt,opScrypt,opExp,opXor],f)
 where
   f x |  x==opInv = 
            Just [(UnOp opInv (UnOp opInv (Var x1)),(Var x1))]
       |  x==opCrypt = 
            Just [(BinOp opCrypt (UnOp opInv (Var x1)) (BinOp opCrypt (Var x1) (Var x2)),(Var x2)),
                  (BinOp opCrypt (Var x1) (BinOp opCrypt (UnOp opInv (Var x1)) (Var x2)),(Var x2))]
       |  x==opScrypt = 
            Just [(BinOp opScrypt (Var x1) (BinOp opScrypt (Var x1) (Var x2)),(Var x2))]
       |  x==opExp =
            Just [(BinOp opExp (BinOp opExp (Var x1) (Var x2)) (UnOp opInv (Var x2)), (Var x1))]
       |  x==opXor = 
            Just [(BinOp opXor (Var x1) (Var x1), Atom 0 "e"),
                  (BinOp opXor (Var x1) (Atom 0 "e"), Var x1),
                  (BinOp opXor (BinOp opXor (Var x1) (Var x2)) (Var x2), (Var x1))]
       | otherwise = Nothing


theoryOf :: BinOp -- or UnOp
         -> Maybe Equations
theoryOf = snd cancellationStd

irreduc op t = 
 case theoryOf op of
 Just theo -> 
  map (\ (lhs,_) -> 
         let lhs'=rename (-30) lhs in 
         Negsub (msg_vars lhs') [(t, lhs')]) theo
 Nothing -> []

isSafe str =
  let skipcomment = (drop 1) . 
	            (dropWhile ((/=) '\n')) in
  if "(*" `isPrefixOf` str then isSafe (skipcomment str)
  else "SAFE" `isPrefixOf` str 
