%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Digital Contract Signing %% - orchestration problem %% - Goal-style input %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Modelers: MEKKI Mohamed Anis, %% AVANESOV Tigran %% Institution: INRIA %% Date: 2008 -- 2010 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Scenario Info %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Refer to DCS Case study proposed by OpenTrust. %% Orchestration problem: construct Security Server. %% In the role of the Client: Business Portal. %% %% %% Available services: %% TimeStamper, put time stamps %% PKI, Public Key Infrastructure. %% Possesses and return information about CRL (certificate revocation list) %% %% Archiver, Third party storage (archiving) service %% AssertionProvider, internal facility for the Security Server %% %% Orchestration functionality: %% OrchestrationGoal, a partial specification (only communication with Client) of the Security Server. %% The rest is to be found. %% %% %% %% To see the MSC of the expected communications, %% use http://www.websequencediagrams.com/ %% and copy-paste the following text %% (previosly remove trailing '%%%'): %% %% ------------ BEGIN MSC ------------- %%% participant BP %%% participant SS %%% participant TS %%% participant PKI %%% participant ARC %%% %%% BP->SS: CreateRecordRequest %%% SS->BP: CreateRecordResponse %%% BP->SS: PrepareSignatureRequest[1] %%% SS->BP: PrepareSignatureResponse[1] %%% BP->SS: AddSignatureRequest[1] %%% SS->SS: CheckSignature[1] %%% SS->BP: AddSignatureResponse[1] %%% BP->SS: TimeStampRequest[1] %%% SS->TS: TS:TimeStampRequest[1] %%% TS->SS: TS:TimeStampResponse[1] %%% SS->SS: CheckTimeStamp[1] %%% SS->BP: TimeStampResponse[1] %%% BP->SS: CheckCertificateRequest[1] %%% SS->PKI: PKI:CheckCertificateRequest[1] %%% PKI->SS: PKI:CheckCertificateResponse[1] %%% SS->SS: CheckCertificate[1] %%% SS->BP: CheckCertificateResponse[1] %%% BP->SS: PrepareSignatureRequest[2] %%% SS->BP: PrepareSignatureResponse[2] %%% BP->SS: AddSignatureRequest[2] %%% SS->SS: CheckSignature[2] %%% SS->BP: AddSignatureResponse[2] %%% BP->SS: TimeStampRequest[2] %%% SS->TS: TS:TimeStampRequest[2] %%% TS->SS: TS:TimeStampResponse[2] %%% SS->SS: CheckTimeStamp[2] %%% SS->BP: TimeStampResponse[2] %%% BP->SS: CheckCertificateRequest[2] %%% SS->PKI: PKI:CheckCertificateRequest[2] %%% PKI->SS: PKI:CheckCertificateResponse[2] %%% SS->SS: CheckCertificate[2] %%% SS->BP: CheckCertificateResponse[2] %%% BP->SS: ArchiveRecordRequest %%% SS->ARC: ARC:ArchiveRequest %%% ARC->SS: ARC:ArchiveResponse %%% SS->BP: ArchiveRecordResponse %%% %% ------------ END MSC ------------- %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% section signature: state_OrchestrationGoal: agent * nat * nat * public_key * public_key * agent * agent * agent * agent * agent * public_key * public_key * symmetric_key * symmetric_key * text * text * hash_func * bool * bool * protocol_id * protocol_id * protocol_id * protocol_id * text * text * agent * public_key * agent * public_key -> fact % state_OrchestrationClient: agent * nat * nat * agent * agent * agent * agent * agent * public_key * public_key * symmetric_key * symmetric_key * public_key * public_key * hash_func -> fact state_assertionsProvider: agent * nat * nat * public_key * agent * agent * public_key * public_key * hash_func * message * agent * public_key * message * message * agent * public_key * bool -> fact state_arc: agent * nat * nat * public_key * agent * agent * agent * symmetric_key * public_key * public_key * hash_func * set(message) * message * message * agent * public_key * agent * public_key * message * message * message * message * message * message -> fact state_pki: agent * nat * nat * public_key * hash_func * set(pair(agent, public_key)) * agent * public_key -> fact state_timestamper: agent * nat * nat * public_key * hash_func * text * message -> fact keepsecret: message -> fact section types: % tokens used in assertions % "Signature is OK" sigOK : protocol_id SigOK : protocol_id % "Message was timestamped" tsOK : protocol_id TsOK : protocol_id % "Certificate is valid, i.e. not revoked" certOK: protocol_id CertOK: protocol_id % "A contract was archived" arcOK : protocol_id ArcOK : protocol_id % Initial dummy values of variables dummy_set : set(message) dummy_nonce : text dummy_msg : message dummy_pk : public_key dummy_bool : bool dummy_agent : agent Dummy : protocol_id % A storage of the Archiver Archive : set(message) % its init value Dummy_Archive : set(message) % A key shared between Security Server (SS) and Archiver (Arc) KSSARC : symmetric_key Kssarc : symmetric_key kssarc : symmetric_key % Orchestration goal agent OrchestrationGoal : agent % A key shared between Business Portal and SS Kbpss : symmetric_key kbpss : symmetric_key % PKI public key KPKI : public_key Kpki : public_key kpki : public_key % TS public key KTS : public_key Kts : public_key kts : public_key %Text of a contract to sign Contract : text Dummy_Contract : text dummy_contract : text % a session ID for the scenario: % this value helps to identify a session % (if there were several). % It appears almost in all messages Id : text Dummy_Id : text dummy_id : text % Signature policies for the 1st and the 2nd signers signaturePolicy1 : text SignaturePolicy1 : text signaturePolicy2 : text SignaturePolicy2 : text % Hash function Hash : hash_func md5 : hash_func Md5 : hash_func % Session ID % (needed if one role (set of transitions) used several times) SID : nat % Current time (for the Timestamper) Dummy_Time : text Time : text % For AP (assertion provider) % input for checking signature % ...Msg --- message that must be signed Dummy_CheckSigMsg : message CheckSigMsg : message % with public key: Dummy_CheckSigKey : public_key CheckSigKey : public_key % (this pubkey is) of agent: CheckSigAgent : agent Dummy_CheckSigAgent : agent % For AP (assertion provider) % input for checking whether % certificate is not revoked % Agent CheckCertAgent : agent Dummy_CheckCertAgent : agent % and his Public Key CheckCertKey : public_key Dummy_CheckCertKey : public_key % variable for the result % not used in this spec. CheckCertRes : bool Dummy_CheckCertRes : bool % no comments true : bool True : bool false : bool False : bool % agent playing a client sscl : agent Sscl : agent % orchgoal : agent % agent playing TimeStamper ts : agent TS : agent Ts : agent % agent playing Security Server ss : agent SS : agent % agent playing Business Portal % bp : agent % agent playing Assertion Provider ap : agent AP : agent Ap : agent % Public key of AP KAP : public_key kap : public_key Kap : public_key % agent playing Archiver arc : agent ARC : agent Arc : agent % ARC's public key KARC : public_key karc : public_key Karc : public_key % agent playing PKI pki : agent Pki : agent PKI : agent % intruder/composer... i : agent % The first signer signer1 : agent Signer1 : agent Dummy_Signer1 : agent dummy_signer1 : agent % His public key pubKey1 : public_key PubKey1 : public_key Dummy_PubKey1 : public_key dummy_pubKey1 : public_key %The second signer signer2 : agent Signer2 : agent Dummy_Signer2 : agent dummy_signer2 : agent % His public key pubKey2 : public_key PubKey2 : public_key Dummy_PubKey2 : public_key dummy_pubKey2 : public_key % some user and his pulic key user1 : agent key1 : public_key % another user and his pulic key user2 : agent key2 : public_key % Certificate revocation lists % (user1/user2 will be there inside...) crl : set(pair(agent, public_key)) CRL : set(pair(agent, public_key)) % Variables for Archiver's input: % two signers and theirs public keys InSigner2 : agent InSigner1 : agent InPubKeySigner2 : public_key InPubKeySigner1 : public_key Dummy_InPubKeySigner2 : public_key Dummy_InPubKeySigner1 : public_key Dummy_InSigner2 : agent Dummy_InSigner1 : agent % Archiver's Input: contract Dummy_InContract : message InContract : message % Archiver's input: policies % Signature policies InSigPolicy2 : message InSigPolicy1 : message Dummy_InSigPolicy2 : message Dummy_InSigPolicy1 : message % Archiver's input: time % Time of timestamps InTime2 : message InTime1 : message Dummy_InTime2 : message Dummy_InTime1 : message % Archiver's input: revokation status % Was the certificate revoked? % (normally, no) Dummy_InRevoked2 : message Dummy_InRevoked1 : message InRevoked2 : message InRevoked1 : message % Archiver's input: revokation status % Archiver's call(invokation) identifier InID : message Dummy_InID : message % A message to be timestamped % in the input of TimeStamper % and in the Assertion Provider % for generating tsOK MsgToTimestamp : message Dummy_MsgToTimestamp : message CheckTime : message Dummy_CheckTime : message section inits: initial_state init1:= % Initial knowledge for the intruder iknows(i). iknows(pair(arcOK, pair(certOK, pair(sigOK, pair(tsOK, pair(true, false)))))). iknows(pair(karc,pair(kap,pair(kpki,pair(kts,md5))))). % Initial state of the Goal + its knowledge state_OrchestrationGoal(ss,1,1,kap,karc,sscl,pki,ts,arc,ap,kpki,kts,kssarc,kbpss,signaturePolicy1,signaturePolicy2,md5,true,false,arcOK,certOK,sigOK,tsOK,dummy_id,dummy_contract,dummy_signer1,dummy_pubKey1,dummy_signer2,dummy_pubKey2). % the first instances of the TimeStamper, PKI and AP state_assertionsProvider(ap, 6, 1, kap, pki, ts, kpki, kts, md5, dummy_msg, dummy_agent, dummy_pk, dummy_msg, dummy_msg, dummy_agent, dummy_pk, dummy_bool). state_pki(pki, 4, 1, kpki, md5, crl, dummy_agent, dummy_pk). state_timestamper(ts, 3, 1, kts, md5, dummy_nonce, dummy_msg). % A second instance of AP state_assertionsProvider(ap, 9, 1, kap, pki, ts, kpki, kts, md5, dummy_msg, dummy_agent, dummy_pk, dummy_msg, dummy_msg, dummy_agent, dummy_pk, dummy_bool). % an Archiver state_arc(arc, 5, 1, karc, ss, pki, ts, kssarc, kpki, kts, md5, dummy_set, dummy_msg, dummy_msg, dummy_agent, dummy_pk, dummy_agent, dummy_pk, dummy_msg, dummy_msg, dummy_msg, dummy_msg, dummy_msg, dummy_msg). % the second instances of the TimeStamper and PKI state_pki(pki, 8, 1, kpki, md5, crl, dummy_agent, dummy_pk). state_timestamper(ts, 7, 1, kts, md5, dummy_nonce, dummy_msg). % Init of CRL contains(pair(user1, key1), crl). contains(pair(user2, key2), crl) section hornClauses: section rules: % TS: putting timestamp step step_0(TS, KTS, Hash, Dummy_Time, Dummy_MsgToTimestamp, SID, Time, MsgToTimestamp):= state_timestamper(TS, SID, 1, KTS, Hash, Dummy_Time, Dummy_MsgToTimestamp). iknows(MsgToTimestamp) =[exists Time]=> state_timestamper(TS, SID, 1, KTS, Hash, Time, MsgToTimestamp). iknows(pair(MsgToTimestamp, pair(Time, crypt(inv(KTS), pair(apply(Hash, MsgToTimestamp), Time))))) % PKI: check whether a certificate is in CRL % case if it is not in CRL step step_1(PKI, KPKI, Hash, CRL, Dummy_CheckCertAgent, Dummy_CheckCertKey, SID, CheckCertAgent, CheckCertKey):= state_pki(PKI, SID, 1, KPKI, Hash, CRL, Dummy_CheckCertAgent, Dummy_CheckCertKey). iknows(pair(CheckCertAgent, CheckCertKey)). not(contains(pair(CheckCertAgent, CheckCertKey), CRL)) => state_pki(PKI, SID, 1, KPKI, Hash, CRL, CheckCertAgent, CheckCertKey). iknows(pair(CheckCertAgent, pair(CheckCertKey, pair(false, crypt(inv(KPKI), pair(CheckCertAgent, pair(CheckCertKey, false))))))) % case if it is in CRL step step_2(PKI, KPKI, Hash, CRL, Dummy_CheckCertAgent, Dummy_CheckCertKey, SID, CheckCertAgent, CheckCertKey):= state_pki(PKI, SID, 1, KPKI, Hash, CRL, Dummy_CheckCertAgent, Dummy_CheckCertKey). iknows(pair(CheckCertAgent, CheckCertKey)). contains(pair(CheckCertAgent, CheckCertKey), CRL) => state_pki(PKI, SID, 1, KPKI, Hash, CRL, CheckCertAgent, CheckCertKey). iknows(pair(CheckCertAgent, pair(CheckCertKey, pair(true, crypt(inv(KPKI), pair(CheckCertAgent, pair(CheckCertKey, true))))))). contains(pair(CheckCertAgent, CheckCertKey), CRL) % An Archiver: receives a huge mssage, % store it in his database Archive % generates an assertion step step_3(ARC, KARC, SS, PKI, TS, KSSARC, KPKI, KTS, Hash, Dummy_Archive, Dummy_InID, Dummy_InContract, Dummy_InSigner1, Dummy_InPubKeySigner1, Dummy_InSigner2, Dummy_InPubKeySigner2, Dummy_InSigPolicy1, Dummy_InSigPolicy2, Dummy_InRevoked1, Dummy_InRevoked2, Dummy_InTime1, Dummy_InTime2, SID, InID, InContract, InSigner1, InPubKeySigner1, InSigner2, InPubKeySigner2, InSigPolicy1, InSigPolicy2, InRevoked1, InRevoked2, InTime1, InTime2):= state_arc(ARC, SID, 1, KARC, SS, PKI, TS, KSSARC, KPKI, KTS, Hash, Dummy_Archive, Dummy_InID, Dummy_InContract, Dummy_InSigner1, Dummy_InPubKeySigner1, Dummy_InSigner2, Dummy_InPubKeySigner2, Dummy_InSigPolicy1, Dummy_InSigPolicy2, Dummy_InRevoked1, Dummy_InRevoked2, Dummy_InTime1, Dummy_InTime2). iknows(scrypt(KSSARC, pair(InID, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigner2, pair(InPubKeySigner2, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigPolicy1, pair(InContract, pair(InSigner2, pair(InPubKeySigner2, pair(InSigPolicy2, pair(InSigner1, pair(InPubKeySigner1, pair(InRevoked1, pair(InSigner2, pair(InPubKeySigner2, pair(InRevoked2, pair(crypt(inv(InPubKeySigner1), pair(InContract, pair(InSigner1, pair(InPubKeySigner1, InSigPolicy1)))), pair(InTime1, pair(crypt(inv(KTS), pair(apply(Hash, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigPolicy1, crypt(inv(InPubKeySigner1), pair(InContract, pair(InSigner1, pair(InPubKeySigner1, InSigPolicy1))))))))), InTime1)), pair(crypt(inv(InPubKeySigner2), pair(InContract, pair(InSigner2, pair(InPubKeySigner2, InSigPolicy2)))), pair(InTime2, pair(crypt(inv(KTS), pair(apply(Hash, pair(InContract, pair(InSigner2, pair(InPubKeySigner2, pair(InSigPolicy2, crypt(inv(InPubKeySigner2), pair(InContract, pair(InSigner2, pair(InPubKeySigner2, InSigPolicy2))))))))), InTime2)), pair(crypt(inv(KPKI), pair(InSigner1, pair(InPubKeySigner1, InRevoked1))), crypt(inv(KPKI), pair(InSigner2, pair(InPubKeySigner2, InRevoked2)))))))))))))))))))))))))))))))) => state_arc(ARC, SID, 1, KARC, SS, PKI, TS, KSSARC, KPKI, KTS, Hash, Dummy_Archive, InID, InContract, InSigner1, InPubKeySigner1, InSigner2, InPubKeySigner2, InSigPolicy1, InSigPolicy2, InRevoked1, InRevoked2, InTime1, InTime2). iknows(scrypt(KSSARC, pair( InID, % Contract is archieved crypt(inv(KARC), pair(arcOK, pair( apply(Hash, InContract), pair(pair(InSigner1, InPubKeySigner1), pair(InSigner2, InPubKeySigner2)))))))). contains(pair(InID, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigner2, pair(InPubKeySigner2, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigPolicy1, pair(InContract, pair(InSigner2, pair(InPubKeySigner2, pair(InSigPolicy2, pair(InSigner1, pair(InPubKeySigner1, pair(InRevoked1, pair(InSigner2, pair(InPubKeySigner2, pair(InRevoked2, pair(crypt(inv(InPubKeySigner1), pair(InContract, pair(InSigner1, pair(InPubKeySigner1, InSigPolicy1)))), pair(InTime1, pair(crypt(inv(KTS), pair(apply(Hash, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigPolicy1, crypt(inv(InPubKeySigner1), pair(InContract, pair(InSigner1, pair(InPubKeySigner1, InSigPolicy1))))))))), InTime1)), pair(crypt(inv(InPubKeySigner2), pair(InContract, pair(InSigner2, pair(InPubKeySigner2, InSigPolicy2)))), pair(InTime2, pair(crypt(inv(KTS), pair(apply(Hash, pair(InContract, pair(InSigner2, pair(InPubKeySigner2, pair(InSigPolicy2, crypt(inv(InPubKeySigner2), pair(InContract, pair(InSigner2, pair(InPubKeySigner2, InSigPolicy2))))))))), InTime2)), pair(crypt(inv(KPKI), pair(InSigner1, pair(InPubKeySigner1, InRevoked1))), crypt(inv(KPKI), pair(InSigner2, pair(InPubKeySigner2, InRevoked2)))))))))))))))))))))))))))))), Dummy_Archive). keepsecret(pair(InID, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigner2, pair(InPubKeySigner2, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigPolicy1, pair(InContract, pair(InSigner2, pair(InPubKeySigner2, pair(InSigPolicy2, pair(InSigner1, pair(InPubKeySigner1, pair(InRevoked1, pair(InSigner2, pair(InPubKeySigner2, pair(InRevoked2, pair(crypt(inv(InPubKeySigner1), pair(InContract, pair(InSigner1, pair(InPubKeySigner1, InSigPolicy1)))), pair(InTime1, pair(crypt(inv(KTS), pair(apply(Hash, pair(InContract, pair(InSigner1, pair(InPubKeySigner1, pair(InSigPolicy1, crypt(inv(InPubKeySigner1), pair(InContract, pair(InSigner1, pair(InPubKeySigner1, InSigPolicy1))))))))), InTime1)), pair(crypt(inv(InPubKeySigner2), pair(InContract, pair(InSigner2, pair(InPubKeySigner2, InSigPolicy2)))), pair(InTime2, pair(crypt(inv(KTS), pair(apply(Hash, pair(InContract, pair(InSigner2, pair(InPubKeySigner2, pair(InSigPolicy2, crypt(inv(InPubKeySigner2), pair(InContract, pair(InSigner2, pair(InPubKeySigner2, InSigPolicy2))))))))), InTime2)), pair(crypt(inv(KPKI), pair(InSigner1, pair(InPubKeySigner1, InRevoked1))), crypt(inv(KPKI), pair(InSigner2, pair(InPubKeySigner2, InRevoked2))))))))))))))))))))))))))))))) % AP: checks signature step step_4(AP, KAP, PKI, TS, KPKI, KTS, Hash, Dummy_CheckSigMsg, Dummy_CheckSigAgent, Dummy_CheckSigKey, MsgToTimestamp, CheckTime, CheckCertAgent, CheckCertKey, CheckCertRes, SID, CheckSigMsg, CheckSigAgent, CheckSigKey):= state_assertionsProvider(AP, SID, 1, KAP, PKI, TS, KPKI, KTS, Hash, Dummy_CheckSigMsg, Dummy_CheckSigAgent, Dummy_CheckSigKey, MsgToTimestamp, CheckTime, CheckCertAgent, CheckCertKey, CheckCertRes). iknows(pair(CheckSigMsg, pair(CheckSigAgent, pair(CheckSigKey, crypt(inv(CheckSigKey), CheckSigMsg))))) => state_assertionsProvider(AP, SID, 1, KAP, PKI, TS, KPKI, KTS, Hash, CheckSigMsg, CheckSigAgent, CheckSigKey, MsgToTimestamp, CheckTime, CheckCertAgent, CheckCertKey, CheckCertRes). iknows(pair(CheckSigMsg, % generate an assertion that message CheckSigMsg was signed well crypt(inv(KAP), pair(sigOK, pair(CheckSigMsg, pair(CheckSigAgent, CheckSigKey)))))) % AP: checks timestamp step step_5(AP, PKI, KAP, TS, KPKI, KTS, Hash, CheckSigMsg, CheckSigAgent, CheckSigKey, Dummy_MsgToTimestamp, Dummy_CheckTime, CheckCertAgent, CheckCertKey, CheckCertRes, SID, MsgToTimestamp, CheckTime):= state_assertionsProvider(AP, SID, 1, KAP, PKI, TS, KPKI, KTS, Hash, CheckSigMsg, CheckSigAgent, CheckSigKey, Dummy_MsgToTimestamp, Dummy_CheckTime, CheckCertAgent, CheckCertKey, CheckCertRes). iknows(pair(MsgToTimestamp, pair(CheckTime, crypt(inv(KTS), pair(apply(Hash, MsgToTimestamp), CheckTime))))) => state_assertionsProvider(AP, SID, 1, KAP, PKI, TS, KPKI, KTS, Hash, CheckSigMsg, CheckSigAgent, CheckSigKey, MsgToTimestamp, CheckTime, CheckCertAgent, CheckCertKey, CheckCertRes). iknows(pair(MsgToTimestamp, % message was timestamped crypt(inv(KAP),pair(tsOK,MsgToTimestamp)))) % AP: checks certificate step step_6(AP, PKI, KAP, TS, KPKI, KTS, Hash, CheckSigMsg, CheckSigAgent, CheckSigKey, MsgToTimestamp, CheckTime, Dummy_CheckCertAgent, Dummy_CheckCertKey, Dummy_CheckCertRes, SID, CheckCertAgent, CheckCertKey):= state_assertionsProvider(AP, SID, 1, KAP, PKI, TS, KPKI, KTS, Hash, CheckSigMsg, CheckSigAgent, CheckSigKey, MsgToTimestamp, CheckTime, Dummy_CheckCertAgent, Dummy_CheckCertKey, Dummy_CheckCertRes). iknows(pair(CheckCertAgent, pair(CheckCertKey, pair(false, crypt(inv(KPKI), pair(CheckCertAgent, pair(CheckCertKey, false))))))) => state_assertionsProvider(AP, SID, 1, KAP, PKI, TS, KPKI, KTS, Hash, CheckSigMsg, CheckSigAgent, CheckSigKey, MsgToTimestamp, CheckTime, CheckCertAgent, CheckCertKey, false). iknows(pair( pair(CheckCertAgent, pair(CheckCertKey, false )), % certificate is OK crypt(inv(KAP),pair(certOK, pair(CheckCertAgent, CheckCertKey))))) % The Goal: step step_OG_1(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Dummy_Id,Id,Dummy_Contract,Contract,Dummy_Signer1,Signer1,Dummy_PubKey1,PubKey1,Dummy_Signer2,Signer2,Dummy_PubKey2,PubKey2,Dummy_Time_n1,Dummy_Time_n21,Dummy_InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,1,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Dummy_Id,Dummy_Contract,Dummy_Signer1,Dummy_PubKey1,Dummy_Signer2,Dummy_PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Contract,pair(Signer1,pair(PubKey1,pair(Signer2,PubKey2))))))) => state_OrchestrationGoal(OrchestrationGoal,SID,2,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,Id)) step step_OG_2(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Dummy_Time_n1,Dummy_Time_n21,Dummy_InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,2,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer1,PubKey1)))) => state_OrchestrationGoal(OrchestrationGoal,SID,3,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer1,pair(PubKey1,SignaturePolicy1))))) step step_OG_3(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Dummy_Time_n1,Dummy_Time_n21,Dummy_InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,3,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Contract,pair(Signer1,pair(PubKey1,pair(SignaturePolicy1,crypt(inv(PubKey1),pair(Contract,pair(Signer1,pair(PubKey1,SignaturePolicy1))))))))))) => state_OrchestrationGoal(OrchestrationGoal,SID,4,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(pair(Id,pair(Signer1,PubKey1)),crypt(inv(Kap),pair(SigOK,pair(pair(Contract,pair(Signer1,pair(PubKey1,SignaturePolicy1))),pair(Signer1,PubKey1))))))) step step_OG_4(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Time_n1,Dummy_Time_n21,Dummy_InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,4,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer1,PubKey1)))) => state_OrchestrationGoal(OrchestrationGoal,SID,5,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(pair(Id,pair(Signer1,PubKey1)),crypt(inv(Kap),pair(TsOK,pair(Contract,pair(Signer1,pair(PubKey1,pair(SignaturePolicy1,crypt(inv(PubKey1),pair(Contract,pair(Signer1,pair(PubKey1,SignaturePolicy1))))))))))))) step step_OG_5(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Time_n1,Dummy_Time_n21,Dummy_InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,5,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer1,PubKey1)))) => state_OrchestrationGoal(OrchestrationGoal,SID,6,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(pair(Id,pair(Signer1,pair(PubKey1,False))),crypt(inv(Kap),pair(CertOK,pair(Signer1,PubKey1)))))) step step_OG_6(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Time_n1,Dummy_Time_n21,Dummy_InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,6,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer2,PubKey2)))) => state_OrchestrationGoal(OrchestrationGoal,SID,7,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer2,pair(PubKey2,SignaturePolicy2))))) step step_OG_7(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Time_n1,Dummy_Time_n21,Dummy_InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID, 7,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Contract,pair(Signer2,pair(PubKey2,pair(SignaturePolicy2,crypt(inv(PubKey2),pair(Contract,pair(Signer2,pair(PubKey2,SignaturePolicy2))))))))))) => state_OrchestrationGoal(OrchestrationGoal,SID, 8,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(pair(Id,pair(Signer2,PubKey2)),crypt(inv(Kap),pair(SigOK,pair(pair(Contract,pair(Signer2,pair(PubKey2,SignaturePolicy2))),pair(Signer2,PubKey2))))))) step step_OG_8(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Time_n1,Time_n21,InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,8,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer2,PubKey2)))) => state_OrchestrationGoal(OrchestrationGoal,SID,9,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(pair(Id,pair(Signer2,PubKey2)),crypt(inv(Kap),pair(TsOK,pair(Contract,pair(Signer2,pair(PubKey2,pair(SignaturePolicy2,crypt(inv(PubKey2),pair(Contract,pair(Signer2,pair(PubKey2,SignaturePolicy2))))))))))))) step step_OG_9(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Time_n1,Time_n21,InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,9,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,pair(Signer2,PubKey2)))) => state_OrchestrationGoal(OrchestrationGoal,SID,10,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(pair(Id,pair(Signer2,pair(PubKey2,False))),crypt(inv(Kap),pair(CertOK,pair(Signer2,PubKey2)))))) step step_OG_10(OrchestrationGoal,SID,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2,Time_n1,Time_n21,InID,Dummy_Finish) := state_OrchestrationGoal(OrchestrationGoal,SID,10,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,Id)) => state_OrchestrationGoal(OrchestrationGoal,SID,11,Kap,Karc,Sscl,Pki,Ts,Arc,Ap,Kpki,Kts,Kssarc,Kbpss,SignaturePolicy1,SignaturePolicy2,Md5,True,False,ArcOK,CertOK,SigOK,TsOK,Id,Contract,Signer1,PubKey1,Signer2,PubKey2). iknows(scrypt(Kbpss,pair(Id,crypt(inv(Karc),pair(ArcOK,pair(apply(Md5,Contract),pair(pair(Signer1,PubKey1),pair(Signer2,PubKey2)))))))) section goals: % unreachable goal for the intruder... % attack_state someState(Dummy):= % iknows(kbpss) % The message received by the Archiver should stay secret attack_state secretRevealed(Msg):= keepsecret(Msg). iknows(Msg)