% @verbatim(Formalization of Transport Layer Security (TLS)} % @modeler(David von Oheimb, Siemens AG, 2010-2012) % @clatse(--nb 2 --lvl 0) % We assume encryption and signatures by the channel notation *->* % We implement freshness using session IDs and message counters % We implement message order preservation using message counters specification TLS channel_model CCM entity Environment { symbols server: agent; started(agent): fact; entity Session(C, S: agent) { entity Client (Actor, S: agent) { symbols SessID: text; Counter: nat; PayloadC, PayloadS: text; body { secret_session:(SessID) := fresh(); Counter := 0; % start of session: no payload sent yet Actor *->* S: Actor.SessID.Counter; Counter := succ(Counter); %1 PayloadC := fresh(); Actor *->* S: Client_TLS_Server:((SessID.Counter). PayloadC); S *->* Actor: Server_TLS_Client:((SessID.Counter).?PayloadS); Counter := succ(Counter); %2 PayloadC := fresh(); Actor *->* S: Client_TLS_Server:((SessID.Counter). PayloadC); S *->* Actor: Server_TLS_Client:((SessID.Counter).?PayloadS); %assert finished: false; %%% for executability testing } } entity Server(C, Actor: agent) { % C given here only for stating goals symbols Sessions: (agent*text*nat) set; % global for all Server threads SessID: text; entity Thread(C, Actor: agent, SessID: text, Sessions: (agent*text*nat) set) { symbols N: nat; PayloadC, PayloadS: text; body { while(true) { select { on(C *->* Actor: Client_TLS_Server:((SessID.?N).?PayloadC) & Sessions->contains((C,SessID,?N)) ): { PayloadS := fresh(); Actor *->* C: Server_TLS_Client:((SessID. N). PayloadS); Sessions->remove((C,SessID, N )); Sessions->add ((C,SessID,succ(N))); % N+1 } } } } } body { % of the Server Sessions := {}; while(true) { select { on(?C *->* Actor: ?C.secret_session:(?SessID).0 & % Server learns C here! !Sessions->contains((?C,?SessID,?)) ): { Sessions->add((C,SessID,1)); new Thread(C, Actor, SessID, Sessions); % The Thread's Actor is the same as for the Server! } } } } } body { % of Session new Client(C, S); if (!started(S)) { % force all sessions with the same Server instance started(S); new Server(C, S); } } goals secret_session:(_) {C, S}; Client_TLS_Server:(_) C *->>* S; % confidential, authentic, fresh, ordered Server_TLS_Client:(_) S *->>* C; % confidential, authentic, fresh, ordered } body { % of the Environment any C. Session(C, server) where C!=server; any C. Session(C, server) where C!=server; } }