enrich Step with
   predicates 
       . ⇒1 . : domain × domain;
      comment: policy for Credit card details only flow to the Airline after a confirmation;
       
       . ⇒1 . : domains × domains;
       . ⇒2 . : domain × domain;
      comment: policy for Credit card details never flow to the Travel Agency;
       
       . ⇒2 . : domains × domains;
   
   axioms 
      alter-observe-respects-policy :  ⊦ alter(domvar, nam, ag) ∧ observe(domvar0, nam, ag) → domvar ⇒ domvar0;
      used for : theorem;
       
      flightOffers-no-read-up :  ⊦ observe(domvar, Airline-flightOffers, mkAirline(0)) → dom(Airline-flightOffers, mkAirline(0)) ⇒ domvar;
      comment: attribute flightOffers in class Airline has explicit domain User_TravelAgency_Airline.;
      used for : theorem;
       
      flightOffers-no-write-down :  ⊦ alter(domvar, Airline-flightOffers, mkAirline(0)) → domvar ⇒ dom(Airline-flightOffers, mkAirline(0));
      comment: attribute flightOffers in class Airline has explicit domain User_TravelAgency_Airline.;
      used for : theorem;
       
      ccd-no-read-up :  ⊦ observe(domvar, CreditCardCenter-ccd, mkCreditCardCenter(n)) → dom(CreditCardCenter-ccd, mkCreditCardCenter(n)) ⇒ domvar;
      comment: attribute ccd in class CreditCardCenter has explicit domain User.;
      used for : theorem;
       
      ccd-no-write-down :  ⊦ alter(domvar, CreditCardCenter-ccd, mkCreditCardCenter(n)) → domvar ⇒ dom(CreditCardCenter-ccd, mkCreditCardCenter(n));
      comment: attribute ccd in class CreditCardCenter has explicit domain User.;
      used for : theorem;
       
      domains-interference-def :  ⊦ domsvar ⇒1 domsvar0 ↔ (∃ domvar, domvar0. domvar ∈ domsvar ∧ domvar0 ∈ domsvar0 ∧ domvar ⇒1 domvar0);
      User-interference-def :  ⊦ User ⇒1 domvar ↔ domvar = User ∨ domvar = User->User_Airline ∨ domvar = Abort9;
      used for : s, ls;
       
      User_Airline-interference-def :  ⊦ User_Airline ⇒1 domvar ↔ domvar = User_Airline ∨ domvar = User ∨ domvar = HighLow5 ∨ domvar = Abort8;
      used for : s, ls;
       
      User_TravelAgency_Airline-interference-def
      :  ⊦ User_TravelAgency_Airline ⇒1 domvar ↔ domvar = User_TravelAgency_Airline ∨ domvar = User_Airline ∨ domvar = User;
      used for : s, ls;
       
      User-User_Airline-interference-def :  ⊦ User->User_Airline ⇒1 domvar ↔ domvar = User->User_Airline ∨ domvar = User_Airline;
      used for : s, ls;
       
      HighLow5-interference-def :  ⊦ HighLow5 ⇒1 domvar ↔ domvar = HighLow5 ∨ domvar = User_TravelAgency_Airline;
      used for : s, ls;
       
      Abort8-interference-def :  ⊦ Abort8 ⇒1 domvar ↔ domvar = Abort8 ∨ domvar = User_TravelAgency_Airline;
      used for : s, ls;
       
      Abort9-interference-def :  ⊦ Abort9 ⇒1 domvar ↔ domvar = Abort9 ∨ domvar = User_TravelAgency_Airline;
      used for : s, ls;
       
      IFProperty1
      : ⊦ 
        ¬    ∅ ++ dom(CreditCardCenter-ccd, mkCreditCardCenter(m))
          ⇒1    ∅ ++ dom(Mailbox(GetFlightOffers-AirlineCmd), mkAirline(0)) ++ dom(Mailbox(BookFlightOffer-AirlineCmd), mkAirline(0))
             ++ dom(Mailbox(OkPayCommission-AirlineCmd), mkAirline(0));
      comment: Credit card details only flow to the Airline after a confirmation;
      used for : theorem;
       
      domains-interference-def :  ⊦ domsvar ⇒2 domsvar0 ↔ (∃ domvar, domvar0. domvar ∈ domsvar ∧ domvar0 ∈ domsvar0 ∧ domvar ⇒2 domvar0);
      User-interference-def :  ⊦ User ⇒2 domvar ↔ domvar = User ∨ domvar = User->User_Airline ∨ domvar = Abort9 ∨ domvar = User_Airline;
      used for : s, ls;
       
      User_Airline-interference-def
      :  ⊦ User_Airline ⇒2 domvar ↔ domvar = User_Airline ∨ domvar = User ∨ domvar = HighLow5 ∨ domvar = Abort8 ∨ domvar = User->User_Airline;
      used for : s, ls;
       
      User_TravelAgency_Airline-interference-def
      : ⊦ 
        User_TravelAgency_Airline ⇒2 domvar ↔ domvar = User_TravelAgency_Airline ∨ domvar = User_Airline ∨ domvar = User ∨ domvar = User->User_Airline;
      used for : s, ls;
       
      User-User_Airline-interference-def :  ⊦ User->User_Airline ⇒2 domvar ↔ domvar = User->User_Airline ∨ domvar = User_Airline ∨ domvar = User;
      used for : s, ls;
       
      HighLow5-interference-def :  ⊦ HighLow5 ⇒2 domvar ↔ domvar = HighLow5 ∨ domvar = User_TravelAgency_Airline;
      used for : s, ls;
       
      Abort8-interference-def :  ⊦ Abort8 ⇒2 domvar ↔ domvar = Abort8 ∨ domvar = User_TravelAgency_Airline;
      used for : s, ls;
       
      Abort9-interference-def :  ⊦ Abort9 ⇒2 domvar ↔ domvar = Abort9 ∨ domvar = User_TravelAgency_Airline;
      used for : s, ls;
       
      IFProperty2
      : ⊦ 
        ¬    ∅ ++ dom(CreditCardCenter-ccd, mkCreditCardCenter(m))
          ⇒2       ∅ ++ dom(Mailbox(GetFlightOffers-TravelAgencyCmd), mkTravelAgency(0))
                ++ dom(Mailbox(RetFlightOffers-TravelAgencyCmd), mkTravelAgency(0))
             ++ dom(Mailbox(PayCommission-TravelAgencyCmd), mkTravelAgency(0));
      comment: Credit card details never flow to the Travel Agency;
      used for : theorem;
       
      ConfirmIFProperty1
      : s(User-ConfirmedRelease-count(`3'), mkUser(0)) = mkNat(0), s(declassify-count(`declassifyCCD'), mkCreditCardCenter(0)) = mkNat(0), 
        maxOneNotNull(s), s(state(`init'), mkUser(0)) = wrapBoolean2Data(mkBoolean(true))
        ⊦ 
        [ASM#(; s, boolvar)] 
            (  s(User-ConfirmedRelease-count(`3'), mkUser(0)) .nat = s(declassify-count(`declassifyCCD'), mkCreditCardCenter(0)) .nat
             ∨ s(User-ConfirmedRelease-count(`3'), mkUser(0)) .nat = s(declassify-count(`declassifyCCD'), mkCreditCardCenter(0)) .nat + 1);
      comment: Credit card details only flow to the Airline after a confirmation;
      used for : generated;
       
end enrich