TEXT   10

an ssl

Guest on 23rd June 2022 02:41:38 AM

  1. (herald "Old SSL version discussed by Abadi-Needham.")
  2.  
  3. (comment "CPSA 2.2.11")
  4. (comment "All input read from an_ssl.scm")
  5.  
  6. (defprotocol an_ssl basic
  7.   (defrole init
  8.     (vars (client server name) (k skey) (cert nb text))
  9.     (trace (send (enc k (pubk server))) (recv (enc nb k))
  10.       (send (enc cert (enc nb (privk client)) k))))
  11.   (defrole resp
  12.     (vars (client server name) (k skey) (cert nb text))
  13.     (trace (recv (enc k (pubk server))) (send (enc nb k))
  14.       (recv (enc cert (enc nb (privk client)) k)))))
  15.  
  16. (defskeleton an_ssl
  17.   (vars (nb cert text) (a b name) (k skey))
  18.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  19.   (non-orig (privk a) (privk b))
  20.   (uniq-orig nb k)
  21.   (traces
  22.     ((recv (enc k (pubk b))) (send (enc nb k))
  23.       (recv (enc cert (enc nb (privk a)) k))))
  24.   (label 0)
  25.   (unrealized (0 2))
  26.   (origs (nb (0 1)))
  27.   (comment "1 in cohort - 1 not yet seen"))
  28.  
  29. (defskeleton an_ssl
  30.   (vars (nb cert cert-0 text) (a b server name) (k k-0 skey))
  31.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  32.   (defstrand init 3 (cert cert-0) (nb nb) (client a) (server server)
  33.     (k k-0))
  34.   (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  35.   (non-orig (privk a) (privk b))
  36.   (uniq-orig nb k)
  37.   (operation encryption-test (added-strand init 3) (enc nb (privk a))
  38.     (0 2))
  39.   (traces
  40.     ((recv (enc k (pubk b))) (send (enc nb k))
  41.       (recv (enc cert (enc nb (privk a)) k)))
  42.     ((send (enc k-0 (pubk server))) (recv (enc nb k-0))
  43.       (send (enc cert-0 (enc nb (privk a)) k-0))))
  44.   (label 1)
  45.   (parent 0)
  46.   (unrealized)
  47.   (shape)
  48.   (maps ((0) ((a a) (b b) (k k) (nb nb) (cert cert))))
  49.   (origs (nb (0 1))))
  50.  
  51. (comment "Nothing left to do")
  52.  
  53. (defprotocol an_ssl_revised basic
  54.   (defrole init
  55.     (vars (client server name) (k skey) (cert nb text))
  56.     (trace (send (enc k (pubk server))) (recv (enc nb k))
  57.       (send (enc cert (enc client server k nb (privk client)) k))))
  58.   (defrole resp
  59.     (vars (client server name) (k skey) (cert nb text))
  60.     (trace (recv (enc k (pubk server))) (send (enc nb k))
  61.       (recv (enc cert (enc client server k nb (privk client)) k)))))
  62.  
  63. (defskeleton an_ssl_revised
  64.   (vars (nb cert text) (a b name) (k skey))
  65.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  66.   (non-orig (privk a) (privk b))
  67.   (uniq-orig nb k)
  68.   (traces
  69.     ((recv (enc k (pubk b))) (send (enc nb k))
  70.       (recv (enc cert (enc a b k nb (privk a)) k))))
  71.   (label 2)
  72.   (unrealized (0 2))
  73.   (origs (nb (0 1)))
  74.   (comment "1 in cohort - 1 not yet seen"))
  75.  
  76. (defskeleton an_ssl_revised
  77.   (vars (nb cert cert-0 text) (a b name) (k skey))
  78.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  79.   (defstrand init 3 (cert cert-0) (nb nb) (client a) (server b) (k k))
  80.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  81.   (non-orig (privk a) (privk b))
  82.   (uniq-orig nb k)
  83.   (operation encryption-test (added-strand init 3)
  84.     (enc a b k nb (privk a)) (0 2))
  85.   (traces
  86.     ((recv (enc k (pubk b))) (send (enc nb k))
  87.       (recv (enc cert (enc a b k nb (privk a)) k)))
  88.     ((send (enc k (pubk b))) (recv (enc nb k))
  89.       (send (enc cert-0 (enc a b k nb (privk a)) k))))
  90.   (label 3)
  91.   (parent 2)
  92.   (unrealized (0 2))
  93.   (comment "2 in cohort - 2 not yet seen"))
  94.  
  95. (defskeleton an_ssl_revised
  96.   (vars (nb cert text) (a b name) (k skey))
  97.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  98.   (defstrand init 3 (cert cert) (nb nb) (client a) (server b) (k k))
  99.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  100.   (non-orig (privk a) (privk b))
  101.   (uniq-orig nb k)
  102.   (operation encryption-test (displaced 2 1 init 3)
  103.     (enc cert-0 (enc a b k nb (privk a)) k) (0 2))
  104.   (traces
  105.     ((recv (enc k (pubk b))) (send (enc nb k))
  106.       (recv (enc cert (enc a b k nb (privk a)) k)))
  107.     ((send (enc k (pubk b))) (recv (enc nb k))
  108.       (send (enc cert (enc a b k nb (privk a)) k))))
  109.   (label 4)
  110.   (parent 3)
  111.   (unrealized)
  112.   (shape)
  113.   (maps ((0) ((a a) (b b) (k k) (nb nb) (cert cert))))
  114.   (origs (k (1 0)) (nb (0 1))))
  115.  
  116. (defskeleton an_ssl_revised
  117.   (vars (nb cert cert-0 text) (a b name) (k skey))
  118.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  119.   (defstrand init 3 (cert cert-0) (nb nb) (client a) (server b) (k k))
  120.   (deflistener k)
  121.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((1 2) (0 2))
  122.     ((2 1) (0 2)))
  123.   (non-orig (privk a) (privk b))
  124.   (uniq-orig nb k)
  125.   (operation encryption-test (added-listener k)
  126.     (enc cert (enc a b k nb (privk a)) k) (0 2))
  127.   (traces
  128.     ((recv (enc k (pubk b))) (send (enc nb k))
  129.       (recv (enc cert (enc a b k nb (privk a)) k)))
  130.     ((send (enc k (pubk b))) (recv (enc nb k))
  131.       (send (enc cert-0 (enc a b k nb (privk a)) k)))
  132.     ((recv k) (send k)))
  133.   (label 5)
  134.   (parent 3)
  135.   (unrealized (2 0))
  136.   (comment "1 in cohort - 1 not yet seen"))
  137.  
  138. (defskeleton an_ssl_revised
  139.   (vars (nb cert cert-0 text) (a b name) (k skey))
  140.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  141.   (defstrand init 3 (cert cert-0) (nb nb) (client a) (server b) (k k))
  142.   (deflistener k)
  143.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (2 0)) ((2 1) (0 2)))
  144.   (non-orig (privk a) (privk b))
  145.   (uniq-orig nb k)
  146.   (operation nonce-test (displaced 3 1 init 3) k (2 0) (enc k (pubk b)))
  147.   (traces
  148.     ((recv (enc k (pubk b))) (send (enc nb k))
  149.       (recv (enc cert (enc a b k nb (privk a)) k)))
  150.     ((send (enc k (pubk b))) (recv (enc nb k))
  151.       (send (enc cert-0 (enc a b k nb (privk a)) k)))
  152.     ((recv k) (send k)))
  153.   (label 6)
  154.   (parent 5)
  155.   (unrealized (2 0))
  156.   (comment "empty cohort"))
  157.  
  158. (comment "Nothing left to do")

Raw Paste


Login or Register to edit or fork this paste. It's free.