--------------------------------------------- ------------ PRELIMINARIES ------------------ --------------------------------------------- fmod UNIVERSE is sorts Group User Role Purpose DataType DataValue PrivateDataType PrivateDataValue . subsorts User Role < Group . subsorts PrivateDataType < DataType . subsorts PrivateDataValue < DataValue . endfm view Group from TRIV to UNIVERSE is sort Elt to Group . endv view Purpose from TRIV to UNIVERSE is sort Elt to Purpose . endv view DataType from TRIV to UNIVERSE is sort Elt to DataType . endv view DataValue from TRIV to UNIVERSE is sort Elt to DataValue . endv --------------------------------------------- ------------ PRIVACY POLICIES --------------- --------------------------------------------- fmod PRIVACY-LANGUAGE-SORTS is sorts Permission Hierarchy Condition . endfm view Hierarchy from TRIV to PRIVACY-LANGUAGE-SORTS is sort Elt to Hierarchy . endv view Permission from TRIV to PRIVACY-LANGUAGE-SORTS is sort Elt to Permission . endv fmod PRIVACY-LANGUAGE-CONDITIONS is protecting UNIVERSE . extending PRIVACY-LANGUAGE-SORTS . extending SET{DataType} * ( op _`,_ to __ , op empty to empty-X , op insert to insert-X , op delete to delete-X , op _in_ to _X-in_ , op |_| to card-X , op $card to $card-X , op union to union-X , op intersection to intersection-X , op $intersect to $intersect-X , op _\_ to _diff-X_ , op $diff to $diff-X , op _subset_ to _subset-X_ , op _psubset_ to _psubset-X_ ) . extending SET{DataValue} * ( op _`,_ to __ , op empty to empty-V , op insert to insert-V , op delete to delete-V , op _in_ to _V-in_ , op |_| to card-V , op $card to $card-V , op union to union-V , op intersection to intersection-V , op $intersect to $intersect-V , op _\_ to _diff-V_ , op $diff to $diff-V , op _subset_ to _subset-V_ , op _psubset_ to _psubset-V_ ) . ---these set operators are renamed ---for compatibility with further imports of supersort sets vars X Y : DataType . vars XS YS : Set{DataType} . vars VAL VAL1 VAL2 VAL' : DataValue . vars COND COND' COND1 COND2 : Condition . op domain : DataType -> Set{DataValue} . op var : DataValue -> DataType . op _==_ : DataType DataValue -> [Condition] [ctor prec 14]. op _=/=_ : DataType DataValue -> [Condition] [ctor prec 14]. cmb X == VAL : Condition if VAL V-in domain(X) . cmb X =/= VAL : Condition if VAL V-in domain(X) . op _/\_ : Condition Condition -> Condition [ctor assoc comm prec 15]. op vars : Condition -> Set{DataType} . eq vars(X == VAL) = X . eq vars(X =/= VAL) = X . eq vars(COND1 /\ COND2) = union-X(vars(COND1), vars(COND2)) . op _<=_ : Condition Condition -> Bool . eq COND <= COND = true . eq COND <= COND' = vars(COND') subset-X vars(COND) and $stricter-than(COND, COND', vars(COND')) . op $stricter-than : Condition Condition Set{DataType} -> Bool . eq $stricter-than(COND, COND', empty-X) = true . eq $stricter-than(COND, COND', (X XS)) = allowed(COND, X) subset-V allowed(COND', X) and $stricter-than(COND, COND', XS) . op allowed : Condition DataType -> Set{DataValue} . eq allowed(X == VAL, X) = VAL . eq allowed(X == VAL, Y) = domain(Y) . eq allowed(X =/= VAL, X) = delete-V(VAL, domain(X)) . eq allowed(X =/= VAL, Y) = domain(Y) . eq allowed(COND1 /\ COND2, X) = intersection-V(allowed(COND1, X), allowed(COND2, X)) . endfm fmod PRIVACY-LANGUAGE-PERMISSIONS is protecting UNIVERSE . protecting PRIVACY-LANGUAGE-CONDITIONS . extending PRIVACY-LANGUAGE-SORTS . extending SET{Permission} * (op (_`,_) to __ [prec 28]). sorts UnconditionalPermission ConditionalPermission . subsorts ConditionalPermission UnconditionalPermission < Permission . vars COND COND' : Condition . var P : Permission . var P+ : UnconditionalPermission . vars PS PS' PS1 PS2 : Set{Permission} . var NEPS : NeSet{Permission} . ----------- Define Permissions ----------- ops read write access : -> UnconditionalPermission [ctor]. op disc_ : Group -> UnconditionalPermission [ctor prec 15]. op _if_ : UnconditionalPermission Condition -> ConditionalPermission [ctor prec 16] . op _+_ : Condition Set{Permission} -> Set{Permission} [prec 17] . eq COND + empty = empty . eq COND + P+ = P+ if COND . eq COND + P if COND' = P if COND /\ COND' . eq COND + (P NEPS) = (COND + P) (COND + NEPS) . op _<=_ : Set{Permission} Set{Permission} -> Bool . eq empty <= PS = true . eq P if COND PS <= P if COND' PS' = COND <= COND' and PS <= P if COND' PS' . eq P if COND PS <= P PS' = PS <= P PS' . eq P PS <= P PS' = PS <= P PS' . eq PS1 <= PS2 = false [owise] . endfm fmod PRIVACY-LANGUAGE-HIERARCHIES is protecting UNIVERSE . extending PRIVACY-LANGUAGE-SORTS . protecting SET{Group} . extending SET{Hierarchy} . protecting SET{Purpose} * (op (_`,_) to __ [prec 28]). vars G G' : Group . var R : Role . var USER : User . var PURP : Purpose . var PURPS : Set{Purpose} . var H : Hierarchy . var HS : Set{Hierarchy} . ----------- Define Hierarchy --------------- op nil : -> Hierarchy [ctor]. op _:_`[_`] : Group Set{Purpose} NeSet{Hierarchy} ~> Hierarchy [ctor]. op _:_ : Group Set{Purpose} -> Hierarchy . eq G : PURPS = G : PURPS[nil] . op _`[_`] : Group NeSet{Hierarchy} ~> Hierarchy . eq G[HS] = G : empty[HS] . op _`[`] : Group -> Hierarchy . eq G [] = G : empty[nil] . op cyclicalHierarchyError : -> [Hierarchy] . cmb R : PURPS[HS] : Hierarchy if not R in groups(HS) . cmb USER : PURPS[HS] : Hierarchy if HS = nil . ceq G : PURPS[HS] = cyclicalHierarchyError if G in groups(HS) . op groups : Set{Hierarchy} -> Set{Group} . eq groups(nil) = empty . eq groups(G : PURPS[HS]) = insert(G, groups(HS)). eq groups(empty) = empty . eq groups((H, HS)) = union(groups(H), groups(HS)) . op root : Hierarchy -> Set{Group} . eq root(nil) = empty . eq root(G : PURPS[HS]) = G . op _->_ : Purpose Set{Hierarchy} -> Set{Hierarchy} . eq PURP -> nil = nil . eq PURP -> G : PURPS[HS] = G : insert(PURP, PURPS)[HS] . eq PURP -> (H, HS) = (PURP -> H, PURP -> HS) . endfm fmod PRIVACY-LANGUAGE-POLICIES is protecting PRIVACY-LANGUAGE-PERMISSIONS . protecting PRIVACY-LANGUAGE-HIERARCHIES . sorts PermissionFunction Policy . var PDT : PrivateDataType . vars G G' : Group . var R : Role . var USER : User . vars GS GS' : Set{Group} . var PURP : Purpose . var PURPS : Set{Purpose} . vars P P1 P2 P' : Permission . vars PS PS' PS1 PS2 : Set{Permission} . var NEPS : NeSet{Permission} . vars H H1 H2 : Hierarchy . vars HS HS' : Set{Hierarchy} . vars POL POL1 POL2 : Policy . vars PF PF1 PF2 : PermissionFunction . var COND : Condition . ----------- Define Permission Function ----------- op (p`(_`,_`)=_) : Purpose Group Set{Permission} -> PermissionFunction [ctor prec 29] . op _`,_ : PermissionFunction PermissionFunction -> PermissionFunction [ctor assoc comm prec 30] . op (_`(_`,_`)) : PermissionFunction Purpose Group -> Set{Permission} . eq (p(PURP, G) = PS)(PURP, G) = PS . eq (PF1, PF2)(PURP,G) = union(PF1(PURP,G), PF2(PURP,G)) . eq PF(PURP,G) = empty [owise] . op purposes : PermissionFunction -> Set{Purpose} . eq purposes(PF1, PF2) = union(purposes(PF1), purposes(PF2)) . eq purposes(p(PURP, G) = PS) = PURP . --------------- Define Policy --------------- op _>>_`,_ : PrivateDataType Hierarchy PermissionFunction -> Policy [ctor prec 35] . op _;_ : Policy Policy ~> Policy [ctor assoc comm prec 40] . op types : Policy -> Set{DataType} . eq types(PDT >> H , PF) = PDT . eq types(POL1 ; POL2) = union-X(types(POL1), types(POL2)) . op multiplePoliciesForType : PrivateDataType -> [Policy] . cmb POL1 ; POL2 : Policy if intersection-X(types(POL1), types(POL2)) = empty-X . eq PDT >> H1, PF1 ; PDT >> H2, PF2 = multiplePoliciesForType(PDT) . endfm fmod PRIVACY-LANGUAGE is protecting PRIVACY-LANGUAGE-POLICIES . endfm --------------------------------------------- ------------ PRIVACY CALCULUS --------------- --------------------------------------------- fmod PRIVACY-CALCULUS-SORTS is protecting UNIVERSE . protecting SET{Group} . sorts Name Type . var T T' : Type . var G : Group . --------------- Types --------------- subsort DataType < Type . op _`[_`] : Group Type -> Type [ctor prec 15] . op fg : Type -> Set{Group} . eq fg(G[T]) = insert(G, fg(T)) . eq fg(T) = empty [owise] . op carrying : Type -> [Type] . cmb carrying(T) : Type if G[T'] := T . eq carrying(G[T]) = T . endfm view Name from TRIV to PRIVACY-CALCULUS-SORTS is sort Elt to Name . endv view Type from TRIV to PRIVACY-CALCULUS-SORTS is sort Elt to Type . endv fmod PRIVACY-CALCULUS-CINNI is protecting QID . extending UNIVERSE . extending PRIVACY-CALCULUS-SORTS . extending SET{Name} . sorts NameId IndexedName . subsort Qid < NameId . subsorts IndexedName DataValue < Name . sort Subst . vars X Y : Name . vars A B : NameId . var N : Nat . var SUBST : Subst . op _`{_`} : NameId Nat -> IndexedName [ctor prec 13]. op IDof : IndexedName -> NameId . eq IDof(A{N}) = A . op `[_:=_`] : NameId Name -> Subst [ctor prec 15] . op `[shiftup_`] : NameId -> Subst [ctor prec 15] . op `[shiftdown_`] : NameId -> Subst [ctor prec 15] . op `[lift__`] : NameId Subst -> Subst [ctor prec 15] . op __ : Subst Name -> Name [prec 16] . eq [A := X] A{0} = X . eq [A := X] A{s N} = A{N} . eq [A := X] Y = Y [owise] . eq [shiftup A] A{N} = A{s N} . eq [shiftup A] Y = Y [owise] . eq [shiftdown A] A{s N} = A{N} . eq [shiftdown A] Y = Y [owise] . eq [lift A SUBST] A{0} = A{0} . eq [lift A SUBST] A{s N} = [shiftup A] (SUBST A{N}) . eq [lift A SUBST] Y = [shiftup A] (SUBST Y) [owise] . op __ : Subst Set{Name} -> Set{Name} [ditto] . eq SUBST empty = empty . eq SUBST (X, NEXS:NeSet{Name}) = (SUBST X), SUBST NEXS:NeSet{Name} . endfm fmod PRIVACY-CALCULUS-PROCESSES is extending PRIVACY-CALCULUS-SORTS . protecting PRIVACY-CALCULUS-CINNI . sorts Process NeProcess . subsort NeProcess < Process . vars X Y : Name . vars A B : NameId . var SUBST : Subst . var T : Type . vars P P1 P2 : Process . vars NEP1 NEP2 : NeProcess . --------------- The empty process --------------- op 0P : -> Process [ctor] . --------------- Repeating process --------------- op !_ : Process -> Process [frozen prec 17] . op !_ : NeProcess -> NeProcess [ctor ditto] . --------------- Parallel processes --------------- op _|_ : Process Process -> Process [frozen assoc comm id: 0P prec 19] . op _|_ : Process NeProcess -> NeProcess [ditto] . op _|_ : NeProcess NeProcess -> NeProcess [ctor ditto] . --------------- Name binding --------------- op (`(v_:_`)_) : NameId Type Process -> Process [frozen(3) prec 17] . op (`(v_:_`)_) : NameId Type NeProcess -> NeProcess [ctor ditto] . --------------- Input process --------------- op (in_`(_:_`)._) : IndexedName NameId Type Process -> NeProcess [frozen(4) ctor prec 17] . --- shortcut for binding to the closest binder op (in_`(_:_`)._) : NameId NameId Type Process -> NeProcess [frozen(4) prec 17] . eq in A(B : T). P = in A{0}(B : T). P . --------------- Output process --------------- op (out_`(_`)._) : IndexedName Name Process -> NeProcess [frozen(3) ctor prec 17]. --- shortcuts for binding to the closest binder op (out_`(_`)._) : IndexedName NameId Process -> NeProcess [frozen(3) prec 17]. op (out_`(_`)._) : NameId Name Process -> NeProcess [frozen(3) prec 17]. op (out_`(_`)._) : NameId NameId Process -> NeProcess [frozen(3) prec 17]. eq out X(B). P = out X(B{0}). P . eq out A(Y). P = out A{0}(Y). P . eq out A(B). P = out A{0}(B{0}). P . --------------- Conditional process --------------- op (`[_==_`]`(_;_`)) : Name Name Process Process -> NeProcess [frozen(3 4) ctor] . --- normal form ceq [Y == X](P1 ; P2) = [X == Y](P1 ; P2) if Y : DataValue /\ not X :: DataValue . --- shortcuts for binding to the closest binder op (`[_==_`]`(_;_`)) : NameId Name Process Process -> NeProcess [frozen(3 4)] . op (`[_==_`]`(_;_`)) : NameId NameId Process Process -> NeProcess [frozen(3 4)] . op (`[_==_`]`(_;_`)) : Name NameId Process Process -> NeProcess [frozen(3 4)] . eq [A == X](P1 ; P2) = [A{0} == X](P1 ; P2) . eq [X == A](P1 ; P2) = [X == A{0}](P1 ; P2) . eq [A == B](P1 ; P2) = [A{0} == B{0}](P1 ; P2) . --- shortcuts without else branch op `[_==_`]_ : Name Name Process -> NeProcess [frozen(3) prec 17] . op `[_=/=_`]_ : Name Name Process -> NeProcess [frozen(3) prec 17] . eq [X == Y]P = [X == Y] (P ; 0P) . eq [X =/= Y]P = [X == Y] (0P ; P) . --- shortcuts without else branch and for binding to the closest binder op `[_==_`]_ : NameId Name Process -> NeProcess [frozen(3) prec 17] . op `[_==_`]_ : NameId NameId Process -> NeProcess [frozen(3) prec 17] . op `[_==_`]_ : Name NameId Process -> NeProcess [frozen(3) prec 17] . op `[_=/=_`]_ : NameId Name Process -> NeProcess [frozen(3) prec 17] . op `[_=/=_`]_ : NameId NameId Process -> NeProcess [frozen(3) prec 17] . op `[_=/=_`]_ : Name NameId Process -> NeProcess [frozen(3) prec 17] . eq [A == Y]P = [A{0} == Y] P . eq [Y == A]P = [Y == A{0}] P . eq [A == B]P = [A{0} == B{0}] P . eq [A =/= Y]P = [A{0} =/= Y] P . eq [Y =/= A]P = [Y =/= A{0}] P . eq [A =/= B]P = [A{0} =/= B{0}] P . --------------- Free names --------------- ops fn : Process -> Set{Name} . eq fn(0P) = empty . eq fn(! P) = fn(P) . eq fn(NEP1 | NEP2) = union(fn(NEP1), fn(NEP2)) . eq fn((v A : T) P) = [shiftdown A] delete(A{0}, fn(P)) . eq fn(in X(A : T). P) = insert(X, [shiftdown A] delete(A{0}, fn(P))) . eq fn(out X(Y). P) = insert(X, insert(Y, fn(P))) . eq fn([X == Y] (P1 ; P2)) = insert(X, insert(Y, union(fn(P1), fn(P2)))) . --------------- Free groups --------------- op fg : Process -> Set{Group} . eq fg(0P) = empty . eq fg(! P) = fg(P) . eq fg(NEP1 | NEP2) = union(fg(NEP1), fg(NEP2)) . eq fg((v A : T) P) = union(fg(P), fg(T)) . eq fg(in X(A : T). P) = union(fg(P), fg(T)) . eq fg(out X(Y). P) = fg(P) . eq fg([X == Y] (P1 ; P2)) = union(fg(P1), fg(P2)) . --------------- Name substitution --------------- op __ : Subst Process -> Process [prec 16] . op __ : Subst NeProcess -> NeProcess [ditto] . eq SUBST 0P = 0P . eq SUBST (! P) = ! (SUBST P) . eq SUBST (NEP1 | NEP2) = (SUBST NEP1) | (SUBST NEP2) . eq SUBST ((v A : T) P) = (v A : T) [lift A SUBST] P . eq SUBST (in X(A : T). P) = in (SUBST X)(A : T). [lift A SUBST] P . eq SUBST (out X(Y). P) = out (SUBST X)(SUBST Y). SUBST P . eq SUBST ([X == Y] (P1 ; P2)) = [SUBST X == SUBST Y] (SUBST P1 ; SUBST P2) . endfm fmod PRIVACY-CALCULUS-SYSTEMS is protecting PRIVACY-CALCULUS-PROCESSES . sorts System NeSystem . subsort NeSystem < System . vars X Y : Name . vars A B : NameId . var SUBST : Subst . var T : Type . var P : Process . var S : System . vars NES1 NES2 : NeSystem . var G : Group . var R : Role . var PURP : Purpose . op 0S : -> System [ctor] . op _||_ : System System -> System [frozen assoc comm id: 0S prec 25] . op _||_ : System NeSystem -> NeSystem [ditto] . op _||_ : NeSystem NeSystem -> NeSystem [ctor ditto] . op (`(v_:_`)_) : NameId Type System -> System [frozen(3) prec 23]. op (`(v_:_`)_) : NameId Type NeSystem -> NeSystem [ctor ditto] . op _:_`[_`] : Group Purpose Process -> System [frozen(2) prec 21] . op _:_`[_`] : Group Purpose NeProcess -> NeSystem [ctor ditto] . op _`[_`] : Role System -> System [frozen(2) prec 23] . op _`[_`] : Role NeSystem -> NeSystem [ctor ditto] . --------------- Free names --------------- ops fn : System -> Set{Name} . eq fn(0S) = empty . eq fn(NES1 || NES2) = union(fn(NES1), fn(NES2)) . eq fn((v A : T) S) = [shiftdown A] delete(A{0}, fn(S)) . eq fn(G : PURP[P]) = fn(P) . eq fn(R[S]) = fn(S) . --------------- Free and bound groups --------------- ops fg bg : System -> Set{Group} . eq fg(0S) = empty . eq fg(NES1 || NES2) = union(fg(NES1), fg(NES2)) . eq fg((v A : T) S) = union(fg(S), fg(T)) . eq fg(G : PURP[P]) = delete(G, fg(P)) . eq fg(R[S]) = delete(R, bg(S)) . eq bg(0S) = empty . eq bg(NES1 || NES2) = union(bg(NES1), bg(NES2)) . eq bg((v A : T) S) = bg(S) . eq bg(G : PURP[P]) = G . eq bg(R[S]) = insert(R, bg(S)) . --------------- Name substitution --------------- op __ : Subst System -> System [prec 16] . op __ : Subst NeSystem -> NeSystem [ditto] . eq SUBST 0S = 0S . eq SUBST (NES1 || NES2) = (SUBST NES1) || (SUBST NES2) . eq SUBST ((v A : T) S) = (v A : T) [lift A SUBST] S . eq SUBST (G : PURP[P]) = G : PURP[SUBST P] . eq SUBST (R[S]) = R[SUBST S] . endfm fmod PRIVACY-CALCULUS-SYNTAX is protecting PRIVACY-CALCULUS-PROCESSES . protecting PRIVACY-CALCULUS-SYSTEMS . endfm mod PRIVACY-CALCULUS-SEMANTICS is extending PRIVACY-CALCULUS-SYNTAX . vars X Y Z : Name . var A : NameId . var SUBST : Subst . vars XS YS : Set{Name} . var T : Type . vars P P' P1 P2 P1' P2' : Process . vars NEP1 NEP2 NEP1' NEP2' : NeProcess . var S S1 S2 S' : System . vars NES1 NES2 NES1' NES2' : NeSystem . var G : Group . var R : Role . var PURP : Purpose . ------------- Structural congruence ------------- eq ! 0P = 0P . eq (v A : T) 0P = 0P . eq (v A : T) 0S = 0S . eq G : PURP [0P] = 0S . eq R[0S] = 0S . ------------- Labels ------------- sort Label . vars l l' l1 l2 : Label . op silent : -> Label . op (in _`(_`)) : Name NameId -> Label . op (out _`(_`)) : Name Name -> Label . op (vout_`(_:_`)) : Name Name Type -> Label . ops fn bn : Label -> Set{Name} . eq fn(silent) = empty . eq fn(in X(A)) = X . eq fn(out X(Y)) = insert(X, Y) . eq fn(vout X(Y : T)) = X . eq bn(silent) = empty . eq bn(in X(A)) = empty . ---TODO: is this correct? eq bn(out X(Y)) = empty . eq bn(vout X(Y : T)) = Y . op __ : Subst Label -> Label [prec 22] . eq SUBST silent = silent . eq SUBST in X(A) = in SUBST X(A) . ---TODO: is this correct? eq SUBST out X(Y) = out SUBST X(SUBST Y) . eq SUBST vout X(Y : T) = vout SUBST X(SUBST Y : T) . ------------- Labelled transitions ------------- sorts ActProcess ActSystem . subsort Process < ActProcess . subsort System < ActSystem . op `{_`}_ : Label ActProcess -> ActProcess [frozen(2)] . op `{_`}_ : Label ActSystem -> ActSystem [frozen(2)] . rl [In] : in X(A : T). P => {in X(A)} P . rl [Out] : out X(Y). P => {out X(Y)} P . crl [Rep] : ! P => {l} P' | ! P if P => {l} P' . crl [CondT] : [X == X] (P1 ; P2) => {l} P1' if P1 => {l} P1' . crl [CondF] : [X == Y] (P1 ; P2) => {l} P2' if X =/= Y /\ P2 => {l} P2' . crl [ResGS] : G[S] => {l} G[S'] if S => {l} S' . crl [ResGP] : G : PURP [P] => {l} G : PURP [P'] if P => {l} P' . crl [ResNP] : (v A : T) P => {[shiftdown A] l} (v A : T) P' if P => {l} P' /\ not A{0} in fn(l) . crl [ResNS] : (v A : T) S => {[shiftdown A] l} (v A : T) S' if S => {l} S' /\ not A{0} in fn(l) . crl [OpenP]:(v A : T) P => {vout X(A{0} : T)} P' if P => {out X(A{0})} P' . crl [OpenS]:(v A : T) S => {vout X(A{0} : T)} S' if S => {out X(A{0})} S' . crl [CommP] : NEP1 | NEP2 => {silent} ([A := Z] P1) | P2 if NEP1 => {in X(A)} P1 /\ NEP2 => {out X(Z)} P2 . crl [CommS] : NES1 || NES2 => {silent} ([A := Z] S1) || S2 if NES1 => {in X(A)} S1 /\ NES2 => {out X(Z)} S2 . crl [CloseP]: NEP1 | NEP2 => {silent} (v IDof(Z) : T)(([A := Z][shiftup IDof(Z)] P1) | P2) if NEP1 => {in X(A)} P1 /\ NEP2 => {vout X(Z : T)} P2 . crl [CloseS]: NES1 || NES2 => {silent} (v IDof(Z) : T)(([A := Z][shiftup IDof(Z)] S1) || S2) if NES1 => {in X(A)} S1 /\ NES2 => {vout X(Z : T)} S2 . crl [ParP] : NEP1 | NEP2 => {l} P1 | NEP2 if NEP1 => {l} P1 /\ intersection(bn(l), fn(NEP2)) = empty . crl [ParS] : NES1 || NES2 => {l} S1 || NES2 if NES1 => {l} S1 /\ intersection(bn(l), fn(NES2)) = empty . var AP : ActProcess . sort TraceProcess . subsort TraceProcess < ActProcess . op `[_`] : Process -> TraceProcess [frozen] . crl [reflP] : [ P ] => {l}P' if P => {l}P' . crl [transP] : [ P ] => {l}AP if P => {l}P' /\ [ P' ] => AP /\ AP =/= [ P' ]. var AS : ActSystem . sort TraceSystem . subsort TraceSystem < ActSystem . op `[_`] : System -> TraceSystem [frozen] . crl [reflS] : [ S ] => {l}S' if S => {l}S' . crl [transS] : [ S ] => {l}AS if S => {l}S' /\ [ S' ] => AS /\ AS =/= [ S' ]. endm ------------------------------------------ ------------ TYPE CHECKING --------------- ------------------------------------------ fmod TYPE-SYSTEM-GAMMA-ENVIRONMENTS is protecting PRIVACY-CALCULUS-CINNI . protecting PRIVACY-LANGUAGE-CONDITIONS . sorts GEnvironment NeGEnvironment . subsort NeGEnvironment < GEnvironment . var X : Name . var SUBST : Subst . vars T T' : Type . var G : Group . var COND : Condition . vars NEGAMMA NEGAMMA1 NEGAMMA2 : NeGEnvironment . op none : -> GEnvironment [ctor] . op _:_ : Name Type -> NeGEnvironment [ctor prec 35] . op group:_ : Group -> NeGEnvironment [ctor prec 35] . op cond:_ : Condition -> NeGEnvironment [ctor prec 35] . op _._ : GEnvironment GEnvironment -> GEnvironment [assoc comm id: none prec 40] . op _._ : NeGEnvironment GEnvironment -> NeGEnvironment [ctor ditto] . ---TODO: operator _._ is not always well-defined op nameAppearsTwice : Name -> [GEnvironment] . eq X : T . X : T' = nameAppearsTwice(X) . eq nameAppearsTwice(X) . NEGAMMA = nameAppearsTwice(X) . op groups : GEnvironment -> Set{Group} . eq groups(none) = empty . eq groups(X : T) = empty . eq groups(group: G) = G . eq groups(cond: COND) = empty . eq groups(NEGAMMA1 . NEGAMMA2) = union(groups(NEGAMMA1), groups(NEGAMMA2)). op names : GEnvironment -> Set{Name} . eq names(none) = empty . eq names(group: G) = empty . eq names(cond: COND) = empty . eq names(X : T) = X . eq names(NEGAMMA1 . NEGAMMA2) = union(names(NEGAMMA1), names(NEGAMMA2)) . op __ : Subst GEnvironment -> GEnvironment . eq SUBST none = none . eq SUBST (X : T) = (SUBST X) : T . eq SUBST (group: G) = group: G . eq SUBST (cond: COND) = cond: COND . eq SUBST (NEGAMMA1 . NEGAMMA2) = (SUBST NEGAMMA1) . (SUBST NEGAMMA2) . endfm fmod TYPE-SYSTEM-DELTA-ENVIRONMENTS is protecting PRIVACY-LANGUAGE-PERMISSIONS . protecting PRIVACY-CALCULUS-SORTS . protecting SET{Type} . sorts DEnvironment NeDEnvironment . subsort NeDEnvironment < DEnvironment . var T : Type . var TS : Set{Type} . var PDT : PrivateDataType . vars G G' : Group . var COND : Condition . var PS : Set{Permission} . vars D D1 D2 : DEnvironment . vars NED1 NED2 : NeDEnvironment . op none : -> DEnvironment [ctor] . op _:_ : PrivateDataType Set{Permission} -> NeDEnvironment [ctor prec 35] . op _._ : NeDEnvironment DEnvironment ~> NeDEnvironment [ctor assoc comm id: none prec 40] . op _._ : DEnvironment DEnvironment ~> DEnvironment [ctor ditto] . --- TODO: remove ctor tag without breaking constructor consistency cmb NED1 . NED2 : NeDEnvironment if intersection(types(NED1), types(NED2)) = empty . op types : DEnvironment -> Set{Type} . eq types(none) = empty . eq types(PDT : PS) = PDT . eq types(NED1 . NED2) = union(types(NED1), types(NED2)) . op permissions : DEnvironment DataType -> Set{Permission} . eq permissions(PDT : PS . D, PDT) = PS . eq permissions(D, PDT) = empty [owise] . --------------- Auxuliary functions --------------- op Dr : Type -> DEnvironment . eq Dr(PDT) = PDT : read . eq Dr(G [PDT]) = PDT : access . eq Dr(T) = none [owise] . op Dw : Type -> DEnvironment . eq Dw(G[PDT]) = PDT : write . eq Dw(G [G' [PDT]]) = PDT : disc G . eq Dw(T) = none [owise] . op _+_ : Condition DEnvironment -> DEnvironment . eq COND + none = none . eq COND + PDT : PS = PDT : COND + PS . eq COND + (NED1 . NED2) = (COND + NED1) . (COND + NED2) . op _+_ : DEnvironment DEnvironment ~> DEnvironment [assoc comm id: none prec 41] . op _+_ : NeDEnvironment DEnvironment ~> NeDEnvironment [ditto]. cmb NED1 + NED2 : NeDEnvironment if NED1 : NeDEnvironment /\ NED2 : NeDEnvironment . eq NED1 + NED2 = $+(NED1, NED2, union(types(NED1), types(NED2))) . op $+ : NeDEnvironment NeDEnvironment Set{Type} -> NeDEnvironment . eq $+(D1, D2, empty) = none . eq $+(D1, D2, (PDT, TS)) = $+(D1, D2, TS) . PDT : union(permissions(D1, PDT), permissions(D2,PDT)) . endfm fmod TYPE-SYSTEM-THETA-INTERFACES is protecting PRIVACY-LANGUAGE-POLICIES . protecting TYPE-SYSTEM-DELTA-ENVIRONMENTS . sorts InterfaceHierarchy ThInterface NeThInterface . subsort NeThInterface < ThInterface . subsort InterfaceHierarchy < Hierarchy . var PDT : PrivateDataType . vars G G' : Group . var PURP : Purpose . var PURPS PURPS' : Set{Purpose} . var PS : Set{Permission} . var H : Hierarchy . var HS : Set{Hierarchy} . var NeHS : NeSet{Hierarchy} . vars NED1 NED2 : NeDEnvironment . vars NETH1 NETH2 : NeThInterface . var HTH : InterfaceHierarchy . ----------- Define InterfaceHierarchy ----------- op _`[_`] : Group Purpose -> InterfaceHierarchy [ctor] . op _`[_`] : Group InterfaceHierarchy -> InterfaceHierarchy [ctor]. eq G[PURPS] = G : PURPS [nil] . cmb G : PURPS [HS] : InterfaceHierarchy if HS = nil /\ | PURPS | = s 0 . cmb G : PURPS [HS] : InterfaceHierarchy if PURPS = empty /\ | HS | = s 0 /\ HS =/= nil . ---you can write G' : PURPS' [NEHS] := HS ---instead of HS =/= nil op purpose : InterfaceHierarchy -> Purpose . eq purpose(G : PURP [nil]) = PURP . eq purpose(G : empty [H]) = purpose(H) . --------------- Define ThInterface --------------- op none : -> ThInterface [ctor] . op _>>`(_`,_`) : PrivateDataType InterfaceHierarchy Set{Permission} -> NeThInterface [ctor prec 35] . op _;_ : ThInterface ThInterface ~> ThInterface [ctor assoc comm id: none prec 40] . ---TODO: remove ctor without breaking constructor consistency op _;_ : NeThInterface ThInterface ~> NeThInterface [ctor ditto] . cmb NETH1 ; NETH2 : NeThInterface if NETH1 : NeThInterface /\ NETH2 : NeThInterface . --------------- Auxuliary functions --------------- op _`[_`]+_ : Group Purpose DEnvironment -> ThInterface [prec 35] . op _`[_`]+_ : Group Purpose NeDEnvironment -> NeThInterface [ditto]. eq G[PURP] + none = none . eq G[PURP] + (PDT : PS) = PDT >> (G[PURP], PS) . eq G[PURP] + (NED1 . NED2) = G[PURP] + NED1 ; G[PURP] + NED2 . op _+_ : Group ThInterface -> ThInterface [prec 35] . op _+_ : Group NeThInterface -> NeThInterface [ditto] . eq G + none = none . eq G + (PDT >> (HTH, PS)) = PDT >> (G[HTH], PS) . eq G + (NETH1 ; NETH2) = G + NETH1 ; G + NETH2 . endfm fmod POLICY-SATISFACTION is protecting TYPE-SYSTEM-THETA-INTERFACES . protecting PRIVACY-LANGUAGE . var PDT : PrivateDataType . var G : Group . var GS : Set{Group} . var PURP : Purpose . var PURPS : Set{Purpose} . var H : Hierarchy . var HS : Set{Hierarchy} . var PS : Set{Permission} . var POL : Policy . var PF : PermissionFunction . var HTH : InterfaceHierarchy . vars NETH1 NETH2 : NeThInterface . var TH : ThInterface . op perms : PermissionFunction Hierarchy Set{Group} Purpose ~> Set{Permission} . op $perms : PermissionFunction Set{Hierarchy} Set{Group} Purpose -> Set{Permission} . op incompatibleHierarchy : Hierarchy Set{Group} -> [Set{Permission}]. eq perms(PF, nil, GS, PURP) = empty . eq perms(PF, H, empty, PURP) = empty . ceq perms(PF, G : PURPS [HS], GS, PURP) = incompatibleHierarchy(G : PURPS[HS], GS) if not G in GS . eq perms(PF, G : PURPS [HS], GS, PURP) = union(if PURP in PURPS then PF(PURP, G) else empty fi, $perms(PF, if PURP in PURPS then PURP -> HS else HS fi, intersection(groups(HS), GS), PURP)) . eq $perms(PF, empty, GS, PURP) = empty . eq $perms(PF, (H, HS), GS, PURP) = union( if root(H) subset GS then perms(PF, H, GS, PURP) else empty fi, $perms(PF, HS, GS, PURP)) . op _|=_ : Policy ThInterface -> Bool [prec 50] . eq POL |= none = true . eq PDT >> H, PF |= PDT >> (HTH, PS) = PS <= perms(PF, H, groups(HTH), purpose(HTH)) . eq PDT >> H, PF ; POL |= PDT >> (HTH, PS) = PDT >> H, PF |= PDT >> (HTH, PS) . eq POL |= NETH1 ; NETH2 = POL |= NETH1 and POL |= NETH2 . endfm fmod PRIVACY-TYPING-RULES is protecting TYPE-SYSTEM-GAMMA-ENVIRONMENTS . ---protecting TYPE-SYSTEM-DELTA-ENVIRONMENTS . protecting TYPE-SYSTEM-THETA-INTERFACES . protecting PRIVACY-CALCULUS-SYNTAX . vars X Y : Name . var A : NameId . var T : Type . var R : Role . var G : Group . var PURP : Purpose . var COND : Condition . vars P P' : Process . vars NEP1 NEP2 : NeProcess . var S : System . vars NES1 NES2 : NeSystem . var NED : NeDEnvironment . var NETH : NeThInterface . var GAMMA : GEnvironment . op _|-_ : GEnvironment Name ~> Type . op _|-_ : GEnvironment Process ~> DEnvironment [frozen(2)] . op _|-_ : GEnvironment System ~> ThInterface [frozen(2)] . op fail : GEnvironment Name -> [Type] . op fail : GEnvironment Process -> [DEnvironment] [frozen(2)] . op fail : GEnvironment System -> [ThInterface] [frozen(2)] . eq fail(GAMMA, P) + NED = fail(GAMMA, P) . eq G[PURP] + fail(GAMMA, P) = fail(GAMMA, G : PURP [P]) . eq fail(GAMMA, S) ; NETH = fail(GAMMA, S) . eq G + fail(GAMMA, S) = fail(GAMMA, S) . ceq GAMMA . X : T |- P = GAMMA |- P if not X in fn(P) . ceq GAMMA . X : T |- S = GAMMA |- S if not X in fn(S) . eq cond: COND . GAMMA |- P = COND + (GAMMA |- P) [label CondGamma] . ceq GAMMA |- X = var(X) if X : DataValue /\ not X in names(GAMMA) . ceq GAMMA . X : T |- X = T if fg(T) subset groups(GAMMA) [label Name] . eq GAMMA |- 0P = none [label NilP] . ceq GAMMA |- in X (A : T). P = (([shiftup A] GAMMA) . A{0} : T |- P) + Dr(GAMMA |- X) if carrying(GAMMA |- X) = T [label In]. ceq GAMMA |- out X(Y). P = (GAMMA |- P) + Dw(GAMMA |- X) if carrying(GAMMA |- X) = GAMMA |- Y [label Out]. eq GAMMA |- (v A : T) P = ([shiftup A] GAMMA) . A{0} : T |- P [label ResNP] . eq GAMMA |- ! P = GAMMA |- P [label Rep] . ceq GAMMA |- [X == Y] (P ; P') = (GAMMA . cond:((GAMMA |- Y) == Y) |- P ) + (GAMMA . cond:((GAMMA |- Y) =/= Y) |- P') if Y :: DataValue /\ GAMMA |- Y = GAMMA |- X [label CondC] . ceq GAMMA |- [X == Y] (P ; P') = (GAMMA |- P) + (GAMMA |- P') if not Y :: DataValue /\ GAMMA |- Y = GAMMA |- X [label CondV] . eq GAMMA |- NEP1 | NEP2 = (GAMMA |- NEP1) + (GAMMA |- NEP2) [label ParP] . eq GAMMA |- P = fail(GAMMA, P) [owise] . eq GAMMA |- 0S = none [label NilS] . eq GAMMA |- G : PURP [P] = G [PURP] + (GAMMA . group: G |- P) [label ResGP] . eq GAMMA |- R [S] = R + (GAMMA . group: R |- S) [label ResGS] . eq GAMMA |- (v A : T) S = ([shiftup A] GAMMA) . A{0} : T |- S [label ResNS] . eq GAMMA |- NES1 || NES2 = (GAMMA |- NES1) ; (GAMMA |- NES2) [label ParS] . endfm fmod PRIVACY-TYPE-CHECKER is protecting PRIVACY-TYPING-RULES . protecting POLICY-SATISFACTION . var POL : Policy . var GAMMA : GEnvironment . var S : System . op compatible : Policy GEnvironment System -> Bool . eq compatible(POL, GAMMA, S) = POL |= (GAMMA |- S) . eq compatible(POL, GAMMA, S) = false [owise] . endfm