{-

Open Source Fixedpoint Model-Checker version 2009c

(C) Copyright IBM Corp. 2009

All Rights Reserved.

-}

module Ast where
import Data.List
import Data.Maybe
import Msg

type Protocol = (String,Types,Knowledge,Abstraction,Actions,Goals)

----------- Protocol Description --------------

data Type = Agent Bool Bool --- flags: static, honest
          | Number
	  | PublicKey
	  | SymmetricKey
	  | Function
	  | Purpose
	  | Untyped
	  deriving (Eq,Show)

type Types = [(Type,[Ident])]

type Knowledge = [(Ident,[Msg])]

type Peer = (Ident,Bool,Maybe Msg)

type Channel = (Peer,ChannelType,Peer)

type Action = (Channel,Msg,Maybe Msg,Maybe Msg) 
type Actions = [Action]
  --- every action has the form 
  --- sender, channeltype, receiver, transmitted message, 
  --- and two optional message terms for zero-knowledge, namely a pattern 
  --- for the receiver, and a message that the sender must know

data ChannelType = Insecure | Authentic | Confidential | Secure 
     		 | FreshAuthentic | FreshSecure
                 deriving (Eq,Show)

data Goal = ChGoal Channel Msg
          | Secret Msg [Peer]
	  | Authentication Peer Peer Msg
	  | WAuthentication Peer Peer Msg
	  deriving (Eq,Show)

type Goals = [Goal]

type Abstraction = [ (Ident,Msg) ]
 
