(herald "Second approx to TLS: First get cert, then send pms encrypted.") (comment "CPSA 2.2.11") (comment "All input read from tls1.scm") (defprotocol tls1 basic (defrole client (vars (pre_master_secret skey) (server_key akey) (ca server_name name)) (trace (recv (cat server_name server_key (enc (enc "hash_zero" (cat "cert" server_name server_key)) (privk ca)))) (send (enc "client_version" pre_master_secret server_key))) (non-orig (privk ca))) (defrole server (vars (pre_master_secret skey) (server_key akey)) (trace (recv (enc "client_version" pre_master_secret server_key)))) (defrole certificate_auth (vars (subject_name ca name)) (trace (send (cat subject_name (pubk subject_name) (enc (enc "hash_zero" (cat "cert" subject_name (pubk subject_name))) (privk ca))))))) (defskeleton tls1 (vars (ca s name) (pms skey) (k akey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key k)) (deflistener pms) (non-orig (invk k) (privk ca)) (uniq-orig pms) (comment "Confidentiality should be OK.") (traces ((recv (cat s k (enc (enc "hash_zero" (cat "cert" s k)) (privk ca)))) (send (enc "client_version" pms k))) ((recv pms) (send pms))) (label 0) (unrealized (0 0) (1 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton tls1 (vars (ca s name) (pms skey) (k akey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key k)) (deflistener pms) (precedes ((0 1) (1 0))) (non-orig (invk k) (privk ca)) (uniq-orig pms) (traces ((recv (cat s k (enc (enc "hash_zero" (cat "cert" s k)) (privk ca)))) (send (enc "client_version" pms k))) ((recv pms) (send pms))) (label 1) (parent 0) (unrealized (0 0) (1 0)) (origs (pms (0 1))) (comment "empty cohort")) (comment "Nothing left to do") (defprotocol tls1 basic (defrole client (vars (pre_master_secret skey) (server_key akey) (ca server_name name)) (trace (recv (cat server_name server_key (enc (enc "hash_zero" (cat "cert" server_name server_key)) (privk ca)))) (send (enc "client_version" pre_master_secret server_key))) (non-orig (privk ca))) (defrole server (vars (pre_master_secret skey) (server_key akey)) (trace (recv (enc "client_version" pre_master_secret server_key)))) (defrole certificate_auth (vars (subject_name ca name)) (trace (send (cat subject_name (pubk subject_name) (enc (enc "hash_zero" (cat "cert" subject_name (pubk subject_name))) (privk ca))))))) (defskeleton tls1 (vars (ca s name) (pms skey) (k akey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key k)) (non-orig (invk k) (privk ca)) (uniq-orig pms) (comment "Authenticates CA.") (traces ((recv (cat s k (enc (enc "hash_zero" (cat "cert" s k)) (privk ca)))) (send (enc "client_version" pms k)))) (label 2) (unrealized (0 0)) (origs (pms (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton tls1 (vars (ca s name) (pms skey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key (pubk s))) (defstrand certificate_auth 1 (subject_name s) (ca ca)) (precedes ((1 0) (0 0))) (non-orig (privk ca) (privk s)) (uniq-orig pms) (operation encryption-test (added-strand certificate_auth 1) (enc (enc "hash_zero" (cat "cert" s (pubk s))) (privk ca)) (0 0)) (traces ((recv (cat s (pubk s) (enc (enc "hash_zero" (cat "cert" s (pubk s))) (privk ca)))) (send (enc "client_version" pms (pubk s)))) ((send (cat s (pubk s) (enc (enc "hash_zero" (cat "cert" s (pubk s))) (privk ca)))))) (label 3) (parent 2) (unrealized) (shape) (maps ((0) ((pms pms) (k (pubk s)) (ca ca) (s s)))) (origs (pms (0 1)))) (comment "Nothing left to do") (defprotocol tls1 basic (defrole client (vars (pre_master_secret skey) (server_key akey) (ca server_name name)) (trace (recv (cat server_name server_key (enc (enc "hash_zero" (cat "cert" server_name server_key)) (privk ca)))) (send (enc "client_version" pre_master_secret server_key))) (non-orig (privk ca))) (defrole server (vars (pre_master_secret skey) (server_key akey)) (trace (recv (enc "client_version" pre_master_secret server_key)))) (defrole certificate_auth (vars (subject_name ca name)) (trace (send (cat subject_name (pubk subject_name) (enc (enc "hash_zero" (cat "cert" subject_name (pubk subject_name))) (privk ca))))))) (defskeleton tls1 (vars (ca s name) (pms skey) (k server_key akey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key k)) (defstrand server 1 (pre_master_secret pms) (server_key server_key)) (non-orig (invk k) (privk ca)) (uniq-orig pms) (comment "Authenticates CA and implicit auth for server.") (traces ((recv (cat s k (enc (enc "hash_zero" (cat "cert" s k)) (privk ca)))) (send (enc "client_version" pms k))) ((recv (enc "client_version" pms server_key)))) (label 4) (unrealized (0 0) (1 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton tls1 (vars (ca s name) (pms skey) (k server_key akey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key k)) (defstrand server 1 (pre_master_secret pms) (server_key server_key)) (precedes ((0 1) (1 0))) (non-orig (invk k) (privk ca)) (uniq-orig pms) (traces ((recv (cat s k (enc (enc "hash_zero" (cat "cert" s k)) (privk ca)))) (send (enc "client_version" pms k))) ((recv (enc "client_version" pms server_key)))) (label 5) (parent 4) (unrealized (0 0) (1 0)) (origs (pms (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton tls1 (vars (ca s name) (pms skey) (k akey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key k)) (defstrand server 1 (pre_master_secret pms) (server_key k)) (precedes ((0 1) (1 0))) (non-orig (invk k) (privk ca)) (uniq-orig pms) (operation nonce-test (contracted (server_key k)) pms (1 0) (enc "client_version" pms k)) (traces ((recv (cat s k (enc (enc "hash_zero" (cat "cert" s k)) (privk ca)))) (send (enc "client_version" pms k))) ((recv (enc "client_version" pms k)))) (label 6) (parent 5) (unrealized (0 0)) (origs (pms (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton tls1 (vars (ca s name) (pms skey)) (defstrand client 2 (ca ca) (server_name s) (pre_master_secret pms) (server_key (pubk s))) (defstrand server 1 (pre_master_secret pms) (server_key (pubk s))) (defstrand certificate_auth 1 (subject_name s) (ca ca)) (precedes ((0 1) (1 0)) ((2 0) (0 0))) (non-orig (privk ca) (privk s)) (uniq-orig pms) (operation encryption-test (added-strand certificate_auth 1) (enc (enc "hash_zero" (cat "cert" s (pubk s))) (privk ca)) (0 0)) (traces ((recv (cat s (pubk s) (enc (enc "hash_zero" (cat "cert" s (pubk s))) (privk ca)))) (send (enc "client_version" pms (pubk s)))) ((recv (enc "client_version" pms (pubk s)))) ((send (cat s (pubk s) (enc (enc "hash_zero" (cat "cert" s (pubk s))) (privk ca)))))) (label 7) (parent 6) (unrealized) (shape) (maps ((0 1) ((pms pms) (k (pubk s)) (ca ca) (s s) (server_key (pubk s))))) (origs (pms (0 1)))) (comment "Nothing left to do") (defprotocol tls1 basic (defrole client (vars (pre_master_secret skey) (server_key akey) (ca server_name name)) (trace (recv (cat server_name server_key (enc (enc "hash_zero" (cat "cert" server_name server_key)) (privk ca)))) (send (enc "client_version" pre_master_secret server_key))) (non-orig (privk ca))) (defrole server (vars (pre_master_secret skey) (server_key akey)) (trace (recv (enc "client_version" pre_master_secret server_key)))) (defrole certificate_auth (vars (subject_name ca name)) (trace (send (cat subject_name (pubk subject_name) (enc (enc "hash_zero" (cat "cert" subject_name (pubk subject_name))) (privk ca))))))) (defskeleton tls1 (vars (pms skey) (k akey)) (defstrand server 1 (pre_master_secret pms) (server_key k)) (deflistener pms) (non-orig (invk k)) (uniq-orig pms) (comment "Neither confidentiality nor authentication guarantees to server") (traces ((recv (enc "client_version" pms k))) ((recv pms) (send pms))) (label 8) (unrealized) (shape) (maps ((0 1) ((pms pms) (k k)))) (origs)) (comment "Nothing left to do")