11/7/2018: F2F Consortium meeting at FORTH

Confidentiality - Sequence

rule “Confidentiality – Sequence”

when

$s: Sequence($sId:=id, $pA:=placeholdera, $pB:=placeholderb, $Link:=link)

Property($sId:=subject, category==“Confidentiality”, satisfied==false)

then

if ($pA.hasOperationType(“storeData”)) {

insert(new Property($pA:=subject, category==“EncryptedStorage”, satisfied==false);

}

if ($pA.hasOperationType(“processData”)) {

insert(new Property($pB:=subject, category==“EncryptedProcessing”, satisfied==false);

}

if ($pB.hasOperationType(“storeData”)) {

insert(new Property($pA:=subject, category==“EncryptedStorage”, satisfied==false);

}

if ($pB.hasOperationType(“processData”)) {

insert(new Property($pB:=subject, category==“EncryptedProcessing”, satisfied==false);

}

insert(new Property($Link:=subject, category==“EncryptedChannel”, satisfied==false);

end

Integrity - Sequence

rule “Integrity – Sequence”

when

$s: Sequence($sId:=id, $pA:=placeholdera, $pB:=placeholderb, $Link:=link)

Property($sId:=subject, category==“Integrity”, satisfied==false)

then

if ($pA.hasOperationType(“storeData”)) {

insert(new Property($pA:=subject, category==“SafeStorage”, satisfied==false);

}

if ($pA.hasOperationType(“processData”)) {

insert(new Property($pB:=subject, category==“SafeProcessing”, satisfied==false);

}

if ($pB.hasOperationType(“storeData”)) {

insert(new Property($pA:=subject, category==“SafeStorage”, satisfied==false);

}

if ($pB.hasOperationType(“processData”)) {

insert(new Property($pB:=subject, category==“SafeProcessing”, satisfied==false);

}

insert(new Property($Link:=subject, category==“SafeChannel”, satisfied==false);

end

Availability

rule “Availability – Sequence”

when

$s: Sequence($sId:=id, $pA:=placeholdera, $pB:=placeholderb, $Link:=link)

Property($sId:=subject, category==“Availability”, satisfied==false)

then

insert(new Property($pA:=subject, category==“Redundancy”, satisfied==false);

insert(new Property($pB:=subject, category==“FaultManagement”, satisfied==false);

insert(new Property($pA:=subject, category==“Uptime”, satisfied==false);

end

Signed Message

rule ” Signed Message Verification – Sequence”

when

$P1: Placeholder($pl1:=placeholderid)

$P2: Placeholder($pl2:=placeholderid)

$OP: Operation(($pl1:=subject, operationType==”SignMessage”)

$OP: Operation(($pl2:=subject, operationType==”VerifyMessage”)

$ORCH: Sequence ($seq:=placeholderid, $pl1:=placeholdera, $pl2:=placeholderb)

$PR: Property ($seq:=subject, category==“SignedMessage”, satisfied==false)

then

modify($PR){satisfied=true};

End

rule ” SignedMessage Verification with Certificate #1 – Placeholder”

when

$P1: Placeholder($pl1:=placeholderid)

$Op: Operation($pl1:=subject, name==” SignMessage “)

$PR: Property ($pl1:=subject, category == “SignedMessage”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

Then

if ($PR.checkCertificate($vermeans)){

modify($PR){satisfied=true};

}

end

rule ” SignedMessage Verification with Certificate #2 – Placeholder”

when

$P1: Placeholder($pl1:=placeholderid)

$Op: Operation($pl1:=subject, name==“StegoRetrieve”)

$PR: Property ($pl1:=subject, category == “SignedMessage”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

Audit Log

rule ” Audit Log Verification – Sequence”

when

$P1: Placeholder($pl1:=placeholderid)

$P2: Placeholder($pl2:=placeholderid)

$OP: Operation(($pl2:=subject, operationType==”AuditLog”)

$ORCH: Sequence ($seq:=placeholderid, $pl1:=placeholdera, $pl2:=placeholderb)

$PR: Property ($seq:=subject, category==“AuditLog”, satisfied==false)

then

modify($pr2){satisfied=true};

End

rule ” Audit Log Verification with Certificate – Placeholder”

when

$P1: Placeholder($pl1:=placeholderid)

$Op: Operation($pl1:=subject, name==” Audit Log “)

$PR: Property ($pl1:=subject, category == “AuditLog”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

Authorisation

rule “Authorisation – Sequence”

when

$s: Sequence($sId:=id, $pA:=placeholdera, $pB:=placeholderb, $Link:=link)

Property($sId:=subject, category==“Authorisation”, satisfied==false)

Then

if ($pA.hasOperationType(“interface”)) {

insert(new Property($pA:=subject, category==“SingleAccessPoint”, satisfied==false);

insert(new Property($pA:=subject, category==“AuthorisationEnforcer”, satisfied==false);

}

if ($pA.hasOperationType(“interface”)) {

insert(new Property($pB:=subject, category==“SingleAccessPoint”, satisfied==false);

insert(new Property($pB:=subject, category==“AuthorisationEnforcer”, satisfied==false);

}

end

Authentication

rule “Authentication – Sequence”

when

$s: Sequence($sId:=id, $pA:=placeholdera, $pB:=placeholderb, $Link:=link)

Property($sId:=subject, category==“Authentication”, satisfied==false)

Then

insert(new Property($pA:=subject, category==“AuthenticationEnforcer”, satisfied==false);

insert(new Property($pA:=subject, category==“AuthenticatedSession”, satisfied==false);

insert(new Property($pA:=subject, category==“Blacklist”, satisfied==false);

insert(new Property($pA:=subject, category==“AccountLockout”, satisfied==false);

insert(new Property($pB:=subject, category==“AuthenticationEnforcer”, satisfied==false);

insert(new Property($pB:=subject, category==“AuthenticatedSession”, satisfied==false);

insert(new Property($pB:=subject, category==“Blacklist”, satisfied==false);

insert(new Property($pB:=subject, category==“AccountLockout”, satisfied==false);

insert(new Property($Link:=subject, category==“AuthenticatedChannel”, satisfied==false);

end

Anonymity

rule “Anonymisation – Sequence”

when

$P1: Placeholder($pl1:=placeholderid)

$P2: Placeholder($pl2:=placeholderid)

$PR1: Property($pl2:=subject, category==“Anonymity”, satisfied==true)

$P3: Placeholder($pl3:=placeholderid)

$s1: Sequence($sid1:=id, $pID1:=placeholderA, $pID2:=placeholderB)

$s2: Sequence($sid2:=id, $sID1:=placeholderA, $pID3:=placeholderB)

$PR2: Property($sID2:=subject, category==“Anonymity”, satisfied==false)

then

modify($PR2){satisfied=true};

End

rule “Anonymisation Verification with Certificate – Placeholder”

when

$P1: Placeholder($pID:=placeholderID)

$OP: Operation($opID:=operationID, $pID:=subject, operationType==“Anonymise”)

$PR: Property ($pID:=subject, category==“Anonymity”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

Pseudonymity

rule ” Pseudonymisation – Sequence”

when

$P1: Placeholder($pl1:=placeholderid)

$P2: Placeholder($pl2:=placeholderid)

$PR1: Property($pl2:=subject, category==“Pseudonymity”, satisfied==true)

$P3: Placeholder($pl3:=placeholderid) $s1: Sequence($sid1:=id, $pID1:=placeholderA, $pID2:=placeholderB)

$s2: Sequence($sid2:=id, $sID1:=placeholderA, $pID3:=placeholderB) $PR2: Property($sID2:=subject, category==“Pseudonymity”, satisfied==false)

then

modify($PR2){satisfied=true};

end

rule “Pseudonymisation Verification with Certificate – Placeholder”

when

$P1: Placeholder($pID:=placeholderID)

$OP: Operation($opID:=operationID, $pID:=subject, operationType==“Pseudonymise”)

$PR: Property ($pID:=subject, category==“Pseudonymity”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

Unlinkability

rule “Pseudonymisation – Sequence”

when

$P1: Placeholder($pl1:=placeholderid)

$P2: Placeholder($pl2:=placeholderid)

$PR1: Property($pl2:=subject, category==“Unlinkability”, satisfied==true)

$P3: Placeholder($pl3:=placeholderid)

$s1: Sequence($sid1:=id, $pID1:=placeholderA, $pID2:=placeholderB)

$s2: Sequence($sid2:=id, $sID1:=placeholderA, $pID3:=placeholderB)

$PR2: Property($sID2:=subject, category==“Unlinkability”, satisfied==false)

then

modify($PR2){satisfied=true};

end

rule “Unlinkability Verification with Certificate – Placeholder”

when

$P1: Placeholder($pID:=placeholderID)

$OP: Operation($opID:=operationID, $pID:=subject, operationType==“CoverTrafficGeneration”)

$PR: Property ($pID:=subject, category==“Unlinkability”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

Undetectability

rule ” Single Access Point Verification – Sequence”

when

$P1: Placeholder($pl1:=placeholderid)

$P2: Placeholder($pl2:=placeholderid)

$OP: Operation(($pl1:=subject, operationType==”StegoEmbed”)

$OP: Operation(($pl2:=subject, operationType==”StegoRetrieve”)

$ORCH: Sequence ($seq:=placeholderid, $pl1:=placeholdera, $pl2:=placeholderb)

$PR: Property ($seq:=subject, category==“Undetectability”, satisfied==false)

then

modify($pr2){satisfied=true};

end

rule “Undetectability Verification with Certificate #1 – Placeholder”

when

$P1: Placeholder($pl1:=placeholderid)

$Op: Operation($pl1:=subject, name==“StegoEmbed”)

$PR: Property ($pl1:=subject, category == “Undetectability”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

rule “Undetectability Verification with Certificate #2 – Placeholder”

when

$P1: Placeholder($pl1:=placeholderid)

$Op: Operation($pl1:=subject, name==“StegoRetrieve”)

$PR: Property ($pl1:=subject, category == “Undetectability”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

Redundancy

rule “Redundancy Verification”

when

$p1: Placeholder($pID1:=placeholderID)

$p2: Placeholder($pID2:=placeholderID, $placeholerType1:=type)

$p3: Placeholder($pID3:=placeholderID, $placeholerType2:=type, $placeholerType1==$placeholerType2)

$ch: Choice($chID:=id, $ pID1:=placeholderA, $pID2:=placeholderB, $pID3:=placeholderC)

$pr: Property($chID:=subject, category==“Redundancy”, satisfied==false)

then

modify($pr2){satisfied=true};

end

Fault Management

rule ” Fault Management – Sequence”

when

$P1: Placeholder($pl1:=placeholderid)

$P2: Placeholder($pl2:=placeholderid)

$ORCH: Sequence ($seq:=placeholderid, $pl1:=placeholdera, $pl2:=placeholderb)

$PR: Property ($seq:=subject, category==“FaultManagement”, satisfied==false)

then

insert(new Property($P1, “FaultManagement”, false));

insert(new Property($P2, “FaultManagement”, false));

end

rule ” Fault Management Verification with Certificate – Link”

when

$P: Placeholder($Id:=placeholderID)

$PR: Property ($Id:=subject, category == “FaultManagement”, verificationType == “Certificate”, $vermeans := means, satisfied==false)

then

if ($PR.checkCertificate($vermeans)) {

modify($PR){satisfied=true};

}

end

Technical Interoperability

rule “Sequence Technical Interoperability Verification”

when

Placeholder($pA:=placeholderid)

Property ($pA:=subject, category==“technical”, $prvaluein1:=input_value, $prvalueout1:=output_value, satisfied==true)

Placeholder($pB:=placeholderid)

Property ($pB:=subject, category==“technical”, $prvaluein2:=input_value, $prvalueout2:=out_value, satisfied==true)

Sequence($sId:=placeholderid, $pA:=placeholdera, $pB:=placeholderb)

$PR: Property ($sId:=subject, category==“technical”, $prvalueout1==$prvaluein2, satisfied==false)

then

modify($PR){satisfied=true, input_value=$prvaluein1, output_value=$prvalueout2};

end

Syntactic Interoperability

rule “Sequence Syntactic Interoperability Verification”

when

Placeholder($pA:=placeholderid)

Property ($pA:=subject, category==“dataFormat”, $prvaluein1:=input_value, $prvalueout1:=output_value, satisfied==true)

Placeholder($pB:=placeholderid)

Property ($pB:=subject, category==” dataFormat “, $prvaluein2:=input_value, $prvalueout2:=out_value, satisfied==true)

Sequence($sId:=placeholderid, $pA:=placeholdera, $pB:=placeholderb)

$PR: Property ($sId:=subject, category==” dataFormat “, $prvalueout1==$prvaluein2, satisfied==false)

then

modify($PR){satisfied=true, input_value=$prvaluein1, output_value=$prvalueout2};

end

Semantic Interoperability

rule “Sequence Semantic Interoperability Verification”

when

Placeholder($pA:=placeholderid)

Property ($pA:=subject, category==“semantic”, $prvaluein1:=input_value, $prvalueout1:=output_value, satisfied==true)

Placeholder($pB:=placeholderid)

Property ($pB:=subject, category==“semantic”, $prvaluein2:=input_value, $prvalueout2:=out_value, satisfied==true)

Sequence($sId:=placeholderid, $pA:=placeholdera, $pB:=placeholderb)

$PR: Property ($sId:=subject, category==“semantic”, $prvalueout1==$prvaluein2, satisfied==false)

then

modify($PR){satisfied=true, input_value=$prvaluein1, output_value=$prvalueout2};

end

Organisational Interoperability

rule “Sequence Organisational Interoperability Verification”

when

Placeholder($pA:=placeholderid)

Property ($pA:=subject, category==“Organisational “, $prvaluein1:=input_value, $prvalueout1:=output_value, satisfied==true)

Placeholder($pB:=placeholderid)

Property ($pB:=subject, category==“Organisational “, $prvaluein2:=input_value, $prvalueout2:=out_value, satisfied==true)

Sequence($sId:=placeholderid, $pA:=placeholdera, $pB:=placeholderb)

$PR: Property ($sId:=subject, category==“Organisational “, $prvalueout1==$prvaluein2, satisfied==false)

then

modify($PR){satisfied=true, input_value=$prvaluein1, output_value=$prvalueout2};

end

E2E Interoperability

rule “Sequence Interoperability”

when

Sequence($sId:=placeholderid)

$PR1: Property ($sId:=subject, category==“technical”, satisfied==true)

$PR2: Property ($sId:=subject, category==“dataFormat”, satisfied==true)

$PR3: Property ($sId:=subject, category==“semantic”, satisfied==true)

$PR4: Property ($sId:=subject, category==“E2E_WP_Interoperability”, satisfied==false)

then

modify($PR4){satisfied=true};

end

QoS Bandwidth

rule “Sequence – Decomposition”

when

$s: Sequence($sId:=placeholderid, $pA:=placeholdera, $pB:=placeholderb,$orchLink:=orchlink)

Property($sId:=subject, $prname:=propertyname, $prcategory:=category, $prvalue1:=value,  satisfied==false)

then

insert(new Property($rId,$prname+$prcategory+$pA,$prname, “required”, $prcategory, $prvalue1, “datastate”, $pA, “verificationtype”, “means”, false));

insert(new Property($rId,$prname+$prcategory+$pB,$prname, “required”, $prcategory, $prvalue1, “datastate”, $pB, “verificationtype”, “means”, false));

insert(new Property($rId,$prname+$prcategory+$orchLink,$prname, “required”, $prcategory, $prvalue1, “datastate”, $orchLink, “verificationtype”, “means”, false));

end

rule “Sequence Bandwidth Verification”

when

Placeholder($pA:=placeholderid)

Property ($pA:=subject, category==“qosbandwidth”, $prvalue1:=value,  satisfied==true)

Placeholder($pB:=placeholderid)

Property ($pB:=subject, category==“qosbandwidth”, $prvalue2:=value,  satisfied==true)

Link ($orchLink:=linkid)

Property ($orchLink:=subject, category==“qosbandwidth”, $prvalue3:=value, satisfied==true)

Sequence($sId:=placeholderid, $pA:=placeholdera, $pB:=placeholderb, $orchLink:=orchlink)

$PR: Property ($sId:=subject, category==“qosbandwidth”, $prvalue4:=value, $prvalue4<=$prvalue1, $prvalue4<=$prvalue2, $prvalue4<=$prvalue3, satisfied==false)

then

modify($PR){satisfied=true};

end

Virtual Service Network Function Verification

rule “Virtual Service Network Function Verification”

ruleflow-group “SFC”

salience 30

when

$src: Placeholder($srcName: name)

$dst: Placeholder($dstName: name)

$function: Function($type:=type, instantiated==true)

$chain: Chain($functions: functions, $functions not contains $function, instantiated==false)

$PR: Property($src:=src, $dst:=dst, $reqFunctions:=property.chain.functions, satisfied== false)

Function($type==type) from $reqFunctions

then     System.out.println(“Verification of Function”);

$chain.addFunction($function);update($chain);

end

Service Function Chain Verification

rule “Service Function Chaining Chain Verification”

salience 10

ruleflow-group “SFC”

when

$src: Placeholder($srcName: name)

$dst: Placeholder ($dstName: name)

$function: Function($type:=type, instantiated==true)

$chain: Chain($functions: functions, $functions contains $function, instantiated==true)

$PR: Property($src:=src, $dst:=dst, $reqFunctions:=property.chain.functions, satisfied== false)

then

System.out.println(“Verification of Chain”);

modify($PR){satisfied=true};

end

Service Function Chain Instantiation

rule “SFC Chain Instantiation”

ruleflow-group “SFC”

salience 20

when

$src: Placeholder($srcName: name)

$dst: Placeholder($dstName: name)

$function: Function($type:=type, instantiated==true)

$chain: Chain($functions: functions, $functions contains $function, instantiated==false)

$PR: Property($src:=src, $dst:=dst, $reqFunctions:=property.chain.functions, satisfied== false)

Function($type==type) from $reqFunctions

then

System.out.println(“Instantiation of Chain”);

modify($chain){instantiated=true};

end

Virtual Service Network Function Instantiation

rule “Virtual Service Network Function Instantiation”

ruleflow-group “SFC”

salience 40

when

$src: Placeholder($srcName: name)

$dst: Placeholder ($dstName: name)

$function: Function($type:=type, instantiated==false)

not Function($type:=type, instantiated==true)

$chain: Chain($functions: functions, $functions not contains $function, instantiated==false)

$PR: Property($src:=src, $dst:=dst, $reqFunctions:=property.chain.functions, satisfied== false)

Function($type==type) from $reqFunctions

then

System.out.println(“Instantiation of Function”);

Function function = new Function($function.type);

modify($function){instantiated=true};

end

Composition Reliability

rule “Serial Reliable Composition”

when

$A: Placeholder($input : operation.inputs, $intData: parameters.outputs, $r1:= reliabilityValue)

$B: Placeholder(parameters.inputs == $intData, $output: parameters.outputs, $r2:= reliabilityValue)

$ORCH: Sequence(parameters.inputs:= $input, parameters.outputs == $output, firstActivity == $A, secondActivity == $B)

$OP: Property(subject:= $ORCH, propertyName== “Reliability“, $rel:= propertyValue, $rel<= $r1*$r2, satisfied == false)

$SP: PropertyPlan(property contains $OP)

then

PropertyPlan newPropertyPlan = new PropertyPlan($SP);

newPropertyPlan.removeProperty($OP);

Property NP_A = new Property($OP, “Reliability”, $A);

newPropertyPlan.getProperty().add(NP_A);

insert(NP_A);

Property NP_B = new Property($OP, “Reliability”, $B);

newPropertyPlan.getProperty().add(NP_B);insert(NP_B);

insert(newPropertyPlan);

modify($OP){satisfied=true};

end