Updated ofmc grammar and regenerated parser.
This commit is contained in:
parent
ec42f2f2de
commit
9f66f82aa8
|
|
@ -59,6 +59,8 @@ fun rmOuterOp (Operator(_,[msg])) = msg
|
|||
| TBAR of string
|
||||
| TCOMMA of string
|
||||
| TCPAREN of string
|
||||
| TOBRACE of string
|
||||
| TCBRACE of string
|
||||
| TCRYPT of string
|
||||
| TQUOTE of string
|
||||
| TEXP of string
|
||||
|
|
@ -86,9 +88,13 @@ fun rmOuterOp (Operator(_,[msg])) = msg
|
|||
| TTYPES of string
|
||||
| TWITNESS of string
|
||||
| TXOR of string
|
||||
| TDERIVATION of string
|
||||
|
||||
%nonterm START of ofmc_fp
|
||||
| trace of ofmc_fp
|
||||
| ofmc_fp of ofmc_fp
|
||||
| attackinfo of ofmc_fp
|
||||
| fp_or_attack of ofmc_fp
|
||||
| simple_name of string
|
||||
| role of string
|
||||
| factname of string
|
||||
|
|
@ -114,13 +120,24 @@ fun rmOuterOp (Operator(_,[msg])) = msg
|
|||
|
||||
%%
|
||||
|
||||
START: ofmc_fp (ofmc_fp)
|
||||
START: TBACKEND TCOLON simple_names (update_backend simple_names empty_ofmc_fp)
|
||||
| TBACKEND TCOLON simple_names fp_or_attack (update_backend simple_names fp_or_attack)
|
||||
|
||||
ofmc_fp: TPROTOCOL TCOLON simple_name (update_protocol simple_name empty_ofmc_fp)
|
||||
fp_or_attack:TPROTOCOL TCOLON simple_name (update_protocol simple_name empty_ofmc_fp)
|
||||
| TPROTOCOL TCOLON simple_name ofmc_fp (update_protocol simple_name ofmc_fp)
|
||||
| TBACKEND TCOLON simple_names (update_backend simple_names empty_ofmc_fp)
|
||||
| TBACKEND TCOLON simple_names ofmc_fp (update_backend simple_names ofmc_fp)
|
||||
| TTYPES TCOLON types (update_types ((types_of empty_ofmc_fp)@types) empty_ofmc_fp)
|
||||
|
||||
| TATTACK TOPAREN msglist TCPAREN (update_attack msglist empty_ofmc_fp)
|
||||
| TATTACK TOPAREN msglist TCPAREN attackinfo (update_attack msglist attackinfo)
|
||||
|
||||
|
||||
attackinfo: TATTACK TOPAREN msglist TCPAREN (update_attack msglist empty_ofmc_fp)
|
||||
| TATTACK TOPAREN msglist TCPAREN attackinfo (update_attack msglist attackinfo)
|
||||
| TDERIVATION SIMPLE_NAME SIMPLE_NAME TATTACK TCOLON TATTACK TOPAREN msglist TCPAREN trace ((fn (_,_) => empty_ofmc_fp) (trace,msglist))
|
||||
|
||||
|
||||
|
||||
|
||||
ofmc_fp: TTYPES TCOLON types (update_types ((types_of empty_ofmc_fp)@types) empty_ofmc_fp)
|
||||
| TTYPES TCOLON types ofmc_fp (update_types ((types_of ofmc_fp)@types) ofmc_fp)
|
||||
| TSECTION TINITIAL TSECSTATE TCOLON knowledge (update_knowledge knowledge empty_ofmc_fp)
|
||||
| TSECTION TINITIAL TSECSTATE TCOLON knowledge ofmc_fp (update_knowledge knowledge ofmc_fp)
|
||||
|
|
@ -131,6 +148,20 @@ ofmc_fp: TPROTOCOL TCOLON simple_name (update_pr
|
|||
| TSECTION TABSTRACTION TCOLON abstractions (update_abstractions ((abstractions_of empty_ofmc_fp )@abstractions) empty_ofmc_fp)
|
||||
| TSECTION TABSTRACTION TCOLON (update_abstractions ((abstractions_of empty_ofmc_fp )@[]) empty_ofmc_fp)
|
||||
| TSECTION TABSTRACTION TCOLON abstractions ofmc_fp (update_abstractions ((abstractions_of ofmc_fp)@abstractions) ofmc_fp)
|
||||
|
||||
trace: TMINUS trace (empty_ofmc_fp)
|
||||
| TIKNOWS trace (empty_ofmc_fp)
|
||||
| TSECRET trace (empty_ofmc_fp)
|
||||
| TOBRACE trace (empty_ofmc_fp)
|
||||
| TCBRACE trace (empty_ofmc_fp)
|
||||
| TCBRACE (empty_ofmc_fp)
|
||||
| TOPAREN trace (empty_ofmc_fp)
|
||||
| TCPAREN trace (empty_ofmc_fp)
|
||||
| TCOMMA trace (empty_ofmc_fp)
|
||||
| TCPAREN (empty_ofmc_fp)
|
||||
| TCOMMA (empty_ofmc_fp)
|
||||
| SIMPLE_NAME trace (empty_ofmc_fp)
|
||||
| SIMPLE_NAME (empty_ofmc_fp)
|
||||
|
||||
rules: TSTEP TCOLON facts TMETAIMPLIES facts ([(NONE, facts1, facts2)])
|
||||
| TSTEP TCOLON facts TMETAIMPLIES facts rules ((NONE, facts1, facts2)::rules)
|
||||
|
|
@ -149,10 +180,10 @@ facts: fact ([fact])
|
|||
|
||||
fact: TSTATE TOPAREN role TCOMMA TOBRACKET msglist TCBRACKET TCPAREN (State(role, msglist))
|
||||
| TIKNOWS TOPAREN msg TCPAREN (Iknows(msg))
|
||||
| TATTACK TOPAREN msg TCPAREN (Attack(msg))
|
||||
| TSECRET TOPAREN msglist TCPAREN (Secret(msglist))
|
||||
| TWITNESS TOPAREN msglist TCPAREN (Witness(msglist))
|
||||
| TREQUEST TOPAREN msglist TCPAREN (Request(msglist))
|
||||
| TATTACK TOPAREN msglist TCPAREN (Attack(msglist))
|
||||
|
||||
nfacts: nfact ([nfact])
|
||||
| nfact TSEMICOLON nfacts (nfact::nfacts)
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@ signature OfmcFpParser_TOKENS =
|
|||
sig
|
||||
type ('a,'b) token
|
||||
type svalue
|
||||
val TDERIVATION: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TXOR: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TWITNESS: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TTYPES: (string) * 'a * 'a -> (svalue,'a) token
|
||||
|
|
@ -29,6 +30,8 @@ val TFACT: (string) * 'a * 'a -> (svalue,'a) token
|
|||
val TEXP: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TQUOTE: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCRYPT: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCBRACE: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TOBRACE: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCPAREN: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCOMMA: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TBAR: (string) * 'a * 'a -> (svalue,'a) token
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -72,6 +72,8 @@ ws = [\ \t];
|
|||
|
||||
|
||||
"-" => (Tokens.TMINUS(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"{" => (Tokens.TOBRACE(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"}" => (Tokens.TCBRACE(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"->" => (Tokens.TARROW(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
":" => (Tokens.TCOLON(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"=" => (Tokens.TEQ(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
|
|
@ -113,6 +115,7 @@ ws = [\ \t];
|
|||
"Inv" => (Tokens.TINV(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"Exp" => (Tokens.TEXP(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"Xor" => (Tokens.TXOR(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"Derivation" => (Tokens.TDERIVATION(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
|
||||
(_|{alpha}|{digit})+ => (Tokens.SIMPLE_NAME(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -42,7 +42,7 @@ datatype CMsg = CVariable of string * string
|
|||
|
||||
datatype CFact = CState of string * CMsg list
|
||||
| CIknows of CMsg
|
||||
| CAttack of CMsg
|
||||
| CAttack of CMsg list
|
||||
| CWitness of CMsg list
|
||||
| CRequest of CMsg list
|
||||
| CSecret of CMsg list
|
||||
|
|
@ -114,9 +114,9 @@ fun deabstractMsg abstractions (Atom s) = (case check_abstraction abstra
|
|||
|
||||
fun deabstractFact abstractions (State (n,ms)) = (CState (n, map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Iknows m) = (CIknows (deabstractMsg abstractions m))
|
||||
| deabstractFact abstractions (Attack m) = (CAttack (deabstractMsg abstractions m))
|
||||
| deabstractFact abstractions (Witness ms) = (CWitness (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Attack ms) = (CAttack (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Request ms) = (CRequest (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Witness ms) = (CWitness (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Secret ms) = (CSecret (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Fact (n,m)) = (CFact (n, deabstractMsg abstractions m))
|
||||
| deabstractFact abstractions (NotEqual (n,m)) = (CNotEqual (deabstractMsg abstractions n, deabstractMsg abstractions m))
|
||||
|
|
|
|||
|
|
@ -32,13 +32,22 @@
|
|||
|
||||
signature OFMC_ENCODER =
|
||||
sig
|
||||
val ofmc_thygen: OfmcFp.ofmc_fp -> unit
|
||||
val ofmc_thygenAnB: string -> unit
|
||||
val main: string * string list -> unit
|
||||
type result
|
||||
val ofmc_thygen: OfmcFp.ofmc_fp -> result * OfmcFp.ofmc_fp
|
||||
val ofmc_thygenAnB: string -> result * OfmcFp.ofmc_fp
|
||||
val main: string * string list -> unit * OfmcFp.ofmc_fp
|
||||
end
|
||||
|
||||
structure ofmc_thygen =
|
||||
struct
|
||||
datatype result = unknownError | success | parseError | attackOfmc | attackIsabelle
|
||||
|
||||
fun string_of_result unknownError = "unkown error"
|
||||
| string_of_result success = "success"
|
||||
| string_of_result parseError = "parse error"
|
||||
| string_of_result attackOfmc = "attack found by ofmc"
|
||||
| string_of_result attackIsabelle = "attack found by isabelle"
|
||||
|
||||
|
||||
val varcnt = ref ~1
|
||||
val noproof = ref false
|
||||
|
|
@ -160,7 +169,7 @@ fun gen_datatype ofmcfp =
|
|||
|
||||
fun collect_vars ofmcfp (CState (s,ms)) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CIknows m) = collect_msgvars ofmcfp m
|
||||
| collect_vars ofmcfp (CAttack m) = collect_msgvars ofmcfp m
|
||||
| collect_vars ofmcfp (CAttack ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CWitness ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CRequest ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CSecret ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
|
|
@ -183,7 +192,7 @@ and string_of_cmsg_list [] = ""
|
|||
|
||||
fun string_of_cfact ofmcfp (CState (s,ms)) = "State("^s^", ["^(string_of_cmsg_list ms)^"] )"
|
||||
| string_of_cfact ofmcfp (CIknows m) = "Iknows("^(string_of_cmsg m)^")"
|
||||
| string_of_cfact ofmcfp (CAttack m) = "Attack("^(string_of_cmsg m)^")"
|
||||
| string_of_cfact ofmcfp (CAttack ms) = "Attack("^(string_of_cmsg_list ms)^")"
|
||||
| string_of_cfact ofmcfp (CWitness ms) = "Witness("^(string_of_cmsg_list ms)^")"
|
||||
| string_of_cfact ofmcfp (CRequest ms) = "Request("^(string_of_cmsg_list ms)^")"
|
||||
| string_of_cfact ofmdfp (CSecret ms) = "Secret("^(string_of_cmsg_list ms)^")"
|
||||
|
|
@ -265,7 +274,7 @@ fun gen_fp ofmcfp =
|
|||
|
||||
fun mk_vars_unique (CState (s,ms)) = (CState (s, map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CIknows m) = (CIknows (mk_msgvars_unique m) )
|
||||
| mk_vars_unique (CAttack m) = (CAttack (mk_msgvars_unique m))
|
||||
| mk_vars_unique (CAttack ms) = (CAttack (map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CWitness ms) = (CWitness (map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CRequest ms) = (CRequest (map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CSecret ms) = (CSecret (map mk_msgvars_unique ms))
|
||||
|
|
@ -273,7 +282,7 @@ fun gen_fp ofmcfp =
|
|||
|
||||
fun mk_vars_unique' v (CState (s,ms)) = (CState (s, map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CIknows m) = (CIknows (mk_msgvars_unique' v m) )
|
||||
| mk_vars_unique' v (CAttack m) = (CAttack (mk_msgvars_unique' v m))
|
||||
| mk_vars_unique' v (CAttack ms) = (CAttack (map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CWitness ms) = (CWitness (map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CRequest ms) = (CRequest (map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CSecret ms) = (CSecret (map (mk_msgvars_unique' v) ms))
|
||||
|
|
@ -423,6 +432,8 @@ fun checkfp ofmcfp =
|
|||
|
||||
|
||||
fun ofmc_thygen ofmcfp =
|
||||
if is_safe ofmcfp
|
||||
then
|
||||
let
|
||||
val protocol = protocol_of ofmcfp
|
||||
val _ = print (gen_header ofmcfp)
|
||||
|
|
@ -444,9 +455,11 @@ fun ofmc_thygen ofmcfp =
|
|||
val _ = print ("*)\n")
|
||||
*)
|
||||
val _ = print ("\n\nend (* theory *)\n")
|
||||
in () end
|
||||
in (success,ofmcfp) end
|
||||
else (attackOfmc,ofmcfp)
|
||||
|
||||
val ofmc_thygenAnB = ofmc_thygen o ofmc_connector.parseAnBFile
|
||||
fun ofmc_thygenAnB f = (ofmc_thygen o ofmc_connector.parseAnBFile) f
|
||||
handle _ => (parseError, OfmcFp.empty_ofmc_fp)
|
||||
|
||||
fun print_usage name = let
|
||||
val _ = print("\n")
|
||||
|
|
@ -460,6 +473,8 @@ in
|
|||
()
|
||||
end
|
||||
|
||||
fun warning s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr)
|
||||
|
||||
fun main (name:string,args:(string list)) =
|
||||
let
|
||||
val prgName = (hd o rev) (String.fields (fn s => s = #"/" orelse s = #"\\") name)
|
||||
|
|
@ -471,7 +486,26 @@ fun main (name:string,args:(string list)) =
|
|||
| (n, "--wauth"::ar) => (ofmc_connector.wauth := true ; main(name, ar))
|
||||
| (n, [file]) => if String.isPrefix "-" file
|
||||
then print_usage name
|
||||
else ofmc_thygenAnB file
|
||||
else let
|
||||
val timer = Timer.startRealTimer ()
|
||||
val start = Timer.checkRealTimer timer
|
||||
val (result,fp) = ofmc_thygenAnB file
|
||||
val stop = Timer.checkRealTimer timer
|
||||
val duration = Time.-(stop,start)
|
||||
fun print_result duration result fp =
|
||||
let
|
||||
val _ = warning ("\nprotocol: "^(protocol_of fp)^"\n")
|
||||
val _ = warning ("result: "^(string_of_result result)^"\n")
|
||||
val _ = warning ("duration: "^(Time.toString duration)^"\n")
|
||||
val _ = warning ("fixed-point: "
|
||||
^(Int.toString(List.length (fixedpoint_of fp )))^"\n")
|
||||
val _ = warning ("knowledge: "
|
||||
^(Int.toString(List.length (knowledge_of fp )))^"\n")
|
||||
in () end
|
||||
in
|
||||
print_result duration result fp
|
||||
end
|
||||
|
||||
| (_,_) => print_usage name
|
||||
)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ type ProtocolState = MsgPat list
|
|||
datatype Fact = State of string * Msg list
|
||||
| FPState of string * Msg
|
||||
| Iknows of Msg
|
||||
| Attack of Msg
|
||||
| Attack of Msg list
|
||||
| Witness of Msg list
|
||||
| Request of Msg list
|
||||
| Secret of Msg list
|
||||
|
|
@ -64,30 +64,35 @@ type ofmc_fp = {
|
|||
Knowledge: (string * Fact) list,
|
||||
FixedPoint: (string * Fact) list,
|
||||
Abstractions : (Msg * Msg) list,
|
||||
Attack : Msg list,
|
||||
Source : string
|
||||
}
|
||||
|
||||
|
||||
val empty_ofmc_fp = {Backend="", Protocol="", Types = [("Number",["NI"])], Rules = [], Knowledge=[], FixedPoint=[],
|
||||
Abstractions=[(Atom "ni",Atom "NI")], Source=""}:ofmc_fp
|
||||
Abstractions=[(Atom "ni",Atom "NI")], Source="", Attack=[]}:ofmc_fp
|
||||
(* Abstractions=[(Atom "purpose",Atom "PURPOSE"),(Atom "ni",Atom "NI")], Source=""}:ofmc_fp *)
|
||||
|
||||
fun update_protocol protocol ({Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_backend backend ({Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_types types ({Backend=backend, Protocol=protocol, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_rules rules ({Backend=backend, Protocol=protocol, Types=types, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_knowledge knowledge ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_fixedpoint fixedpoint ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_abstractions abstractions ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_source source ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Abstractions=abstractions, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
|
||||
fun update_protocol protocol ({Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_backend backend ({Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_types types ({Backend=backend, Protocol=protocol, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_rules rules ({Backend=backend, Protocol=protocol, Types=types, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_knowledge knowledge ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_fixedpoint fixedpoint ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, Abstractions=abstractions,Source=source, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_abstractions abstractions ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Source=source, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_source source ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Abstractions=abstractions, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
|
||||
fun update_attack attack ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Abstractions=abstractions, Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Source=source, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Attack=attack}:ofmc_fp)
|
||||
|
||||
|
||||
fun mk_unique [] = []
|
||||
|
|
@ -105,5 +110,9 @@ fun fixedpoint_of (ofmcfp:ofmc_fp) = #FixedPoint ofmcfp
|
|||
fun abstractions_of (ofmcfp:ofmc_fp) = #Abstractions ofmcfp
|
||||
fun source_of (ofmcfp:ofmc_fp) = #Source ofmcfp
|
||||
|
||||
fun attack_of (ofmcfp:ofmc_fp) = #Attack ofmcfp
|
||||
|
||||
fun is_safe ofmcfp = (attack_of ofmcfp = [])
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
Reference in New Issue