TEXT   17

an ssl shapes

Guest on 23rd June 2022 02:42:15 AM

  1. (comment "CPSA 2.2.11")
  2. (comment "Extracted shapes")
  3.  
  4. (herald "Old SSL version discussed by Abadi-Needham.")
  5.  
  6. (comment "CPSA 2.2.11")
  7.  
  8. (comment "All input read from an_ssl.scm")
  9.  
  10. (defprotocol an_ssl basic
  11.   (defrole init
  12.     (vars (client server name) (k skey) (cert nb text))
  13.     (trace (send (enc k (pubk server))) (recv (enc nb k))
  14.       (send (enc cert (enc nb (privk client)) k))))
  15.   (defrole resp
  16.     (vars (client server name) (k skey) (cert nb text))
  17.     (trace (recv (enc k (pubk server))) (send (enc nb k))
  18.       (recv (enc cert (enc nb (privk client)) k)))))
  19.  
  20. (defskeleton an_ssl
  21.   (vars (nb cert text) (a b name) (k skey))
  22.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  23.   (non-orig (privk a) (privk b))
  24.   (uniq-orig nb k)
  25.   (traces
  26.     ((recv (enc k (pubk b))) (send (enc nb k))
  27.       (recv (enc cert (enc nb (privk a)) k))))
  28.   (label 0)
  29.   (unrealized (0 2))
  30.   (origs (nb (0 1)))
  31.   (comment "1 in cohort - 1 not yet seen"))
  32.  
  33. (defskeleton an_ssl
  34.   (vars (nb cert cert-0 text) (a b server name) (k k-0 skey))
  35.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  36.   (defstrand init 3 (cert cert-0) (nb nb) (client a) (server server)
  37.     (k k-0))
  38.   (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  39.   (non-orig (privk a) (privk b))
  40.   (uniq-orig nb k)
  41.   (operation encryption-test (added-strand init 3) (enc nb (privk a))
  42.     (0 2))
  43.   (traces
  44.     ((recv (enc k (pubk b))) (send (enc nb k))
  45.       (recv (enc cert (enc nb (privk a)) k)))
  46.     ((send (enc k-0 (pubk server))) (recv (enc nb k-0))
  47.       (send (enc cert-0 (enc nb (privk a)) k-0))))
  48.   (label 1)
  49.   (parent 0)
  50.   (unrealized)
  51.   (shape)
  52.   (maps ((0) ((a a) (b b) (k k) (nb nb) (cert cert))))
  53.   (origs (nb (0 1))))
  54.  
  55. (comment "Nothing left to do")
  56.  
  57. (defprotocol an_ssl_revised basic
  58.   (defrole init
  59.     (vars (client server name) (k skey) (cert nb text))
  60.     (trace (send (enc k (pubk server))) (recv (enc nb k))
  61.       (send (enc cert (enc client server k nb (privk client)) k))))
  62.   (defrole resp
  63.     (vars (client server name) (k skey) (cert nb text))
  64.     (trace (recv (enc k (pubk server))) (send (enc nb k))
  65.       (recv (enc cert (enc client server k nb (privk client)) k)))))
  66.  
  67. (defskeleton an_ssl_revised
  68.   (vars (nb cert text) (a b name) (k skey))
  69.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  70.   (non-orig (privk a) (privk b))
  71.   (uniq-orig nb k)
  72.   (traces
  73.     ((recv (enc k (pubk b))) (send (enc nb k))
  74.       (recv (enc cert (enc a b k nb (privk a)) k))))
  75.   (label 2)
  76.   (unrealized (0 2))
  77.   (origs (nb (0 1)))
  78.   (comment "1 in cohort - 1 not yet seen"))
  79.  
  80. (defskeleton an_ssl_revised
  81.   (vars (nb cert text) (a b name) (k skey))
  82.   (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  83.   (defstrand init 3 (cert cert) (nb nb) (client a) (server b) (k k))
  84.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  85.   (non-orig (privk a) (privk b))
  86.   (uniq-orig nb k)
  87.   (operation encryption-test (displaced 2 1 init 3)
  88.     (enc cert-0 (enc a b k nb (privk a)) k) (0 2))
  89.   (traces
  90.     ((recv (enc k (pubk b))) (send (enc nb k))
  91.       (recv (enc cert (enc a b k nb (privk a)) k)))
  92.     ((send (enc k (pubk b))) (recv (enc nb k))
  93.       (send (enc cert (enc a b k nb (privk a)) k))))
  94.   (label 4)
  95.   (parent 2)
  96.   (unrealized)
  97.   (shape)
  98.   (maps ((0) ((a a) (b b) (k k) (nb nb) (cert cert))))
  99.   (origs (k (1 0)) (nb (0 1))))
  100.  
  101. (comment "Nothing left to do")

Raw Paste


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