import "library.tf".

////////////////////////////////////////////////////////////
// On-Demand Attachments Protocol
// The WS-Email Project (wsemail.ws)
// February 2005
//
// The encoding below is in an extension of the Pi calculus.  It is
// usable as input to the Samoa Project's TulaFale language compiler.
// The output of the TulaFale compiler may be used as input to
// B. Blanchet's Cryptographic Protocol Verifier.
//
// The script proves a correspondance assertion: 
//
// If the Receiving Client (RC) receives an attachment it must have been
// sent previously by the Sending Client (SC). 
//
// This correspondence may be checked by leaving just the
// queries involving the Received Attachment and SentAttachment events
// uncommented in the query section below.
//
// --------------------------------------------------------
// The 9 messages in the protocol are as follows:
//
// 1- SC -> SS: (username | nonce | creation) | HMAC(nonce | creation | pwd, msg | userAtDomain)
//
// 2- SS -> RS : S(SSx509key, (msg | userAtDomain) | filekey)
//		    | S(SSx509key, (msg | userAtDomain) | filekey)
//
// 3-RS -> RC: S(RSx509key, msgid)
//
// 4-RC -> RS : (username | nonce | creation) | HMAC(nonce | creation | pwd, msgid)
// 
// 5- RS -> RC : S(RSx509key, msgid | S(SSx509cert, (msg | username@domain) | filekey))
//
// 6- RC -> RS : (username | nonce | creation) | HMAC(nonce | creation | pwd, container | pubkey)
// 
// 7- RS -> RC : fedtoken | S(RSx509key, "token granted")
//
// 8- RC -> SS : S(fedtoken, recipientname, filekey)
//
// 9- SS -> RC : S(SSx509cert, attachment, filekey)
// --------------------------------------------------------/
//
// The names of the processes are as given in http://wsemail.ws/WSEmail.pdf
/////////////////////////////////////////////////////////////////


////////////////////////////////////////////////////////////
// Constructors
////////////////////////////////////////////////////////////
// message 1 contains (UserTokenKey for SC, Attachment, text of the email, destination address)
data constructor Message1(item, string, string, item):item.

// message 2 contains (SS's x509 certificate, text of the email, destination address, file key for the the attachment)
data constructor Message2(bytes, string, item, bytes):item.

// message 3 contains (RS's x509 certificate, message id)
data constructor Message3(bytes, bytes):item.

// message 4 contains (UserTokenKey for RC, message id)
data constructor Message4(item, bytes):item.

// message 5 contains (RS x509 certificate, message id, Signed copy of message 2)
data constructor Message5(bytes, bytes, item):item.

// message 6 contains (UserTokenKey for RC, container for public key, public key)
data constructor Message6(item, bytes, bytes):item.

// message 7 contains (RS's x509 certificate, federated token (x509 cert), a string indicating that the fedtoken was granted)
data constructor Message7(bytes, bytes, string):item.

// message 8 contains (federated token (x509 cert), RC's name, filekey for the attachment)
data constructor Message8(bytes, string, bytes):item.

// message 9 contains (SS's x509 certificate, attachment filekey for the attachment)
data constructor Message9(bytes, string, bytes):item.

// UName's parameters (username, domain)
data constructor UName(string, string):item.

// file key to index an attachment
data constructor FileKey(string):bytes.

// message id constructor (email string, attachment file key)
data constructor MessageID(string, bytes):bytes.

////////////////////////////////////////////////////////////
// Public Channels
////////////////////////////////////////////////////////////
// channel to talk to SS
channel SSchan(item). 
// channel to talk to RS
channel RSchan(item).
// channel to publish to everyone (including attacker)
channel publish(item).
// channel to talk to RC
channel RCchan(item).

////////////////////////////////////////////////////////////
// Events
////////////////////////////////////////////////////////////
// Message events
event SentMsg1(item).
event ReceivedMsg1(item).
event SentMsg2(item).
event ReceivedMsg2(item).
event SentMsg3(item).
event ReceivedMsg3(item).
event SentMsg4(item).
event ReceivedMsg4(item).
event SentMsg5(item).
event ReceivedMsg5(item).
event SentMsg6(item).
event ReceivedMsg6(item).
event SentMsg7(item).
event ReceivedMsg7(item).
event SentMsg8(item).
event ReceivedMsg8(item).
event SentMsg9(item).
event ReceivedMsg9(item).

// Lower level events
event CheckedMsg7(item).
event MadeFedtoken(bytes).
event ReceivedFedtoken(bytes).
event SentAttachment(string).
event ReceivedAttachment(string).
event SentEmail(string).
event ReceivedEmail(string).

////////////////////////////////////////////////////////////
// Building and Checking Messages
////////////////////////////////////////////////////////////

///////////////
// Message 1
///////////////
// takes parameters (SC's private user token, nonce, creation time for message, attachment, email text, RC's name, RS's name, Msg1, and Msg1 Signed)
predicate mkMsg1(SC:item, nonce:bytes, creation:string, attachment:string, email:string, TOuser:string, TOdom:string, Msg1:item, Msg1Signed:item) :-
	destUserAtDomain = UName(TOuser, TOdom),
	isUserTokenKey(TokSC, SC, nonce, creation, KeySC),
	Msg1 = Message1(TokSC, attachment, email, destUserAtDomain),
    	mkSignature(Sig, "hmacsha1", KeySC, <list>Msg1</>),
	Msg1Signed = <env>Sig Msg1</>.

predicate isMsg1(Msg1Signed:item, SC:item, TOdom:string, TOuser:string, attachment:string, email:string, destUserAtDomain:item, Msg1:item) :-
  Msg1Signed = <env>Sig Msg1</>,
  Msg1 = Message1(TokSC, attachment, email, destUserAtDomain),
  isUserTokenKey(TokSC, SC, nonce, creation, KeySC),
  isSignature(Sig, "hmacsha1", KeySC, <list>Msg1</>),
  destUserAtDomain = UName(TOuser, TOdom).

///////////////
// Message 2
///////////////
// takes parameters (SS's public certificate, SS's private key, email text, destination address, attachment, Message 2, Signed version of Message 2)
predicate mkMsg2(SScert:bytes, SSx509:bytes, email:string, destUserAtDomain:item, attachment:string, Msg2:item, Msg2Signed:item) :-
	fk = FileKey(attachment),
	Msg2 = Message2(SScert, email, destUserAtDomain, fk),
	mkSignature(Sig, "rsasha1", SSx509, <list>Msg2</>),
	Msg2Signed = <env>Sig Msg2</>.

// takes parameters (Signed Message 2, verification key of the CA, Message 2 unsigned, RC's name, text of the email, filekey of attachment)
predicate isMsg2(Msg2Signed:item, pCA:bytes, Msg2:item, TOuser:string, email:string, fk:bytes) :-
	Msg2Signed = <env>Sig Msg2</>,
	Msg2 = Message2(SScert, email, destUserAtDomain, fk),
	destUserAtDomain = UName(TOuser, TOdom),
	isX509Cert(SScert, pCA, "SS", "rsasha1", SSpubkey),
	isSignature(Sig, "rsasha1", SSpubkey, <list>Msg2</>).

///////////////
// Message 3
///////////////
// takes parameters (RS's public cert, RS's private key, email text, file key for attachment, Message 3, Message 3 signed)
predicate mkMsg3(RScert:bytes, RSx509:bytes, email:string, filekey:bytes, Msg3:item, Msg3Signed:item) :-
	msgid = MessageID(email, filekey),
	Msg3 = Message3(RScert, msgid),
	mkSignature(Sig, "rsasha1", RSx509, <list>Msg3</>),
	Msg3Signed = <env>Sig Msg3</>.

// takes parameters (Signed version of Message 3, verification key of the CA, Message 3 unsigned, message id)
predicate isMsg3(Msg3Signed:item, pCA:bytes, Msg3:item, msgid:bytes) :-
	Msg3Signed = <env>Sig Msg3</>,
	Msg3 = Message3(RScert, msgid),
	isX509Cert(RScert, pCA, "RS", "rsasha1", RSpubkey),
	isSignature(Sig, "rsasha1", RSpubkey, <list>Msg3</>).

///////////////
// Message 4
///////////////

predicate mkMsg4(RC:item, nonce:bytes, creation:string, msgid:bytes, Msg4:item, Msg4Signed:item) :-
	isUserTokenKey(TokRC, RC, nonce, creation, KeyRC),
	Msg4 = Message4(TokRC, msgid),
    	mkSignature(Sig, "hmacsha1", KeyRC, <list>Msg4</>),
	Msg4Signed = <env>Sig Msg4</>.

predicate isMsg4(Msg4Signed:item, RC:item, msgid:bytes, Msg4:item) :-
	Msg4Signed = <env>Sig Msg4</>,
	Msg4 = Message4(TokRC, msgid),
  	isUserTokenKey(TokRC, RC, nonce, creation, KeyRC),
  	isSignature(Sig, "hmacsha1", KeyRC, <list>Msg4</>).

///////////////
// Message 5
///////////////

predicate mkMsg5(RScert:bytes, RSx509:bytes, msgid:bytes, Msg2Signed:item, Msg5:item, Msg5Signed:item) :-
	Msg5 = Message5(RScert, msgid, Msg2Signed),
	mkSignature(Sig, "rsasha1", RSx509, <list>Msg5</>),
	Msg5Signed = <env>Sig Msg5</>.

predicate isMsg5(Msg5Signed:item, pCA:bytes, msgid:bytes, Msg2Signed:item, Msg5:item) :-
	Msg5Signed = <env>Sig Msg5</>,
	Msg5 = Message5(RScert, msgid, Msg2Signed),
	isX509Cert(RScert, pCA, "RS", "rsasha1", RSpubkey),
	isSignature(Sig, "rsasha1", RSpubkey, <list>Msg5</>).

///////////////
// Message 6
///////////////

predicate mkMsg6(RC:item, nonce:bytes, creation:string, container:bytes, pubkey:bytes, Msg6:item, Msg6Signed:item) :-
	isUserTokenKey(TokRC, RC, nonce, creation, KeyRC),
	Msg6 = Message6(TokRC, container, pubkey),
	mkSignature(Sig, "hmacsha1", KeyRC, <list>Msg6</>),
	Msg6Signed = <env>Sig Msg6</>.

predicate isMsg6(Msg6Signed:item, RC:item, container:bytes, pubkey:bytes, Msg6:item) :-
	Msg6Signed = <env>Sig Msg6</>,
	Msg6 = Message6(TokRC, container, pubkey),
	isUserTokenKey(TokRC, RC, nonce, creation, KeyRC),
	isSignature(Sig, "hmacsha1", KeyRC, <list>Msg6</>).

///////////////
// Message 7
///////////////

predicate mkMsg7(RScert:bytes, RSx509:bytes, granted:string, fedtoken:bytes, Msg7:item, Msg7Signed:item) :-
	Msg7 = Message7(RScert, fedtoken, granted),
	mkSignature(Sig, "rsasha1", RSx509, <list>Msg7</>),
	Msg7Signed = <env>Sig Msg7</>.

predicate isMsg7(Msg7Signed:item, pCA:bytes, fedtoken:bytes, granted:string, Msg7:item) :-
	Msg7Signed = <env>Sig Msg7</>,
	Msg7 = Message7(RScert, fedtoken, granted),
	isX509Cert(RScert, pCA, "RS", "rsasha1", RSpubkey),
	isSignature(Sig, "rsasha1", RSpubkey, <list>Msg7</>).

predicate mkFedtoken(RSx509:bytes, RCpubkey:bytes, fedtoken:bytes) :-
	fedtoken = x509(RSx509, "RC", "rsasha1", RCpubkey).

predicate isFedtoken(fedtoken:bytes, pCA:bytes, RScert:bytes, RCx509:bytes) :-
	isX509Cert(RScert, pCA, "RS", "rsasha1", RSpubkey),
	isX509Cert(fedtoken, RSpubkey, "RC", "rsasha1", RCpubkey),
	RCpubkey = pk(RCx509).

predicate checkFedtoken(fedtoken:bytes, pCA:bytes, RScert:bytes, RCpubkey:bytes) :-
	isX509Cert(RScert, pCA, "RS", "rsasha1", RSpubkey),
	isX509Cert(fedtoken, RSpubkey, "RC", "rsasha1", RCpubkey).

///////////////
// Message 8
///////////////

predicate mkMsg8(fedtoken:bytes, RCx509:bytes, RCname:string, filekey:bytes, Msg8:item, Msg8Signed:item) :-
	Msg8 = Message8(fedtoken, RCname, filekey),
	mkSignature(Sig, "rsasha1", RCx509, <list>Msg8</>),
	Msg8Signed = <env>Sig Msg8</>.

predicate isMsg8(Msg8Signed:item, RScert:bytes, pCA:bytes, RCname:string, filekey:bytes, Msg8:item) :-
	Msg8Signed = <env>Sig Msg8</>,
	Msg8 = Message8(fedtoken, RCname, filekey),
	isX509Cert(RScert, pCA, "RS", "rsasha1", RSpubkey),
	isX509Cert(fedtoken, RSpubkey, "RC", "rsasha1", RCpubkey),
	isSignature(Sig, "rsasha1", RCpubkey, <list>Msg8</>).
	
///////////////
// Message 9
///////////////

predicate mkMsg9(SScert:bytes, SSx509:bytes, filekey:bytes, Msg9:item, Msg9Signed:item) :-
	filekey = FileKey(attachment),
	Msg9 = Message9(SScert, attachment, filekey),
	mkSignature(Sig, "rsasha1", SSx509, <list>Msg9</>),
	Msg9Signed = <env>Sig Msg9</>.

predicate isMsg9(Msg9Signed:item, pCA:bytes, filekeyIN:bytes, attachment:string, Msg9:item) :-
	Msg9Signed = <env>Sig Msg9</>,
	Msg9 = Message9(SScert, attachment, filekey),
	isX509Cert(SScert, pCA, "SS", "rsasha1", SSpubkey),
	isSignature(Sig, "rsasha1", SSpubkey, <list>Msg9</>),
	filekeyIN = FileKey(attachment),
	filekeyIN = filekey.

/////////////////////////////////////////////////////////////
// Processses
/////////////////////////////////////////////////////////////
process pSC(SC:item) =
	// needed pieces
	new nonce:bytes; new creation:string; new attachment:string; new email:string; new TOuser:string; new TOdom:string;

	// create the first message
	filter mkMsg1(SC, nonce, creation, attachment, email, TOuser, TOdom, Msg1, Msg1Signed) -> Msg1,Msg1Signed;
	// we've made the first message
	event SentMsg1(Msg1);
	// sent the attachment
	event SentAttachment(attachment);
	// sent the email text
	event SentEmail(email);
	// now send it
	out SSchan (Msg1Signed).

process pSS(SC:item, RScert:bytes, SScert:bytes, SSx509:bytes, pCA:bytes) = 
	// received the first message
	in SSchan (Msg1S);
	// check it for accuracy
	filter isMsg1(Msg1S, SC, TOuser, TOdom, attachment, email, destUserAtDomain, Msg1) -> TOuser, TOdom, attachment, email, destUserAtDomain, Msg1;
	// we've got a message 1
	event ReceivedMsg1(Msg1);

	// create message 2
	filter mkMsg2(SScert, SSx509, email, destUserAtDomain, attachment, Msg2, Msg2Signed) -> Msg2, Msg2Signed;
	// we've created it
	event SentMsg2(Msg2);
	// now send it
	out RSchan(Msg2Signed);

	// receive message 8
	in SSchan(Msg8Signed);
	// check it
	filter isMsg8(Msg8Signed, RScert, pCA, RCname, filekey, Msg8) -> RCname, filekey, Msg8;
	// we've got message 8
	event ReceivedMsg8(Msg8);

	// now build message 9
	filter mkMsg9(SScert, SSx509, filekey, Msg9, Msg9Signed) -> Msg9, Msg9Signed;
	// we've created it
	event SentMsg9(Msg9);
	// now send it
	out RCchan(Msg9Signed).	

process pRS(RScert:bytes, RSx509:bytes, SScert:bytes, pCA:bytes, RC:item) = 
	// receive the second message
	in RSchan(Msg2Signed);
	//check for its accuracy
	filter isMsg2(Msg2Signed, pCA, Msg2, TOuser, email, fk) -> Msg2, TOuser, email, fk;
	//we've got a message 2
	event ReceivedMsg2(Msg2);

	// now make the third message
	filter mkMsg3(RScert, RSx509, email, fk, Msg3, Msg3Signed) -> Msg3, Msg3Signed;
	// we've created it
	event SentMsg3(Msg3);
	// now send it
	out RCchan(Msg3Signed);

	// receive the fourth message
	in RSchan(Msg4Signed);
	// check for its accuracy
	filter isMsg4(Msg4Signed, RC, msgid, Msg4) -> msgid, Msg4;
	// we've got it
	event ReceivedMsg4(Msg4);

	// now make the fifth message
	filter mkMsg5(RScert, RSx509, msgid, Msg2Signed, Msg5, Msg5Signed) -> Msg5, Msg5Signed;
	// we've created it
	event SentMsg5(Msg5);
	// now send it
	out RCchan(Msg5Signed);

	// receive the sixth message
	in RSchan(Msg6Signed);
	// check for its accuracy
	filter isMsg6(Msg6Signed, RC, container, RCpubkey, Msg6) -> container, RCpubkey, Msg6;
	// we've got it
	event ReceivedMsg6(Msg6);

	// make the federated token
	filter mkFedtoken(RSx509, RCpubkey, fedtoken) -> fedtoken;
	// we made it
	event MadeFedtoken(fedtoken);
	// publish the federated token
	out publish(base64(fedtoken));

	// now make the seventh message
	new granted:string;
	filter mkMsg7(RScert, RSx509, granted, fedtoken, Msg7, Msg7Signed) -> Msg7, Msg7Signed;
	// we've created it
	event SentMsg7(Msg7);

	// now send it
	out RCchan(Msg7Signed).

process pRC(RC:item, RCx509:bytes, RCpubkey:bytes, RScert:bytes, pCA:bytes) = 
	// pieces needed for Msg6
	new nonce2:bytes; new creation2:string; new container:bytes;

	//receive the third message
	in RCchan(Msg3Signed);
	// check for its accuracy
	filter isMsg3(Msg3Signed, pCA, Msg3, msgid) -> Msg3, msgid;
	// we've got message 3
	event ReceivedMsg3(Msg3);

	// now build message 4
	new nonce:bytes; new creation:string;
	filter mkMsg4(RC, nonce, creation, msgid, Msg4, Msg4Signed) -> Msg4, Msg4Signed;
	// we've created it
	event SentMsg4(Msg4);
	// now send it
	out RSchan(Msg4Signed);

	// receive the fifth message
	in RCchan(Msg5Signed);
	// check it that it's a valid message 5
	filter isMsg5(Msg5Signed, pCA, msgid, Msg2Signed, Msg5) -> Msg2Signed, Msg5;
	// now check that we have a valid message 2
	filter isMsg2(Msg2Signed, pCA, Msg2, TOuser, email, fk) -> Msg2, TOuser, email, fk;
	// we've got it
	event ReceivedMsg5(Msg5);
	// we've got the email
	event ReceivedEmail(email);

	// now build message 6
	filter mkMsg6(RC, nonce2, creation2, container, RCpubkey, Msg6, Msg6Signed) -> Msg6, Msg6Signed;
	// we've created it
	event SentMsg6(Msg6);
	// now send it
	out RSchan(Msg6Signed);

	// now accept the seventh message
	in RCchan(Msg7Signed);
	// try checking it
	filter isMsg7(Msg7Signed, pCA, fedtoken, granted, Msg7) -> fedtoken, granted, Msg7;
	// we've got message 7
	event ReceivedMsg7(Msg7);
	// check the fedtoken
	filter isFedtoken(fedtoken, pCA, RScert, RCx509) -> ;
	// we've got a federated token
	event ReceivedFedtoken(fedtoken);

	// get our name
	filter isUser(RC, RCname, RCpwd) -> RCname, RCpwd;
	// now build message 8
	filter mkMsg8(fedtoken, RCx509, RCname, fk, Msg8, Msg8Signed) -> Msg8, Msg8Signed;
	// we've built it
	event SentMsg8(Msg8);
	// now send it
	out SSchan(Msg8Signed);

	// now receive message 9
	in RCchan(Msg9Signed);
	// check it
	filter isMsg9(Msg9Signed, pCA, fk, attachment, Msg9) -> attachment, Msg9;
	// we've got it
	event ReceivedMsg9(Msg9);
	// we've got the attachment
	event ReceivedAttachment(attachment).	

//////////////////////////////////////////////////////////////////
// Queries
//////////////////////////////////////////////////////////////////
// queries to prevent trivial correspondences
//query SentMsg1(Msg1).
//query ReceivedMsg1(Msg1).
//query SentMsg2(Msg2).
//query ReceivedMsg2(Msg2).
//query SentMsg3(Msg3).
//query ReceivedMsg3(Msg3).
//query SentMsg4(Msg4).
//query ReceivedMsg4(Msg4).
//query SentMsg5(Msg5).
//query ReceivedMsg5(Msg5).
//query SentMsg6(Msg6).
//query ReceivedMsg6(Msg6).
//query SentMsg7(Msg7).
//query ReceivedMsg7(Msg7).
//query SentMsg8(Msg8).
//query ReceivedMsg8(Msg8).
//query SentMsg9(Msg9).
//query ReceivedMsg9(Msg9).

//query MadeFedtoken(fedtoken).
//query ReceivedFedtoken(fedtoken).
//query CheckedMsg7(Msg7).
//query CheckedMsg7(Msg7) ==> SentMsg7(Msg7).

// queries for the attachment
//
// Use the following three queries to check the correspondence
// mentioned above.
//
//query SentAttachment(attachment).
query ReceivedAttachment(attachment).
query ReceivedAttachment(attachment) ==> SentAttachment(attachment).

// queries for messages being received if sent
//query ReceivedMsg1(Msg1) ==> SentMsg1(Msg1).
//query ReceivedMsg2(Msg2) ==> SentMsg2(Msg2).
//query ReceivedMsg3(Msg3) ==> SentMsg3(Msg3).
//query ReceivedMsg4(Msg4) ==> SentMsg4(Msg4).
//query ReceivedMsg5(Msg5) ==> SentMsg5(Msg5).
//query ReceivedMsg6(Msg6) ==> SentMsg6(Msg6).
//query ReceivedMsg7(Msg7) ==> SentMsg7(Msg7).

// correspondence of email
//query ReceivedEmail(email) ==> SentEmail(email).

// correspondence of protocol
// receiving 2 implies 1 was sent
//query ReceivedMsg2(Msg2) ==> SentMsg1(Msg1).
//query ReceivedMsg3(Msg3) ==> SentMsg1(Msg1).
//query ReceivedMsg4(Msg4) ==> SentMsg1(Msg1).
//query ReceivedMsg5(Msg5) ==> SentMsg1(Msg1).
//query ReceivedMsg6(Msg6) ==> SentMsg1(Msg1).
//query ReceivedMsg7(Msg7) ==> SentMsg7(Msg7).

/////////////////////////////////////////////////////////////////
// Main process
/////////////////////////////////////////////////////////////////
// create the shared user name and password for SC
new SCname:string; new SCpwd:string;
// create the shared user name and password for RC
new RCname:string; new RCpwd:string;

// create the usertoken for SC
filter isUser(SC, SCname, SCpwd) -> SC;
// create the usertoken for RC
filter isUser(RC, RCname, RCpwd) -> RC;

// CA private and public keys
new CAx509:bytes;
let pCA = pk(CAx509);

// x509 cert for SS
new SSx509:bytes; let SScert = x509(CAx509,"SS","rsasha1",pk(SSx509));
//x509 cert for RS
new RSx509:bytes; let RScert = x509(CAx509, "RS", "rsasha1", pk(RSx509));

// new private key for RC
new RCx509:bytes;
// new public key for RC
let RCpubkey = pk(RCx509);

// public the certs and CA's public key in base64 encoding
out publish(base64(pCA));
out publish(base64(SScert));
out publish(base64(RScert));

!pSC(SC) | !pSS(SC, RScert, SScert, SSx509, pCA) | !pRS(RScert, RSx509, SScert, pCA, RC) | !pRC(RC, RCx509, RCpubkey, RScert, pCA)