*** Needham-Scroeder Public-Key Athentication Protocol *** Olveczky version ... *** Note, THIS VERSION is minuscully modified---actually, only an additional *** importation of 'full-maude.maude' is removed---version of the 'REAL' *** NSPK example taught in INF220. Keep THAT file as the canonical *** version (~/NYTTKURS/Examples/nspk.maude). (omod OID-SET is sort OidSet . subsort Oid < OidSet . op none : -> OidSet [ctor] . op _;_ : OidSet OidSet -> OidSet [ctor assoc comm id: none] . endom) (omod NSPK is protecting NAT . *** Some data types. *** First, the "nonces". I just define them as different *** from the natural numbers, since they cannot be guessed. *** One may later equate them with appropriate numbers if so desired. sort Nonce . op nonce : Oid Nat -> Nonce [ctor] . *** We need a sort for public keys: sort Key . op pubKey : Oid -> Key [ctor] . *** Messages involved in the specification. *** First we define the content of unencrypted messages: sorts MsgContent EncrMsgContent . op _;_ : Nonce Oid -> MsgContent [ctor] . *** Message kind "1" op _;_ : Nonce Nonce -> MsgContent [ctor] . *** Message kind "2" subsort Nonce < MsgContent . *** Message kind "3" op encrypt_with_ : MsgContent Key -> EncrMsgContent [ctor] . msg msg_from_to_ : EncrMsgContent Oid Oid -> Msg . *** Next, we define the "Initiator" class: class Initiator | initSessions : InitSessions, nonceCtr : Nat . *** initSessions stores information about all the sessions that this *** Initiator could be involved in and their states: sorts Sessions InitSessions . *** State of the sessions for which this object is, *** or could be, the initiator subsort Sessions < InitSessions . op emptySession : -> Sessions [ctor] . op __ : InitSessions InitSessions -> InitSessions [ctor assoc comm id: emptySession] . op __ : Sessions Sessions -> Sessions [ctor assoc comm id: emptySession] . op notInitiated : Oid -> InitSessions [ctor] . *** Not initaited yet a session with this node, but could start one. op initiated : Oid Nonce -> InitSessions [ctor] . *** Have initiated a session with this node, with the given nonce op trustedConnection : Oid -> Sessions [ctor] . *** Have established a trusted connection with the given node. *** Now we define the protocol: vars A B : Oid . vars M N : Nat . vars NONCE NONCE' : Nonce . var IS : InitSessions . rl [start-send-1] : < A : Initiator | initSessions : notInitiated(B) IS, nonceCtr : N > => < A : Initiator | initSessions : initiated(B, nonce(A, N)) IS, nonceCtr : N + 1 > msg (encrypt (nonce(A, N) ; A) with pubKey(B)) from A to B . rl [read-2-send-3] : (msg (encrypt (NONCE ; NONCE') with pubKey(A)) from B to A) < A : Initiator | initSessions : initiated(B, NONCE) IS > => < A : Initiator | initSessions : trustedConnection(B) IS > msg (encrypt NONCE' with pubKey(B)) from A to B . *** Responder: two states: responded and trustedConnection: class Responder | respSessions : RespSessions, nonceCtr : Nat . sort RespSessions . subsort Sessions < RespSessions . op __ : RespSessions RespSessions -> RespSessions [ctor assoc comm id: emptySession] . op responded : Oid Nonce -> RespSessions [ctor] . *** Do we already have a session going for an object: op _inSession_ : Oid RespSessions -> Bool . var RS : RespSessions . eq A inSession emptySession = false . eq A inSession (trustedConnection(B) RS) = (A == B) or (A inSession RS) . eq A inSession (responded(B, NONCE) RS) = (A == B) or (A inSession RS) . *** The rules, first receive message 1, and send message 2: crl [read-1-send-2] : (msg (encrypt (NONCE ; A) with pubKey(B)) from A to B) < B : Responder | respSessions : RS, nonceCtr : N > => < B : Responder | respSessions : responded(A, nonce(B, N)) RS, nonceCtr : N + 1 > msg (encrypt (NONCE ; nonce(B, N)) with pubKey(A)) from B to A if not A inSession RS . *** Finally, the responder receives message 3: rl [read-3] : (msg (encrypt NONCE with pubKey(B)) from A to B) < B : Responder | respSessions : responded(A, NONCE) RS > => < B : Responder | respSessions : trustedConnection(A) RS > . *** Finally, a node may both be initiator and responder: class InitiatorAndResponder . subclass InitiatorAndResponder < Initiator Responder . endom) (omod TEST-NSPK is including NSPK . including STRING . subsort String < Oid . op init : -> Configuration . eq init = < "a" : Initiator | initSessions : notInitiated("b"), nonceCtr : 1 > < "b" : Responder | respSessions : emptySession, nonceCtr : 1 > . op init2 : -> Configuration . eq init2 = < "a" : InitiatorAndResponder | initSessions : notInitiated("c"), respSessions : emptySession, nonceCtr : 1 > < "Bank" : Responder | respSessions : emptySession, nonceCtr : 1 > < "c" : InitiatorAndResponder | initSessions : notInitiated("Bank") notInitiated("a"), respSessions : emptySession, nonceCtr : 1 > . endom) (omod NSPK-INTRUDER is including NSPK . including OID-SET . *** Specifies all the possibilities of a "stupid intruder" *** The intruder must be able to store *** - nonces it has seen *** - encrypted message content it has seen, but could not decrypt *** - names of other agents it has seen vars NONCE NONCE' : Nonce . vars A B I O O' O'' : Oid . var ENCRMSG : EncrMsgContent . var ENCRMSGS : EncrMsgContentSet . var N : Nat . var OS : OidSet . var NSET : NonceSet . var IS : InitSessions . var RS : RespSessions . var MSGC : MsgContent . *** Set of nonces seen: sort NonceSet . subsort Nonce < NonceSet . op emptyNonceSet : -> NonceSet [ctor] . op __ : NonceSet NonceSet -> NonceSet [ctor assoc comm id: emptyNonceSet] . eq NONCE NONCE = NONCE . *** Set of encrypted messages seen: sort EncrMsgContentSet . subsort EncrMsgContent < EncrMsgContentSet . op emptyEncrMsg : -> EncrMsgContentSet [ctor] . op __ : EncrMsgContentSet EncrMsgContentSet -> EncrMsgContentSet [ctor assoc comm id: emptyEncrMsg] . eq ENCRMSG ENCRMSG = ENCRMSG . *** Set of agents seen is an OidSet, which is really a multiset, *** so we add the following axiom: eq O ; O = O . *** The intruder has the capabilities of a initiator and responder, *** and can in addition do all kinds of strange message sending: class Intruder | initSessions : InitSessions, respSessions : RespSessions, nonceCtr : Nat, agentsSeen : OidSet, noncesSeen : NonceSet, encrMsgsSeen : EncrMsgContentSet . *** The usual protocol roles. Strictly speaking, the intruder *** does not have to have these rules, since they are subsumed *** in its "wild" message sending. However, to make it slightly more *** realistic we add that as an explicit policy: rl [I-send-1] : < I : Intruder | initSessions : notInitiated(B) IS, nonceCtr : N, agentsSeen : OS, noncesSeen : NSET > => < I : Intruder | initSessions : initiated(B, nonce(I, N)) IS, nonceCtr : N + 1, agentsSeen : OS ; B, noncesSeen : nonce(I, N) NSET > (msg (encrypt (nonce(I, N) ; I) with pubKey(B)) from I to B) . crl [I-rcv-1] : (msg (encrypt (NONCE ; A) with pubKey(I)) from A to I) < I : Intruder | respSessions : RS, nonceCtr : N, agentsSeen : OS, noncesSeen : NSET > => < I : Intruder | respSessions : responded(A, nonce(I, N)) RS, nonceCtr : N + 1, agentsSeen : OS ; A, noncesSeen : NSET NONCE nonce(I, N) > (msg (encrypt (NONCE ; nonce(I, N)) with pubKey(A)) from I to A) if not A inSession RS . rl [I-rcv-2] : (msg (encrypt (NONCE ; NONCE') with pubKey(I)) from B to I) < I : Intruder | initSessions : initiated(B, NONCE) IS, noncesSeen : NSET > => < I : Intruder | initSessions : trustedConnection(B) IS, noncesSeen : NSET NONCE' > (msg (encrypt NONCE' with pubKey(B)) from I to B) . rl [I-rcv-3] : (msg (encrypt NONCE with pubKey(I)) from A to I) < I : Intruder | respSessions : responded(A, NONCE) IS > => < I : Intruder | respSessions : trustedConnection(A) IS > . *** Now, we model the less pleasant capabilities of the intruder. *** The intruder may overhear messages passed around in the system. *** We get a lot of cases here, depending on whether *** the agent can read the message or not. *** We first state the cases where the intruder can overhear *** a message he cannot understand: *** It may be tempting to check also whether the sender *** of the messages overheard is different from the intruder. *** Obviously, an intruder does not need to intercept a message *** he sent himself. This is clearly a tempting restriction *** since it may reduce the search space. However, to get a most *** general intruder, it may intercept or overhear messages ostensibly *** sent by itself. This is because it could have been a message *** faked by another intruder, so that this intruder could actually learn *** something from that message! This restriction can be added *** if there can only be one intruder! crl [overhear-but-not-understand] : (msg (encrypt MSGC with pubKey(O)) from O' to O) < I : Intruder | agentsSeen : OS, encrMsgsSeen : ENCRMSGS > => < I : Intruder | agentsSeen : OS ; O ; O', encrMsgsSeen : (encrypt MSGC with pubKey(O)) ENCRMSGS > (msg (encrypt MSGC with pubKey(O)) from O' to O) if O =/= I . crl [intercept-but-not-understand] : (msg (encrypt MSGC with pubKey(O)) from O' to O) < I : Intruder | agentsSeen : OS, encrMsgsSeen : ENCRMSGS > => < I : Intruder | agentsSeen : OS ; O ; O', encrMsgsSeen : (encrypt MSGC with pubKey(O)) ENCRMSGS > if O =/= I . *** We may strictly speaking be done with storing stuff. However, *** for extreme caution, in case there are other guys around, *** may store messages which are encrypted with I's key ... *** May skip these rules if the state space becomes too big! rl [intercept-msg1-and-understand] : (msg (encrypt (NONCE ; A) with pubKey(I)) from O to I) < I : Intruder | agentsSeen : OS, noncesSeen : NSET > => < I : Intruder | agentsSeen : OS ; O ; A, noncesSeen : NSET NONCE > . rl [intercept-msg2-and-understand] : (msg (encrypt (NONCE ; NONCE') with pubKey(I)) from O to I) < I : Intruder | agentsSeen : OS, noncesSeen : NSET > => < I : Intruder | agentsSeen : OS ; O, noncesSeen : NSET NONCE NONCE' > . rl [intercept-msg3-and-understand] : (msg (encrypt NONCE with pubKey(I)) from O to I) < I : Intruder | agentsSeen : OS, noncesSeen : NSET > => < I : Intruder | agentsSeen : OS ; O, noncesSeen : NSET NONCE > . *** And now, the fun part! The sending of messages *** into the wild ocean! *** First, it sends messages it could not read out to *** arbitrary receives "from arbitrary sender". ***( This is the most general in case the intruder does not know with which key a message has been encrypted. However, that he could store when intercepting the message since the intended receiver was given in plaintext crl [send-encrypted] : < I : Intruder | encrMsgsSeen : ENCRMSG ENCRMSGS, agentsSeen : A ; B ; OS > => < I : Intruder | > (msg ENCRMSG from A to B) if A =/= B /\ B =/= I . so we instead use the following rule: )*** crl [send-encrypted] : < I : Intruder | encrMsgsSeen : (encrypt MSGC with pubKey(B)) ENCRMSGS, agentsSeen : A ; OS > => < I : Intruder | > (msg (encrypt MSGC with pubKey(B)) from A to B) if A =/= B /\ B =/= I . *** Now, we send stuff whose contents we know. Clearly, the contents *** must be encrypted with the recipient's key: crl [send-1-fake] : < I : Intruder | agentsSeen : A ; B ; OS, noncesSeen : NONCE NSET > => < I : Intruder | > (msg (encrypt (NONCE ; A) with pubKey(B)) from A to B) if A =/= B /\ B =/= I . crl [send-2-fake] : < I : Intruder | agentsSeen : A ; B ; OS, noncesSeen : NONCE NONCE' NSET > => < I : Intruder | > (msg (encrypt (NONCE ; NONCE') with pubKey(A)) from B to A) if A =/= B /\ A =/= I . crl [send-3-fake] : < I : Intruder | agentsSeen : A ; B ; OS, noncesSeen : NONCE NSET > => < I : Intruder | > (msg (encrypt NONCE with pubKey(B)) from A to B) if A =/= B /\ B =/= I . endom) (omod TEST-INTRUSION is including NSPK-INTRUDER . including STRING . subsort String < Oid . --- two fake messages should be just one: eq M:Msg M:Msg = M:Msg . op intruderInit : -> Configuration . eq intruderInit = < "Peter" : Initiator | initSessions : notInitiated("Walker"), nonceCtr : 1 > < "Bank" : Responder | respSessions : emptySession, nonceCtr : 1 > < "Walker" : Intruder | initSessions : notInitiated("Bank"), respSessions : emptySession, nonceCtr : 1, agentsSeen : "Bank" ; "Walker", noncesSeen : emptyNonceSet, encrMsgsSeen : emptyEncrMsg > . endom) ***( To write core Maude content to file and quit: (show all .) q )*** ***( This is the search we really wanted, but takes too long: (search [1] intruderInit =>* C:Configuration < "Bank" : Responder | respSessions : trustedConnection("Peter") RS:RespSessions, ATTS:AttributeSet > .) )*** --- *** However, we just managed to split the search in two: ***( (search [1] intruderInit =>* C:Configuration < "Bank" : Responder | respSessions : responded("Peter", N:Nonce) RS:RespSessions, ATTS:AttributeSet > .) (search [1] < "Walker" : Intruder | nonceCtr : 1, initSessions : notInitiated("Bank"), respSessions : emptySession, encrMsgsSeen : emptyEncrMsg, noncesSeen : nonce("Peter", 1), agentsSeen : ("Bank" ; "Peter" ; "Walker") > < "Peter" : Initiator | nonceCtr : 2, initSessions : initiated("Walker", nonce("Peter",1)) > (msg encrypt nonce("Peter",1); nonce("Bank",1) with pubKey("Peter") from "Bank" to "Peter") < "Bank" : Responder | respSessions : responded("Peter", nonce("Bank", 1)), nonceCtr : 2 > =>* C:Configuration < "Bank" : Responder | respSessions : trustedConnection("Peter") RS:RespSessions, ATTS:AttributeSet > .) )***