MessageEncryption.spdl.txt

protocol smartExchange(Meter,Monitor)  
    {

	role Meter {

    	fresh Message: Nonce;
    	var Confirm;
    
    	send_1(Meter,Monitor,{Message}k(k));
    	
    	recv_2(Monitor,Meter,{Confirm}k(k));
    
    	claim_Meter1(Meter, Secret, (k));
    	claim_Meter2(Meter, Secret, Message);

	}

	role Monitor {

    	var Message;
    	fresh Confirm: Nonce;
    
    	recv_1(Meter,Monitor,{Message}k(k));
    	
    	send_2(Monitor,Meter,{Confirm}k(k));
    
    	claim_Monitor1(Monitor, Secret, (k));
    	claim_Monitor2(Monitor, Secret, Message);
    }

}