---- The Kao Chow Repeated Authentication Protocols --------------------------------------------------- --- We modify only the relevant MAUDE-NPA modules --------------------------------------------------- fmod PROTOCOL-EXAMPLE-SYMBOLS is --- Importing sorts Msg, Fresh, Public protecting DEFINITION-PROTOCOL-RULES . ---------------------------------------------------------- --- Overwrite this module with the syntax of your protocol --- Notes: --- * Sort Msg and Fresh are special and imported --- * Every sort must be a subsort of Msg --- * No sort can be a supersort of Msg ---------------------------------------------------------- --- Sort Information sorts UName SName Name Key Nonce Masterkey Sessionkey . subsort Name Nonce Key < Msg . subsort Masterkey Sessionkey < Key . subsort SName UName < Name . subsort Name < Public . --- This is quite relevant and necessary --- Nonce operator op n : Name Fresh -> Nonce [frozen] . op t : Name Fresh -> Nonce [frozen] . ---Nonce del server --- User names ops a b i : -> UName . --- Server name op s : -> SName . --- MKey op mkey : Name Name -> Masterkey [frozen] . --- Seskey op seskey : Name Name Nonce -> Sessionkey [frozen] . ---encrypt op e : Key Msg -> Msg [frozen] . op d : Key Msg -> Msg [frozen] . --- successor op p : Msg -> Msg [frozen] . --- Concatenation op _;_ : Msg Msg -> Msg [frozen gather (e E)] . endfm fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS . ---------------------------------------------------------- --- Overwrite this module with the algebraic properties --- of your protocol ---------------------------------------------------------- eq d(K:Key, e(K:Key, Z:Msg)) = Z:Msg [variant] . eq e(K:Key, d(K:Key, Z:Msg)) = Z:Msg [variant] . endfm fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS . protecting DEFINITION-PROTOCOL-RULES . protecting DEFINITION-CONSTRAINTS-INPUT . ---------------------------------------------------------- --- Overwrite this module with the strands --- of your protocol ---------------------------------------------------------- var A B : UName . var D : Name . var r r' r'' r''' r# r## : Fresh . --- Comerntario chorra vars TS NA NB : Nonce . vars M1 M2 M N MA : Msg . var K Kt : Key . var SK : Sessionkey . eq STRANDS-DOLEVYAO = :: nil :: [ nil | +(D), nil ] & :: nil :: [ nil | -(K), -(M), +(d(K,M)), nil ] & :: nil :: [ nil | -(K), -(M), +(e(K,M)), nil ] & :: nil :: [ nil | -(N), -(M), +(M ; N) , nil ] & :: nil :: [ nil | -(M ; N), +(M) , nil ] & :: nil :: [ nil | -(M ; N), +(N) , nil ] & :: nil :: [ nil | +(mkey(i,D)), nil ] & :: nil :: [ nil | +(mkey(D,i)), nil ] [nonexec] . eq STRANDS-PROTOCOL = --- A->S : A,B,Na --- S->B : E(Kas:A, B, Na, Kab), E(Kbs:A, B, Na, Kab) --- B->A : E(Kas:A, B, Na, Kab), E(Kab:Na), Nb --- A->B : E(Kab:Nb) --- Alice's Strand :: r :: [ nil | +(A ; B ; n(A,r)), -(e(mkey(A,s), A ; B ; n(A,r) ; SK) ; e(SK, n(A,r)) ; NB), +(e(SK, NB)) , nil ] & --- Bob's Strand :: r :: [ nil | -(MA ; e(mkey(B,s), A ; B ; NA ; SK)) , +(MA ; e(SK, NA) ; n(B,r)), -(e(SK, n(B,r))), nil ] & :: r :: --- Server's Strand [ nil | -(A ; B ; NA), +( e(mkey(A,s), A ; B ; NA ; seskey(A,B,n(s,r))) ; e(mkey(B,s), A ; B ; NA ; seskey(A,B,n(s,r)))), nil ] [nonexec] . eq ATTACK-STATE(0) = :: r :: --- A normal execution of the protocol [ nil , -(MA ; e(mkey(b,s), a ; b ; NA ; SK)) , +(MA ; e(SK, NA) ; n(b,r)), -(e(SK, n(b,r))) | nil ] || empty || nil || nil || nil [nonexec] . eq ATTACK-STATE(1) = :: r :: --- An execution where the intruder finds out the Session key generated by the server [ nil, -(MA ; e(mkey(b,s), a ; b ; NA ; SK)) , +(MA ; e(SK, NA) ; n(b,r)), -(e(SK, n(b,r))) | nil ] || SK inI || nil || nil || nil [nonexec] . eq ATTACK-STATE(2) = :: r :: ---An execution where Bob completed the protocol believing that talks to Alice, but it is not so [ nil , -(MA ; e(mkey(b,s), a ; b ; NA ; SK)) , +(MA ; e(SK, NA) ; n(b,r)), -(e(SK, n(b,r))) | nil ] || empty || nil || nil || never *** Pattern for authentication (:: R:FreshSet :: [ nil | +(A ; B ; NA), -(MA ; e(SK, NA) ; n(b,r)), +(e(SK, n(b,r))), nil ] & S:StrandSet || K:IntruderKnowledge) [nonexec] . ---eq USER-GRAMMARS ---= (grl empty => e(#1:Key, #2:Msg) inL . ! S2) ---[nonexec] . endfm --- THIS HAS TO BE THE LAST LOADED MODULE !!!! fmod MAUDE-NPA is protecting GENERIC-TOOLS . endfm