% !! THIS FILE IS AUTOMATICALLY GENERATED % !! FROM CRP.c USING THE C PREPROCESSOR. % !! DO NOT EDIT THIS FILE DIRECTLY. % % @verbatim(Specification of the Car Registration Office in D5.1) % @modeler(David von Oheimb, Siemens AG) % @modeler(Marius Minea, IeAT) % @modeler(Gabriel Erzse, IeAT) % @satmc(--mutex=1) % @ofmc(--classic --untyped) % @clatse(--not_hc) specification CarRegistrationProtocol channel_model CCM entity Environment { types decision < message; role < message; info < message; capability < info; symbols % DKAL-like policy predicates and functions: % A piece of information (represented as an element of type info) is % known to an agent without involving communication at the meta level % but possibly at the system level. Typically, this kind of knowledge % is acquired upon reception of a message over the network. knows0 (agent, info): fact; % A piece of information (represented as an element of type info) is % known to an agent possibly involving communication at the meta level. knows (agent, info): fact; % Agents may communicate parts of their knowledge at the meta level to % other principals (this is a different kind of communication with % respect to communication at the system level). It is worth noticing % that the meta level communication is secure and targeted; e.g., % a1->saysTo(a2,x) means that agent a1 says a piece of information x % to agent a2 and the intruder will have no access to x. Notice that % the piece of information x in a1->saysTo(a2,x) is part of the % knowledge of agent a1 that might have been obtained from some other % agent a3. saysTo (agent, agent, info): fact; % Instead, if we write a1->saysTo0(a2,x), then the piece of % information x is part of the "internal" knowledge of agent a1, i.e. % it is not obtained from some other principal but only by some % computation, e.g. reception of a message over the network at the % system level. saysTo0 (agent, agent, info): fact; % The function symbols said and said0 allows one to characterize how % a piece of information has been obtained by an agent. For example, % if an agent a1 saysTo an agent a2 a piece of information x, then a2 % knows that a1 said the piece of information x. said (agent, info): info; % The difference between said and said0 is that the latter reflects % that the piece of information has been acquired by a principal % without resorting to communication at the meta level. said0 (agent, info): info; % The function symbols tdOn and tdOn0 encode trust relationships % between agents concerning some piece of information. % The difference between tdOn and tdOn0 is that the former allows % agents to delegate trust while the latter does not. For example, % the piece of information a tdOn x expresses not only trust in the % agent a about some piece of information x but also a permission for % agent a to delegate the trust about x. tdOn (agent, info): info; tdOn0 (agent, info): info; % Generic policy information. It states that a certain capability % (e.g. hasRole or canStoreDoc) applies to certain agent. The second % parameter is of type message and not agent, because in general some % additional information may be present, like when stating roles for % agents: granted(hasRole, peter.employee.regOffice) nonpublic granted(capability, message) : info; % Possible roles that can be played in registration offices. head, employee: role; % Two capabilities that can be used when assigning rights to agents. nonpublic hasRole : capability; nonpublic canStoreDoc : capability; % Meta level assertions about the position of each agent in the system. % They are used in the meta level Horn clauses. nonpublic isEmployee(agent) : fact; nonpublic isHead(agent) : fact; nonpublic isRegOffice(agent) : fact; % States that a certain employee received from the certification % authority a certificat about the role of a possibly different % employee or head in a certain registration office. nonpublic emplReceivedCert(agent, agent, role, agent) : fact; % States that a head of a registration office granted the right to % store documents into the central repository to a certain employee. nonpublic headGrantedStoreRight(agent, agent) : fact; % Primitive to create a role certificate by the certification % authority, i.e. an employee can either be a (simple) employee or % the head of a car registration office. rolecert(agent, role, agent): message; % The empty form, provided by the central repository to anyone upon % request. nonpublic emptyDoc : message; % Input predicate (for employees): we abstracted away how an employee % decides whether a request is correct or not. nonpublic noninvertible isok(message) : fact; % Operation of filling an empty document by a citizen. nonpublic fillDoc(agent, message) : message; % Flags saying that a request has been refused or accepted. nonpublic refused, accepted: decision; % Messages sent by agents when they invoke services of other agents. requestEmptyDoc : message; nonpublic submitDoc(message) : message; nonpublic docReceived(message) : message; nonpublic requestWork : message; nonpublic provideWork(agent, message, nat) : message; nonpublic workDone(decision, agent, message, nat) : message; nonpublic notifyCitizen(message) : message; nonpublic storeDoc(message) : message; nonpublic authorized : message; % The agents in the system. regOffice : agent; % Registration Office. theCentrRep : agent; % Central Repository. theCA: agent; % Certification Authority. melinda : agent; % Head of the Registration Office. peter : agent; % Employee of the Registration Office, % trusted with storing documents into % the Central Repository. mike : agent; % Citizen. % Facts for signaling completion of steps in the workflow. % They are used for specifying security goals. nonpublic citizenSubmittedDoc(agent, message) : fact; nonpublic citizenReceivedRegNo(agent, message, nat) : fact; nonpublic citizenReceivedDecision(agent, message, nat, decision) : fact; nonpublic regOfficeDispatchedWork(agent, agent) : fact; nonpublic centrRepStoredRequest(message) : fact; macros signedDoc(Actor,Doc) = {Doc}_inv(pk(Actor)); signedRoleCert(CA,Empl,Role,RegOffice) = {rolecert(Empl,Role,RegOffice)}_inv(pk(CA)); A->trusts (B,M) = A->knows(B->tdOn (M)); A->trusts0(B,M) = A->knows(B->tdOn0(M)); clauses % An employee who receives a certificate (about a possibly different % employee/head), asserts this at the meta level. employeeAssertsCertReception(RO, E, E1, Role): E->knows(theCA->said0(granted(hasRole, E1.Role.RO))) :- E->emplReceivedCert(E1, Role, RO); regOfficeAssertsCertReception(RO, E, E1, Role): RO->knows(theCA->said0(granted(hasRole, E1.Role.RO))) :- E->emplReceivedCert(E1, Role, RO); centrRepAssertsCertReception(RO, E, E1, Role): theCentrRep->knows(theCA->said0(granted(hasRole, E1.Role.RO))) :- E->emplReceivedCert(E1, Role, RO); % The head of the car registration office decides that some of her % employees can be trusted to store accepted requests in the central % repository. headGrantsStoreRight(Head, Empl) : Head->knows0(granted(canStoreDoc, Empl)) :- headGrantedStoreRight(Head, Empl); % The head of the car registration office, once he/she has decided to % grant the capability of storing processed requests in the central % repository to some of his/her employees, is willing to share this % information with the respective employees. headSharesStoreRightWithEmpl(Head, Empl) : Head->saysTo0(Empl, granted(canStoreDoc, Empl)) :- Head->knows0(granted(canStoreDoc, Empl)) & isHead(Head) & isEmployee(Empl); % Similarly with the above, the head of the registration office is % willing to share with the central repository any capabilities that % were granted to employees. headSharesStoreRightWithCR(Head, Empl) : Head->saysTo0(theCentrRep, granted(canStoreDoc, Empl)) :- Head->knows0(granted(canStoreDoc, Empl)) & isHead(Head) & isEmployee(Empl); % Anyone trusts the certification authority on the hasRole capability. employeeTrustsCA(E) : E->trusts0(theCA, hasRole) :- isEmployee(E); regOfficeTrustsCA(RO) : RO->trusts0(theCA, hasRole) :- isRegOffice(RO); centrRepTrustsCA : theCentrRep->trusts0(theCA, hasRole); % Anyone trusts the head of a car registration office on the % canStoreDoc capability, once it has checked that there are % certificates proving that he/she is the head of a registration % office and that the subject of his/her certificate is an employee % from the same registration office. anyoneTrustsHead(Anyone, RO, Head): Anyone->trusts0(Head, canStoreDoc) :- Anyone->knows(theCA->said0(granted(hasRole, Head.head.RO))) & isHead(Head) & isRegOffice(RO); % The following Horn clauses characterize (an over-approximation of) % the DKAL language. % Internal knowledge is knowledge knowledge0inf(P,AnyThing): P->knows (AnyThing) :- P->knows0(AnyThing); % An agent knows whatever is said to him and he/she also knows whether % the piece of knowledge being communicated is based on the internal % knowledge of the speaker (says2know0) or not (says2knowinf). says2know0(P,Q,AnyThing): P->knows (Q->said0(AnyThing)) :- Q->saysTo0(P,AnyThing); says2knowinf(P,Q,AnyThing): P->knows (Q->said(AnyThing)) :- Q->saysTo(P,AnyThing); % An agent P knows a policy information granted(C,M) whenever P knows % that another agent Q said that and P knows that the agent Q is % trusted on saying things about capability C. trustapp0(P,Q,C,M): P->knows(granted(C,M)) :- P->trusts0(Q,C) & P->knows(Q->said0(granted(C,M))); trustappinf(P,Q,C,M): P->knows(granted(C,M)) :- P->trusts(Q,C) & P->knows(Q->said(granted(C,M))); %%% % Citizen % % Citizen sends a request to Central Repository for obtaining the empty % form. Then he fills the form, signs it and submits it to the % Registration Office. The Registration Office assigns a unique % registration number to the document and informs the citizen about % this registration number. After the document is processed, the % Registration Office informs the Citizen about the decision, referring % back to the initial registration number. entity Citizen(Actor, RO : agent) { symbols Doc : message; RegNo : nat; Decision : decision; body { % The citizen requests and receives the empty form. Actor *-> theCentrRep : requestEmptyDoc; theCentrRep *-> Actor : ?Doc; channel_goal empty_doc_authentic : theCentrRep *-> Actor : Doc; % The citizen fills the empty form with data, then signs it. Doc := signedDoc(Actor, fillDoc(Actor, Doc)); % The citizen submits the filled and signed form. Actor *->* RO : submitDoc(Doc); citizenSubmittedDoc(Actor, Doc); % The citizen receives the registration number for the submitted doc. RO *->* Actor : docReceived(signedDoc(RO, ?RegNo.Doc)); % Make sure that the received registration number is authentic. channel_goal regno_authentic : RO *-> Actor : RegNo; citizenReceivedRegNo(Actor, Doc, RegNo); % The citizen receives the decision for his request. RO *->* Actor : notifyCitizen( signedDoc(RO, RegNo.?Decision)); channel_goal decision_authentic : RO *-> Actor : Decision; citizenReceivedDecision(Actor, Doc, RegNo, Decision); } goals % S7 (Liveness) % ------------- % A citizen who submitted a document should eventually receive from % the Registration Office a registration number. % ! This goal cannot be validated by the backends. %citizen_eventually_receives_regno : % forall Cit Doc . []( % citizenSubmittedDoc(Cit, Doc) => % exists RegNo . % <>(citizenReceivedRegNo(Cit, Doc, RegNo)) % ); % S3 (Correct workflow sequence) % ------------------------------ % A citizen who receives a registration number for a document, % should have submitted that documment. citizen_receives_regno_only_after_submit : forall Cit Doc RegNo . [](!( citizenReceivedRegNo(Cit, Doc, RegNo) & !citizenSubmittedDoc(Cit, Doc) )); % S7 (Liveness) % ------------- % A citizen who received a registration number from the Registration % Office should eventually receive a decision about his submitted % document. % ! This goal cannot be validated by the backends. %citizen_eventually_receives_decision : % forall Cit Doc RegNo . []( % citizenReceivedRegNo(Cit, Doc, RegNo) => % exists Decision . % <>(citizenReceivedDecision(Cit, Doc, RegNo, Decision)) % ); % S3 (Correct workflow sequence) % ------------------------------ % A citizen who receives a decision should have received a % registration number before. citizen_receives_decision_only_after_regno : forall Cit Doc RegNo Decision . [](!( citizenReceivedDecision(Cit, Doc, RegNo, Decision) & !citizenReceivedRegNo(Cit, Doc, RegNo) )); % S2 (Proper logging of data) % --------------------------- % If a citizen receives a positive answer, the request of the % citizen was properly stored in the central repository. % ! This goal cannot be validated by the backends. %accepted_requests_are_properly_stored : % forall Cit Doc RegNo . []( % citizenReceivedDecision(Cit, Doc, RegNo, accepted) => % exists Empl . centrRepStoredRequest(signedDoc(Empl,Doc)) % ); % S4 (Privacy of data) % -------------------- % A request submitted by a citizen is never learned by the intruder. submitted_requests_are_secret : forall Cit Doc . [](!( citizenSubmittedDoc(Cit, Doc) & iknows(Doc) )); % S4 (Privacy of data) % -------------------- % A registration number assigned by a registration office to a % request is never learned by the intruder. assigned_regnos_are_secret : forall Cit Doc RegNo . [](!( citizenReceivedRegNo(Cit, Doc, RegNo) & iknows(RegNo) )); % S4 (Privacy of data) % -------------------- % A decision sent by a registration office to a citizen is never % learned by the intruder. taken_decisions_are_secret : forall Cit Doc RegNo Decision . [](!( citizenReceivedDecision(Cit, Doc, RegNo, Decision) & iknows(Decision) )); } %%% % Certification Authority % % It has the role of distributing certificates to employees of % Registration Offices. Certificates are distributed over confidential % channels, because in general the internal organization of Registration % Offices should be protected. % The Certification Authority receives two sets: one of Head employees % and one with regular employees. Each member of the two sets will % receive an appropriate certificate. entity CA(Actor: agent, Heads, Regulars : (agent,agent) set) { symbols Empl, RO : agent; body { % Each Head employee receives a certificate. while (Heads->contains((?Empl,?RO))) { Heads->remove((Empl,RO)); Actor *->* Empl : signedRoleCert(Actor, Empl, head, RO); } % Each Regular employee receives a certificate. while (Regulars->contains((?Empl,?RO))) { Regulars->remove((Empl,RO)); Actor *->* Empl : signedRoleCert(Actor, Empl, employee, RO); } } goals % S4 (Privacy of data) % -------------------- % The intruder never learns any policy information about roles. roles_are_secret : forall M . [](!( iknows(granted(hasRole, M)) )); } %%% % Registration Office Head % % The role of the Head is to distribute certificates to trusted % employees, so that they can store documents in the central repository. entity Head(Actor, RO: agent, Trusted: agent set) { symbols Empl : agent; body { % The Head does not do anything until he/she receives the needed % certificate from the CA. theCA *->* Actor : signedRoleCert(theCA, Actor, head, RO); % The Head sends its own certificate to all trusted employees, and % also grants them rights to store documents in the central % repository. while (Trusted->contains(?Empl)) { Trusted->remove(Empl); headGrantedStoreRight(Actor, Empl); Actor *->* Empl : signedRoleCert(theCA, Actor, head, RO); } } goals % S4 (Privacy of data) % -------------------- % The intruder never learns any policy information about who can % store docs in the central repository. storage_capabilities_are_secret : forall A . [](!( iknows(granted(canStoreDoc, A)) )); } %%% % Regular Employee of Registration Office % % Continuously asks for work from the Registration Office and solves % car registration requests sent by the Registration Office. Also % accepts certificates about employees (himself and the head of the % registration office) and makes the knowledge derived from the % certificate available at the meta level. entity Employee(Actor, RO, Head : agent) { symbols RegNo : nat; Cit : agent; Doc : message; SignedReq: message; body { % The employee does not start any work until he receives two % certificates: one that states his role as employee, and one that % states the role of the registration office head. theCA *->* Actor : signedRoleCert(theCA, Actor, employee, RO); Actor->emplReceivedCert(Actor, employee, RO); Head *->* Actor : signedRoleCert(theCA, Head, head, RO); Actor->emplReceivedCert(Head, head, RO); while(true) { % The employee asks for work. Actor *->* RO : requestWork; select { % If the registration office sends back a signed registration % request, and the request meets certain criteria (abstracted % away in this model), and the employee has appropriate access % rights, will send the document to the central repository and % then he will accept it. on (RO *->* Actor : provideWork(?Cit, ?SignedReq, ?RegNo) & ?SignedReq = signedDoc(?Cit, ?Doc) & isok(?Doc) & Actor->knows(granted(canStoreDoc, Actor))) : { Actor *->* theCentrRep : storeDoc(signedDoc(Actor, SignedReq)); % When the central repository authorizes the request, notify % the registration office, which in turn will notify the % citizen. theCentrRep *->* Actor : authorized; Actor *->* RO : workDone(accepted, Cit, SignedReq, RegNo); } % If the document is not valid, then the employee will reject % it. He will notify the registration office, which in turn % will notify the citizen. on (RO *->* Actor : provideWork(?Cit, ?SignedReq, ?RegNo) & ?SignedReq = signedDoc(?, ?Doc) & !isok(?Doc)) : { Actor *->* RO : workDone(refused, Cit, SignedReq, RegNo); } } % end select reg office response } % end while(true) } % end body } %%% % Car Registration Office % % Holds a local database with car registration requests. The requests % are split into three categories: those waiting to be processed, those % that were dispatched to employees and are being processed, and those % that were processed. % Registration requests are received from citizens and stored into the % local database. Employees of the registration office query for pending % registration requests. Solved requests will be stored by authorized % employees directly into the central repository. entity RegistrationOffice(Actor: agent) { symbols Empl, Cit : agent; SignedReq : message; Decision : decision; RegNo : nat; PendingDB, InProgressDB, ProcessedDB : (agent, message, nat) set; body { % Initially there is no request in the local database. PendingDB := {}; InProgressDB := {}; ProcessedDB := {}; % The registration office runs indefinitely. while(true) { select { % Anyone can submit a filled and signed car registration request. % A unique registration number is assigned to the request. The % request, together with the registration number and the % citizen who sent the request, are stored in the local database % for later processing. The registration number is sent back to % the citizen. on (?Cit *->* Actor : submitDoc(?SignedReq) & !PendingDB->contains((?Cit, ?SignedReq, ?)) & !InProgressDB->contains((?Cit, ?SignedReq, ?)) & !ProcessedDB->contains((?Cit, ?SignedReq, ?))) : { RegNo := fresh(); PendingDB->add((Cit, SignedReq, RegNo)); Actor *->* Cit : docReceived(signedDoc(Actor, RegNo.SignedReq)); % The registration number that makes it to the citizen is the % authentic one. channel_goal regno_authentic : Actor *-> Cit : RegNo; } % Employees can request a document for processing. The request % is accepted only if the sender is indeed an employee of the % registration office and if there is a pending registration % request to be processed. Such a pending registration request % will be sent to the employee. on (?Empl *->* Actor : requestWork & Actor->knows(granted(hasRole, ?Empl.employee.Actor)) & PendingDB->contains((?Cit, ?SignedReq, ?RegNo))) : { PendingDB->remove((Cit,SignedReq,RegNo)); InProgressDB->add((Cit,SignedReq,RegNo)); Actor *->* Empl : provideWork(Cit, SignedReq, RegNo); regOfficeDispatchedWork(Actor, Empl); } % Employees can instruct the registration office to notify % customers about decisions taken. Again, the sender of such a % request must be indeed an employee of the registration office. on (?Empl *->* Actor : workDone(?Decision, ?Cit, ?SignedReq, ?RegNo) & Actor->knows(granted(hasRole, ?Empl.employee.Actor)) & InProgressDB->contains((?Cit,?SignedReq,?RegNo))) : { InProgressDB->remove((Cit,SignedReq, RegNo)); ProcessedDB->add((Cit, SignedReq, RegNo)); Actor *->* Cit : notifyCitizen(signedDoc(Actor, RegNo.Decision)); % The decision that makes it to the citizen is the authentic one. channel_goal decision_authentic : Actor *-> Cit : Decision; } } % end select } % end while } % end body goals % S6 (Proper authorization for task distribution) work_sent_only_to_legitimate_employees : forall RO Empl . [](!( regOfficeDispatchedWork(RO, Empl) & !knows(RO, granted(hasRole, Empl.employee.RO)) )); } %%% % Central Repository % % Has the role of providing empty registration forms to anyone and of % storing documents sent by authorized employees of registration offices. entity CentralRepository(Actor: agent) { symbols CentrDB : message set; Requestor : agent; DoubleSignedReq : message; body { % Initially there is nothing stored in the central database. CentrDB := {}; % The central repository runs indefinitely. while(true) { select { % Anybody can obtain the empty form. on (?Requestor *-> Actor : requestEmptyDoc) : { Actor *-> Requestor : emptyDoc; % Make sure the authentic empty form makes it to the requestor. channel_goal empty_doc_authentic : Actor *-> Requestor : emptyDoc; } % Upon reception of a request to store a document in the % database, check whether the employee asking for this to be % done has the right to do this. Also check that the document % is double signed. If so, store the request in the database. on (?Requestor *->* Actor : storeDoc(?DoubleSignedReq) & ?DoubleSignedReq = signedDoc(?Requestor, signedDoc(?,?)) & Actor->knows(granted(canStoreDoc, ?Requestor)) & !CentrDB->contains(?DoubleSignedReq)) : { CentrDB->add(DoubleSignedReq); centrRepStoredRequest(DoubleSignedReq); Actor *->* Requestor : authorized; } } } } goals % S1 (Data Consistency) % --------------------- % All car registration requests stored by the central repository % are double signed. % ! This goal cannot be validated by the backends. %documents_stored_in_cr_are_double_signed : % forall DoubleSignedReq . []( % centrRepStoredRequest(DoubleSignedReq) => % exists Empl Cit Doc . % DoubleSignedReq = signedDoc(Empl, signedDoc(Cit, Doc)) % ); % S5 (Proper authorization for changing data) % ------------------------------------------- only_authorized_employees_store_docs_in_cr : forall Empl SignedReq . [](!( centrRepStoredRequest(signedDoc(Empl, SignedReq)) & !theCentrRep->knows(granted(canStoreDoc, Empl)) )); } % Initialization of the overall system. body { % We abstract away the criteria for the correctness of registration % requests. We simply state that the car registration request filled % by Mike is correct (while requests filled by others are not corect). isok(fillDoc(mike,emptyDoc)); % The certification authority receives two sets: one with the Head % employees and another one with regular employees. new CA(theCA, {(melinda,regOffice)}, {(peter,regOffice)}); % The central repository. new CentralRepository(theCentrRep); % The registration office. isRegOffice(regOffice); new RegistrationOffice(regOffice); % Melinda, the Head employee of the registration office. She receives % two sets of employees, one with trusted employees, and another one % with untrusted employees. isHead(melinda); new Head(melinda, regOffice, {peter}); % Peter, a trusted employee of the registration office. isEmployee(peter); new Employee(peter, regOffice, melinda); % Mike, a citizen who submits a car registration request. new Citizen(mike, regOffice); } }