Verification of the NSLPK Authentication Protocol (1) Kazuhiro Ogata (NEC Software Hokuriku, Ltd./JAIST) * Introduction The Needham-Schroeder public-key authentication protocol, or NSPK is a security protocol designed by Needham and Schroeder in 1978. 17 years later, Lowe fond a serious attack to the protocol and propsed a possible modification; the modified protocol is called the Needham-Schroeder-Lowe public-key authentication protocol, or NSLPK. This shows how subtle security protocols are; security protocols deserve to verify formally. * Terminology and Notions - Principals - Public-Key Cryptosystems - Nonces * Principals Participants in security protocols are called principals. Principals could be human beings, computer software, PDAs, etc. * Public-Key Cryptosystems - Traditional crytosystems +----------+ === Encrypt with K ===> +-----------+ |Plain text| |Cipher text| +----------+ <=== Decryot with K === +-----------+ - Public-Key Cryptosystems +----------+ === Encrypt with K ===> +-----------+ |Plain text| |Cipher text| +----------+ <=== Decryot with K^{-1} === +-----------+ where K =/= K^{-1}. K: Public key; can be known by everyone. K^{-1}: Private key; must be kept secret. * Nonces Nonces are values each of wihch should be used only once for a purpose. Nonces are classified into two types: - Guessable ones; implemented by indexes, time stamps, etc. - Nonguessable ones; implemenmted by large random numbers. The latter are used in NSPK and NSLPK. * NSPK enc(p, m1, m2, ...) : The cipher text obtained by encrypting m1, m2, ... with the principal p's public key. Suppose that each principal is given a pair of keys; the private one is known by only the principal, while the public one is known by every principal. ---------------------------------------------------------------- Msg1 p --> q : enc(q, n_p, p) Msg2 q --> p : enc(p, n_p, n_q) Msg3 p --> q : enc(q, n_q) ---------------------------------------------------------------- p is called an initiator, and q a responder. An execution of protocols is called a run. When a run of the protocol successfully completes, what does the two principals involved in the run expect? For each successfully completed run that seems involved by two principals p and q, - Two nonces used in the run are never leaked. - The two principals p and q have really involved in the run. * Counter Example p i q Run A Run B | | | | --- enc(i,n_p,p) ---> | | | | | | | --- enc(q,n_p,p) ---> | | | | | | <-- enc(p,n_p,n_q) -- | | | | | <-- enc(p,n_p,n_q) -- | | | | | | ---- enc(i,n_q) ----> | | | | | | | ---- enc(q,n_q) ----> | | | | At the end of run B, principal q believes that p and q have been mutually authenticated and the two nonces n_p and n_q are known by only p and q. But, principal p does not involve run B, and principal i knows the two nonces. * NSLPK One possible modification to solve the flaw is to include responders' IDs in Msg2 messages. ---------------------------------------------------------------- Msg1 p --> q : enc(q, n_p, p) Msg2 q --> p : enc(p, n_p, n_q, q) Msg3 p --> q : enc(q, n_q) ---------------------------------------------------------------- In order to confirm that NSLPK really works as expected, we are going to formally verify that the protocol has desired (security) properties. But, in order to verify that the protocol has desired properties, we should make a formal model of the protocol. * Assumptions - Each principal is given a pair of keys; the public counterpart is known by every principal, while the private counterpart is known by only the principal. - Cryptosystems used are perfect, namely that the cipher text obtained by encrypting with a public key cannot be decrypted without the private counterpart, and nonces cannot be guessed. - The medium by which messages are transmitted, or the network is insecure, namely that any message being transmitted over the network can be eavesdropped, and any message that seems to originate from any principal can be addressed to any principal. - There are an arbitrary number of trustable principals who exactly follow the protocol. - There exists a malicious (untrustable) principal, called the intruder, who may also do something against the protocol: + The intruder eavesdrops all messages that have been sent. + If a cipher text retrieved from a message is encrypted with the intruder's public key, then the intruder memorize the nonces used in the cipher text. + Otherwise, the intruder memorize the cipher text. + The intruder fakes messages only based on the gleaned nonces and cipher texts and sends them. If the intruder obtains enc(i, n_p, n_q, q) where i is the intruder, he/she obtains the nonces n_p and n_q from this cipher text. Even if the intrudr obtains enc(p, n_p, n_q, q) where p is not the intruder, he/she cannot obtain the nonces n_p and n_q from this cipher text. If the intruder knows nonces n_p and n_q, then he/she can fake enc(p, n_p, n_q, q) and sends it to p as it has originated from q. Unless the intruder knows nonces n_p and n_q, then he/she cannot make enc(p, n_p, n_q, q). * Data Types to Formalize Messages - Principals (IDs) - Random numbers - Nonces - Three types of cipher texts - Principals mod* PRINCIPAL principal-sort Principal { [Principal] op intruder : -> Principal op _=_ : Principal Principal -> Bool {comm} var P : Principal eq (P = P) = true . } - Random numbers mod* RANDOM principal-sort Random { [Random] op _=_ : Random Random -> Bool {comm} var R : Random eq (R = R) = true . } - Nonces Given principals p,q and random number r, term n(p,q,r) denotes a nonce generated by principal p to authenticate principal q, where random number r makes the nonce globally unique and unguessable. mod! NONCE principal-sort Nonce { pr(PRINCIPAL + RANDOM) [Nonce] op n : Principal Principal Random -> Nonce op creator : Nonce -> Principal op forwhom : Nonce -> Principal op random : Nonce -> Random op _=_ : Nonce Nonce -> Bool {comm} vars N1 N2 : Nonce var C : Principal var W : Principal var R : Random eq creator(n(C,W,R)) = C . eq forwhom(n(C,W,R)) = W . eq random(n(C,W,R)) = R . eq (N1 = N2) = (creator(N1) = creator(N2) and forwhom(N1) = forwhom(N2) and random(N1) = random(N2)) . } - Cipher texts (1) Given principals p,q and nonce n_p, term enc1(q,n_p,p) denotes cipher text enc(q,n_p,p). mod! CIPHER1 principal-sort Cipher1 { pr(PRINCIPAL + NONCE) [Cipher1] op enc1 : Principal Nonce Principal -> Cipher1 op key : Cipher1 -> Principal op nonce : Cipher1 -> Nonce op principal : Cipher1 -> Principal op _=_ : Cipher1 Cipher1 -> Bool {comm} vars E11 E12 : Cipher1 var K : Principal var N : Nonce var P : Principal eq key(enc1(K,N,P)) = K . eq nonce(enc1(K,N,P)) = N . eq principal(enc1(K,N,P)) = P . eq (E11 = E12) = (key(E11) = key(E12) and nonce(E11) = nonce(E12) and principal(E11) = principal(E12)) . } - Cipher texts (2) Given principals p,q and nonces n_p,n_q term enc2(p,n_p,n_q,p) denotes cipher text enc(p,n_p,n_q,p). mod! CIPHER2 principal-sort Cipher2 { pr(PRINCIPAL + NONCE) [Cipher2] op enc2 : Principal Nonce Nonce Principal -> Cipher2 op key : Cipher2 -> Principal op nonce1 : Cipher2 -> Nonce op nonce2 : Cipher2 -> Nonce op principal : Cipher2 -> Principal op _=_ : Cipher2 Cipher2 -> Bool {comm} vars E21 E22 : Cipher2 var K : Principal var N1 : Nonce var N2 : Nonce var P : Principal eq key(enc2(K,N1,N2,P)) = K . eq nonce1(enc2(K,N1,N2,P)) = N1 . eq nonce2(enc2(K,N1,N2,P)) = N2 . eq principal(enc2(K,N1,N2,P)) = P . eq (E21 = E22) = (key(E21) = key(E22) and nonce1(E21) = nonce1(E22) and nonce2(E21) = nonce2(E22) and principal(E21) = principal(E22)) . } - Cipher texts (3) Given principal q and nonce n_q term enc3(q,n_q) denotes cipher text enc(q,n_q). mod! CIPHER3 principal-sort Cipher3 { pr(PRINCIPAL + NONCE) [Cipher3] op enc3 : Principal Nonce -> Cipher3 op key : Cipher3 -> Principal op nonce : Cipher3 -> Nonce op _=_ : Cipher3 Cipher3 -> Bool {comm} vars E31 E32 : Cipher3 var K : Principal var N : Nonce eq key(enc3(K,N)) = K . eq nonce(enc3(K,N)) = N . eq (E31 = E32) = (key(E31) = key(E32) and nonce(E31) = nonce(E32)) . } * Formalizing Messages The three operators (data constructors) to deonte the three types of messages: op m1 : Principal Principal Principal Cipher1 -> Message op m2 : Principal Principal Principal Cipher2 -> Message op m3 : Principal Principal Principal Cipher3 -> Message The first argument of each operator means the actual sender of the corresponding message, which is the meta information that is only available to the outside observer and the principal that has sent the message. The second argument of each operator means the seeming sender of the corresponding message. The third argument of each operator means the destination of the corresponding message. Suppoe that there exists m1(p1,p2,q,c1) in the network. - It is true that the message has been sent by p1. - If p1 is different from p2, then the message has been faked by p1 who is the intruder. - If p2 is the intruder, then so is p1 because one and only principal who fakes messages is the intruder. mod! MESSAGE principal-sort Message { pr(PRINCIPAL + CIPHER1 + CIPHER2 + CIPHER3) [Message] -- creator sender receiver -- -------------------------------------------------- op m1 : Principal Principal Principal Cipher1 -> Message op m2 : Principal Principal Principal Cipher2 -> Message op m3 : Principal Principal Principal Cipher3 -> Message -- op m1? : Message -> Bool op m2? : Message -> Bool op m3? : Message -> Bool -- op creator : Message -> Principal op sender : Message -> Principal op receiver : Message -> Principal op cipher1 : Message -> Cipher1 op cipher2 : Message -> Cipher2 op cipher3 : Message -> Cipher3 -- op _=_ : Message Message -> Bool {comm} -- vars M M1 M2 : Message vars C S R : Principal var E1 : Cipher1 var E2 : Cipher2 var E3 : Cipher3 -- eq m1?(m1(C,S,R,E1)) = true . eq m1?(m2(C,S,R,E2)) = false . eq m1?(m3(C,S,R,E3)) = false . eq m2?(m1(C,S,R,E1)) = false . eq m2?(m2(C,S,R,E2)) = true . eq m2?(m3(C,S,R,E3)) = false . eq m3?(m1(C,S,R,E1)) = false . eq m3?(m2(C,S,R,E2)) = false . eq m3?(m3(C,S,R,E3)) = true . -- eq creator(m1(C,S,R,E1)) = C . eq creator(m2(C,S,R,E2)) = C . eq creator(m3(C,S,R,E3)) = C . eq sender(m1(C,S,R,E1)) = S . eq sender(m2(C,S,R,E2)) = S . eq sender(m3(C,S,R,E3)) = S . eq receiver(m1(C,S,R,E1)) = R . eq receiver(m2(C,S,R,E2)) = R . eq receiver(m3(C,S,R,E3)) = R . eq cipher1(m1(C,S,R,E1)) = E1 . eq cipher2(m2(C,S,R,E2)) = E2 . eq cipher3(m3(C,S,R,E3)) = E3 . -- eq (M = M) = true . ceq (M1 = M2) = (m1?(M2) and creator(M1) = creator(M2) and sender(M1) = sender(M2) and receiver(M1) = receiver(M2) and cipher1(M1) = cipher1(M2)) if m1?(M1) . ceq (M1 = M2) = (m2?(M2) and creator(M1) = creator(M2) and sender(M1) = sender(M2) and receiver(M1) = receiver(M2) and cipher2(M1) = cipher2(M2)) if m2?(M1) . ceq (M1 = M2) = (m3?(M2) and creator(M1) = creator(M2) and sender(M1) = sender(M2) and receiver(M1) = receiver(M2) and cipher3(M1) = cipher3(M2)) if m3?(M1) . } * Formalizing the Network - The network is modeled as a bag (multiset) of messages. - The network is used as the storage that the intruder use. - The network is also used as each principal's private memory. - Any message that has been sent or put once into the network is supposed to be never deleted from the network; consequently, the emptiness of the network means that no messages have been sent. The intruder tries to glean four kinds of quantities from the network. - nonces - three types of cipher texts The collections of those quantities are denoted by the operators: op cnonce : Network -> ColNonce op cenc1 : Network -> ColCipher1 op cenc2 : Network -> ColCipher2 op cenc3 : Network -> ColCipher3 Given network nw, - cnonce(nw) denotes the collection of nonces gleaned from nw. - cenc1(nw) denotes the collection of cipher texts in Msg1 messages. - cenc2(nw) denotes the collection of cipher texts in Msg2 messages. - cenc3(nw) denotes the collection of cipher texts in Msg3 messages. The operators are defined with equations. - cnonce eq N \in cnonce(void) = (creator(N) = intruder) . ceq N \in cnonce(M,NW) = true if m1?(M) and key(cipher1(M)) = intruder and nonce(cipher1(M)) = N . ceq N \in cnonce(M,NW) = true if m2?(M) and key(cipher2(M)) = intruder and nonce1(cipher2(M)) = N . ceq N \in cnonce(M,NW) = true if m2?(M) and key(cipher2(M)) = intruder and nonce2(cipher2(M)) = N . ceq N \in cnonce(M,NW) = true if m3?(M) and key(cipher3(M)) = intruder and nonce(cipher3(M)) = N . ceq N \in cnonce(M,NW) = N \in cnonce(NW) if not(m1?(M) and key(cipher1(M)) = intruder and nonce(cipher1(M)) = N) and not(m2?(M) and key(cipher2(M)) = intruder and nonce1(cipher2(M)) = N) and not(m2?(M) and key(cipher2(M)) = intruder and nonce2(cipher2(M)) = N) and not(m3?(M) and key(cipher3(M)) = intruder and nonce(cipher3(M)) = N) . - cenc1 eq E1 \in cenc1(void) = false . ceq E1 \in cenc1(M,NW) = true if m1?(M) and not(key(cipher1(M)) = intruder) and E1 = cipher1(M) . ceq E1 \in cenc1(M,NW) = E1 \in cenc1(NW) if not(m1?(M) and not(key(cipher1(M)) = intruder) and E1 = cipher1(M)) . - cenc2 eq E2 \in cenc2(void) = false . ceq E2 \in cenc2(M,NW) = true if m2?(M) and not(key(cipher2(M)) = intruder) and E2 = cipher2(M) . ceq E2 \in cenc2(M,NW) = E2 \in cenc2(NW) if not(m2?(M) and not(key(cipher2(M)) = intruder) and E2 = cipher2(M)) . - cenc3 eq E3 \in cenc3(void) = false . ceq E3 \in cenc3(M,NW) = true if m3?(M) and not(key(cipher3(M)) = intruder) and E3 = cipher3(M) . ceq E3 \in cenc3(M,NW) = E3 \in cenc3(NW) if not(m3?(M) and not(key(cipher3(M)) = intruder) and E3 = cipher3(M)) . Modules related to the network are given. Three parameterized modules are used. Module EQTRIV is used as a formal parameter of those three modules. mod* EQTRIV principal-sort Elt { pr(TRIV) op _=_ : Elt Elt -> Bool {comm} } mod! BAG (D :: EQTRIV) principal-sort Bag { [Elt.D < Bag] op void : -> Bag op _,_ : Bag Bag -> Bag {assoc comm id: void} op _\in_ : Elt.D Bag -> Bool var B : Bag vars E1 E2 : Elt.D eq E1 \in void = false . ceq E1 \in (E2,B) = true if E1 = E2 . ceq E1 \in (E2,B) = E1 \in B if not(E1 = E2) . } mod! SET (D :: EQTRIV) principal-sort Set { [Elt.D < Set] op empty : -> Set op __ : Set Set -> Set {assoc comm idem id: empty} op _\in_ : Elt.D Set -> Bool var S : Set vars E1 E2 : Elt.D eq E1 \in empty = false . ceq E1 \in (E2 S) = true if E1 = E2 . ceq E1 \in (E2 S) = E1 \in S if not(E1 = E2) . } mod* COLLECTION(D :: TRIV) principal-sort Collection { [Elt.D < Collection] op _\in_ : Elt.D Collection -> Bool } Module NETWORK defines networks. mod! NETWORK { pr(PRINCIPAL + NONCE) pr(CIPHER1 + CIPHER2 + CIPHER3) pr(BAG(MESSAGE)*{sort Bag -> Network}) pr(COLLECTION(NONCE)*{sort Collection -> ColNonce}) pr(COLLECTION(CIPHER1)*{sort Collection -> ColCipher1}) pr(COLLECTION(CIPHER2)*{sort Collection -> ColCipher2}) pr(COLLECTION(CIPHER3)*{sort Collection -> ColCipher3}) -- op cnonce : Network -> ColNonce op cenc1 : Network -> ColCipher1 op cenc2 : Network -> ColCipher2 op cenc3 : Network -> ColCipher3 -- var NW : Network var M : Message var N : Nonce var E1 : Cipher1 var E2 : Cipher2 var E3 : Cipher3 -- -- cnonce -- eq N \in cnonce(void) = (creator(N) = intruder) . ceq N \in cnonce(M,NW) = true if m1?(M) and key(cipher1(M)) = intruder and nonce(cipher1(M)) = N . ceq N \in cnonce(M,NW) = true if m2?(M) and key(cipher2(M)) = intruder and nonce1(cipher2(M)) = N . ceq N \in cnonce(M,NW) = true if m2?(M) and key(cipher2(M)) = intruder and nonce2(cipher2(M)) = N . ceq N \in cnonce(M,NW) = true if m3?(M) and key(cipher3(M)) = intruder and nonce(cipher3(M)) = N . ceq N \in cnonce(M,NW) = N \in cnonce(NW) if not(m1?(M) and key(cipher1(M)) = intruder and nonce(cipher1(M)) = N) and not(m2?(M) and key(cipher2(M)) = intruder and nonce1(cipher2(M)) = N) and not(m2?(M) and key(cipher2(M)) = intruder and nonce2(cipher2(M)) = N) and not(m3?(M) and key(cipher3(M)) = intruder and nonce(cipher3(M)) = N) . -- -- cenc1 -- eq E1 \in cenc1(void) = false . ceq E1 \in cenc1(M,NW) = true if m1?(M) and not(key(cipher1(M)) = intruder) and E1 = cipher1(M) . ceq E1 \in cenc1(M,NW) = E1 \in cenc1(NW) if not(m1?(M) and not(key(cipher1(M)) = intruder) and E1 = cipher1(M)) . -- -- cenc2 -- eq E2 \in cenc2(void) = false . ceq E2 \in cenc2(M,NW) = true if m2?(M) and not(key(cipher2(M)) = intruder) and E2 = cipher2(M) . ceq E2 \in cenc2(M,NW) = E2 \in cenc2(NW) if not(m2?(M) and not(key(cipher2(M)) = intruder) and E2 = cipher2(M)) . -- -- cenc3 -- eq E3 \in cenc3(void) = false . ceq E3 \in cenc3(M,NW) = true if m3?(M) and not(key(cipher3(M)) = intruder) and E3 = cipher3(M) . ceq E3 \in cenc3(M,NW) = E3 \in cenc3(NW) if not(m3?(M) and not(key(cipher3(M)) = intruder) and E3 = cipher3(M)) . } * Formalizing Trustable Principals Two values are suposed to be observable from the outside of the protocol. - The set of used random numbers - The network Thoese are denoted by the two observation operators. bop ur : System -> URand bop nw : System -> Network Let init denote any initial state of the protocol. eq ur(init) = empty . eq nw(init) = void . The behavior of trustable principals, namely sending the three types of messages, are denoted by the three action operators. bop sdm1 : System Principal Principal Random -> System bop sdm2 : System Principal Random Message -> System bop sdm3 : System Principal Random Message Message -> System - sdm1(s,p,q,r) corresponds to that principal p makes cipher text enc1(q,n(p,q,r),p) and sends it to principal q. - sdm2(s,q,r,m1) corresponds to that if principal q receives Msg1 message m1, enc1(q,n1,p), that seems to have been sent by a principal, say p, then q makes cipher text enc2(p,n1,n(q,p,r),q) and sends it to p. - sdm3(s,p,r,m1,m2) corresponds to that principal p has sent Msg1 message m1, enc1(q,n(p,q,r),p), to a principal, say q, and receives Msg2 message m2, enc2(p,n(p,q,r),n2,q), that seems to have been sent by q, then p makes cipher text enc3(q,n2) and sends it to q. In order for a principal, say p, to receive a message, say m, from a principal, say q, there must exist m that seems to have been sent to p by q in the network. The following conditions have something like that there exists a message in the network instead of that a principal receives a message. Those action operators are defined with equations. - sdm1 op c-sdm1 : System Principal Principal Random -> Bool eq c-sdm1(S,P,Q,R) = not(R \in ur(S)) . -- ceq ur(sdm1(S,P,Q,R)) = R ur(S) if c-sdm1(S,P,Q,R) . ceq nw(sdm1(S,P,Q,R)) = m1(P,P,Q,enc1(Q,n(P,Q,R),P)) , nw(S) if c-sdm1(S,P,Q,R) . ceq sdm1(S,P,Q,R) = S if not c-sdm1(S,P,Q,R) . - sdm2 M : m1(??,P,Q,enc1(Q,N,P)) c-sdm2(S,Q,R,M) = m1(??,P,Q,enc1(Q,N,P)) \in nw(S) and not(R \in ur(S)) op c-sdm2 : System Principal Random Message -> Bool eq c-sdm2(S,Q,R,M) = (M \in nw(S) and m1?(M) and receiver(M) = Q and key(cipher1(M)) = Q and principal(cipher1(M)) = sender(M) and not(R \in ur(S))) . -- ceq ur(sdm2(S,Q,R,M)) = R ur(S) if c-sdm2(S,Q,R,M) . ceq nw(sdm2(S,Q,R,M)) = m2(Q,Q,sender(M),enc2(sender(M),nonce(cipher1(M)),n(Q,sender(M),R),Q)) , nw(S) if c-sdm2(S,Q,R,M) . ceq sdm2(S,Q,R,M) = S if not c-sdm2(S,Q,R,M) . - sdm3 M1: m1(P,P,Q,enc1(Q,n(P,Q,R),P)) M2: m2(??,Q,P,enc2(P,n(P,Q,R),N,Q)) c-sdm3(S,P,R,M1,M2) = m1(P,P,Q,enc1(Q,n(P,Q,R),P)) \in nw(S) and m2(??,Q,P,enc2(P,n(P,Q,R),N,Q)) \in nw(S) op c-sdm3 : System Principal Random Message Message -> Bool eq c-sdm3(S,P,R,M1,M2) = (M1 \in nw(S) and M2 \in nw(S) and m1?(M1) and m2?(M2) and creator(M1) = P and sender(M1) = P and receiver(M1) = sender(M2) and key(cipher1(M1)) = sender(M2) and nonce(cipher1(M1)) = n(P,sender(M2),R) and principal(cipher1(M1)) = P and receiver(M2) = P and key(cipher2(M2)) = P and nonce1(cipher2(M2)) = n(P,sender(M2),R) and principal(cipher2(M2)) = sender(M2)) . -- eq ur(sdm3(S,P,R,M1,M2)) = ur(S) . ceq nw(sdm3(S,P,R,M1,M2)) = m3(P,P,sender(M2),enc3(sender(M2),nonce2(cipher2(M2)))) , nw(S) if c-sdm3(S,P,R,M1,M2) . ceq sdm3(S,P,R,M1,M2) = S if not c-sdm3(S,P,R,M1,M2) . * Formalizing the Intruder Part of the intruder has been modeled as the network; what information gleaned by the intruder from the network has been defined. What messages faked by the intruder based on the gleaned info will be defined. For each type of messages, - Messages are faked based on gleaned nonces, and - Messages are faked based on gleaned cipher texts, Each of which is denoted by one action operators. Therefore, the intruder's faking messages are denoted by the six action operators. bop fkm11 : System Principal Principal Cipher1 -> System bop fkm12 : System Principal Principal Nonce -> System bop fkm21 : System Principal Principal Cipher2 -> System bop fkm22 : System Principal Principal Nonce Nonce -> System bop fkm31 : System Principal Principal Cipher3 -> System bop fkm32 : System Principal Principal Nonce -> System - fkm11(s,p,q,c1) corresponds to that the intruder fakes message m1(intruder,p,q,c1) and put it into the network. - fkm12(s,p,q,n) corresponds to that the intruder fakes message m1(intruder,p,q,enc1(q,n,p)) and put it into the network. - You can imagine what the remaining operators correspond to. Those action operators are defined with equations. - fkm11 op c-fkm11 : System Principal Principal Cipher1 -> Bool eq c-fkm11(S,P,Q,E1) = E1 \in cenc1(nw(S)) . -- eq ur(fkm11(S,P,Q,E1)) = ur(S) . ceq nw(fkm11(S,P,Q,E1)) = m1(intruder,P,Q,E1) , nw(S) if c-fkm11(S,P,Q,E1) . ceq fkm11(S,P,Q,E1) = S if not c-fkm11(S,P,Q,E1) . - fkm12 op c-fkm12 : System Principal Principal Nonce -> Bool eq c-fkm12(S,P,Q,N) = N \in cnonce(nw(S)) . -- eq ur(fkm12(S,P,Q,N)) = ur(S) . ceq nw(fkm12(S,P,Q,N)) = m1(intruder,P,Q,enc1(Q,N,P)) , nw(S) if c-fkm12(S,P,Q,N) . ceq fkm12(S,P,Q,N) = S if not c-fkm12(S,P,Q,N) . You can imgine how to define the remaining action operators with equations. Module NSLPK is given. mod* NSLPK { pr(NETWORK) pr(SET(RANDOM)*{sort Set -> URand}) *[System]* -- any initial state op init : -> System -- observations bop ur : System -> URand bop nw : System -> Network -- actions -- sending messages according to the protocol bop sdm1 : System Principal Principal Random -> System bop sdm2 : System Principal Random Message -> System bop sdm3 : System Principal Random Message Message -> System -- faking messages based on the gleaned info bop fkm11 : System Principal Principal Cipher1 -> System bop fkm12 : System Principal Principal Nonce -> System bop fkm21 : System Principal Principal Cipher2 -> System bop fkm22 : System Principal Principal Nonce Nonce -> System bop fkm31 : System Principal Principal Cipher3 -> System bop fkm32 : System Principal Principal Nonce -> System -- CafeOBJ variables var S : System vars M M1 M2 : Message vars P Q : Principal var R : Random vars N N1 N2 : Nonce var E1 : Cipher1 var E2 : Cipher2 var E3 : Cipher3 -- for any initial state eq ur(init) = empty . eq nw(init) = void . -- for sdm1 op c-sdm1 : System Principal Principal Random -> Bool eq c-sdm1(S,P,Q,R) = not(R \in ur(S)) . -- ceq ur(sdm1(S,P,Q,R)) = R ur(S) if c-sdm1(S,P,Q,R) . ceq nw(sdm1(S,P,Q,R)) = m1(P,P,Q,enc1(Q,n(P,Q,R),P)) , nw(S) if c-sdm1(S,P,Q,R) . ceq sdm1(S,P,Q,R) = S if not c-sdm1(S,P,Q,R) . -- for sdm2 op c-sdm2 : System Principal Random Message -> Bool eq c-sdm2(S,Q,R,M) = (M \in nw(S) and m1?(M) and receiver(M) = Q and key(cipher1(M)) = Q and principal(cipher1(M)) = sender(M) and not(R \in ur(S))) . -- ceq ur(sdm2(S,Q,R,M)) = R ur(S) if c-sdm2(S,Q,R,M) . ceq nw(sdm2(S,Q,R,M)) = m2(Q,Q,sender(M),enc2(sender(M),nonce(cipher1(M)),n(Q,sender(M),R),Q)) , nw(S) if c-sdm2(S,Q,R,M) . ceq sdm2(S,Q,R,M) = S if not c-sdm2(S,Q,R,M) . -- for sdm3 op c-sdm3 : System Principal Random Message Message -> Bool eq c-sdm3(S,P,R,M1,M2) = (M1 \in nw(S) and M2 \in nw(S) and m1?(M1) and m2?(M2) and creator(M1) = P and sender(M1) = P and receiver(M1) = sender(M2) and key(cipher1(M1)) = sender(M2) and nonce(cipher1(M1)) = n(P,sender(M2),R) and principal(cipher1(M1)) = P and receiver(M2) = P and key(cipher2(M2)) = P and nonce1(cipher2(M2)) = n(P,sender(M2),R) and principal(cipher2(M2)) = sender(M2)) . -- eq ur(sdm3(S,P,R,M1,M2)) = ur(S) . ceq nw(sdm3(S,P,R,M1,M2)) = m3(P,P,sender(M2),enc3(sender(M2),nonce2(cipher2(M2)))) , nw(S) if c-sdm3(S,P,R,M1,M2) . ceq sdm3(S,P,R,M1,M2) = S if not c-sdm3(S,P,R,M1,M2) . -- for fkm11 op c-fkm11 : System Principal Principal Cipher1 -> Bool eq c-fkm11(S,P,Q,E1) = E1 \in cenc1(nw(S)) . -- eq ur(fkm11(S,P,Q,E1)) = ur(S) . ceq nw(fkm11(S,P,Q,E1)) = m1(intruder,P,Q,E1) , nw(S) if c-fkm11(S,P,Q,E1) . ceq fkm11(S,P,Q,E1) = S if not c-fkm11(S,P,Q,E1) . -- for fkm12 op c-fkm12 : System Principal Principal Nonce -> Bool eq c-fkm12(S,P,Q,N) = N \in cnonce(nw(S)) . -- eq ur(fkm12(S,P,Q,N)) = ur(S) . ceq nw(fkm12(S,P,Q,N)) = m1(intruder,P,Q,enc1(Q,N,P)) , nw(S) if c-fkm12(S,P,Q,N) . ceq fkm12(S,P,Q,N) = S if not c-fkm12(S,P,Q,N) . -- for fkm21 op c-fkm21 : System Principal Principal Cipher2 -> Bool eq c-fkm21(S,P,Q,E2) = E2 \in cenc2(nw(S)) . -- eq ur(fkm21(S,P,Q,E2)) = ur(S) . ceq nw(fkm21(S,P,Q,E2)) = m2(intruder,P,Q,E2) , nw(S) if c-fkm21(S,P,Q,E2) . ceq fkm21(S,P,Q,E2) = S if not c-fkm21(S,P,Q,E2) . -- for fkm22 op c-fkm22 : System Principal Principal Nonce Nonce -> Bool eq c-fkm22(S,P,Q,N1,N2) = N1 \in cnonce(nw(S)) and N2 \in cnonce(nw(S)) . -- eq ur(fkm22(S,P,Q,N1,N2)) = ur(S) . ceq nw(fkm22(S,P,Q,N1,N2)) = m2(intruder,P,Q,enc2(Q,N1,N2,P)) , nw(S) if c-fkm22(S,P,Q,N1,N2) . ceq fkm22(S,P,Q,N1,N2) = S if not c-fkm22(S,P,Q,N1,N2) . -- for fkm31 op c-fkm31 : System Principal Principal Cipher3 -> Bool eq c-fkm31(S,P,Q,E3) = E3 \in cenc3(nw(S)) . -- eq ur(fkm31(S,P,Q,E3)) = ur(S) . ceq nw(fkm31(S,P,Q,E3)) = m3(intruder,P,Q,E3) , nw(S) if c-fkm31(S,P,Q,E3) . ceq fkm31(S,P,Q,E3) = S if not c-fkm31(S,P,Q,E3) . -- for fkm32 op c-fkm32 : System Principal Principal Nonce -> Bool eq c-fkm32(S,P,Q,N) = N \in cnonce(nw(S)) . -- eq ur(fkm32(S,P,Q,N)) = ur(S) . ceq nw(fkm32(S,P,Q,N)) = m3(intruder,P,Q,enc3(Q,N)) , nw(S) if c-fkm32(S,P,Q,N) . ceq fkm32(S,P,Q,N) = S if not c-fkm32(S,P,Q,N) . } Verification of the NSLPK Authentication Protocol (2) * Introduction Now that we have made a formal model of NSLPK and described in CafeOBJ, we are about to verify that (the model of) NSLPK has desired properties. * Properties to be Verified Let us recall what the protocol achieves. ---------------------- NSLPK ----------------------------------- Msg1 p --> q : enc(q, n_p, p) Msg2 q --> p : enc(p, n_p, n_q, q) Msg3 p --> q : enc(q, n_q) ---------------------------------------------------------------- For each successfully completed run that seems involved by two principals p and q, 1. Two nonces used in the run are never leaked. 2. The two principals p and q have really involved in the run. Property 1 is called nonce secrecy property. Property 2 is called (one-to-many) agreement property. * Formalizing Properties Property 1 is rephrased as follows: 1. The intruder cannot glean any nonces generated by any other principal to authenticate any other principal. E.g. n(p,q,r), where neither p nor q is the intruder, cannot be gleaned by the intruder. In other words, all nonces that the intruder can glean are those generated by the intruder and for the intruder. Therefore, property 1 is formally expressed as follows: 1. For any reachable statet s, any nonce n, n \in cnonce(nw(s)) implies (creator(n) = intruder or forwhom(n) = intruder). Property 2 is rephrased as follows: 2. If a trustable principal p has sent an Msg1 message m1 to a principal q and has recevied an Msg2 message m2 that conforms to the protocol and that seems to have been sent by q in response to m1, then m2 really originates from q, p -- enc(q, n_p, p) --> q p <-- enc(p, n_p, n_q, q) -- ?? <-- ... -- q and if a trustable principal q has sent an Msg1 messaeg m2 to a principal p and has received an Msg3 message m3 that conforms to the protocol and that seems to have been sent by p in response to m2, then m3 really originates from p. p <-- enc(p, n_p, n_q, q) -- q p -- ... --> ?? -- enc(q, n_q) --> q Therefore, property 2 is formally expressed as follows: 2. For any reachable state s, any principals p,q,p1,q1, any nonce n, any random number r, (not(p = intruder) and m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) and m2(q1,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s)) implies m2(q,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s) and (not(q = intruder) and m2(q,q,p,enc2(p,n,n(q,p,r),q)) \in nw(s) and m3(p1,p,q,enc3(q,n(q,p,r))) \in nw(s) implies m3(p,p,q,enc3(q,n(q,p,r))) \in nw(s)). Actually, property 2 is divided into two proerties when verifying it. In order to verify the three properties, 14 more properties are needed. In all, 17 properties are verified. * How to Write Proof Scores of Invariants If a predicate is true in any reachable state of a system, then the predicate is called invariant to the system. All properties to be verified in this seminar are invariants. Let us consider proving that (1) pred1(s,x1) is invariant to a system, where s is a state parameter, and x1 other parameteres. It is often the case that we cannot prove that pred1(s,x1) is invariant by itself. Suppose that it is possible to prove that (2) pred1(s,x1) /\ ... /\ predn(s,xn) is invariant. Let pred(s,x1,...,xn) be predicate (2). Note that you should find pred2(s,x2),...,predn(s,xn) while you are proving that pred1(s,x1) is invariant and the remaining ones are invariant. There are some tips or heuristics to find such lemma-like predicates. Suppose that we prove that pred(s,x1,...,xn) is invariant by induction on the number of action operators (transition rules) applied. Let us consider an inductive case where it is shown that action operator "a" preserves pred(s,x1,...,xn). pred(s,x1,...,xn) ==> pred(a(s,y),x1,...,xn) The proof can be replaced with those of the n formulas. pred1(s,x1) ==> pred1(a(s,y),x1) (3) ... predn(s,xn) ==> predn(a(s,y),xn) Some of (3) cannot be proved as they are, especially the 1st one from the assumption becasue the inductive hypothesis is weak. Let the ith one predi(s,xi) ==> predi(a(s,y),xi) be such a formula. To prove the formula, we should find what strengthens the inductive hypothesis predi(s,xi). SIHi = predj1(s,uj1) /\ ... /\ predjm(s,ujm) where 1 <= j1,...,hm <= n and uj (j = j1,...,jm) is a term (an instance of the correespinding parameter). The proof of the ith formula is replaced with that of the following: (4) (SIHi /\ predi(s,xi)) ==> predi(a(s,y),xi) We may have to split the case into multiple subcases. Suppose that the case is split into l subcases denoted by casei1, ..., caseil which should satisfy (casei1 \/ ... \/ caseil) = true Then, the proof of (4) is replaced with those of the l formulas: (casei1 /\ SIHi /\ predi(s,xi)) ==> predi(a(s,y),xi) (5) ... (caseil /\ SIHi /\ predi(s,xi)) ==> predi(a(s,y),xi) SIHi may not be needed fro some subcases. Note that you should find hot to split the case into multiple subcase while you are proving the corresponding formula. What you have to do first is to split the case into two subcases: one where the (effective) condition of the action operator is true, and the other where it is false. Let us consider writing proof scores of the n invariants. - Operators denoting the n invariants are declared in a module, say INV. op inv1 : H V1 -> Bool ... op invn : H Vn -> Bool eq inv1(W,X1) = pred1(W,X1) . ... eq invn(W,Xn) = predn(W,Xn) . (I) Base case; let init denote any initial state. open INV red invi(init,xi) . close - Predicates to prove in each inductive case are declared in a module, say ISTEP. op istep1 : V1 -> Bool ... op istepn : Vn -> Bool eq istep1(X1) = inv1(s,X1) implies inv1(s',X1) . ... eq istepn(Xn) = invn(s,Xn) implies invn(s',Xn) . These predicates correspond to (3) (2) Inductive case. Let us consider writing proof scores of an inductive case where it is shown that action operator a preserves predi(s,xi) (or invi(s,xi)). open ISTEP -- arbitrary objects op y : -> Y . -- assumptoins eq CASEik = true . -- successor state eq s' = a(s,y) . -- check red SIHi implies istepi(xi) . close SIHi implies (invi(s,Xn) implies invi(a(s,y),Xn)) (SIHi and invi(s,Xn)) implies invi(a(s,y),Xn)) where CASEik corresponds to caseik (1 <= k <= l). caseik is denoted by equatoins, but more than one equation may have to be used. * Modules INV and ISTEP *** See invariants.mod *** * Proof Scores of Nonce Secrecy and One-to-Many Agreemnet *** See proof130.mod *** Nonce Secrecy *** See proof170.mod *** One-to-Many Agreement (1st conjunct) *** See proof180.mod *** One-to-Many Agreement (2nd conjunct) - Some tips on writing proof scores. 1. How to split the case. a. First split the case into two: one where the condition holds, and the other where the condition does not. (See proof130.mod) The former case often needs to be split again. b. Split the case into two based on predicates in the specification such as n = n(p10,q10,r10) and p10 = intruder. (See proof130.mod) To find such predicates, you should understand the formal model of a system under consideration and problems to be solved. Reduced terms may give you some hints on such predicates. 2. How to write equations denoting assumptions. a. Write an equation whose lefthand side is in normal form. (See proof130.mod) b. If an assumption is expressed as P1 /\ ... /\ Pn, then basically write n equations each of which denotes Pi (1 <= i <= n). (See proof130.mod) Basically, eq li = ri . if Pi is li = ri. eq pi = true . if Pi is pi. eq pi = false . if Pi is not(pi). (Effective) conditions of action operators can be in this form. The assumption "m10 \in nw(s)" is denoted by "eq nw(s) = m10 , nw10 ." so that the equations defining cnonce, etc can be effectively used. c. Do not write an equation that makes the lefthand side of another equatoin unnormal. (See proof130.mod) If it is necessary to write such an equation, the lefthand side that has become unnormal should be replaced with the normal one. (See proof170.mod) d. If you have an equation c(a1, ..., an) = c(b1, ..., bn) as an assumption, where c is a data constructor, then you may have to declare the n equations a1 = b1, ..., an = bn instead of the original one. (See proof170.mod) The original equation may be deduced from the n equations with rewriting, but the contrary may not with rewriting. 3. How to find other invariants to strengthen inductive hypotheses. a. Conjecture likely invariants. (You should understand (the model of) the system under consideration to some extent.) (See proof130.mod) When modeling the protocol, the intruder glean only cipher texts that are not encrypted with the intruder's public key. From this, we can conjecture that e1 \in cenc1(nw(s)) implies not(key(e1) = intruder) is invariant. b. Suppose that the case under consideration is unreachable, and conjecture likely invariants. (See proof130.mod) In the example, we suppose that there exists a Msg1 message msg1(??,intruder,p10,enc1(p10,n,intruder)) in the network. From this assumption, we conclude that enc1(p10,n,intruder) \in cenc1(nw(s)) On the other hand, the message must have been sent by the intruder, and then nonce n must be known by the intruder. But, we suppose that the nonce is not available to the intruder. Contradiction! We conjecture that (e1 \in cenc1(nw(s)) and principal(e1) = intruder) implies nonce(e1) \in cnonce(nw(s)) is invariant, which is inv140.