Re: [isabelle] 转发 :the inductive approach analyze the NS protocol



Papers describing the modelling method are here: <http://www.cl.cam.ac.uk/~lp15/papers/protocols.html >

See especially <http://www.cl.cam.ac.uk/~lp15/papers/Auth/jcs.pdf>. The proof you mention is of a "possibility property" and is discussed on page 19 of that paper.

Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
15 JJ Thomson Avenue, Cambridge CB3 0FD, England
Tel: +44(0)1223 334623    Fax: +44(0)1223 334678


BEGIN:VCARD
VERSION:3.0
N:Paulson;Lawrence;;;
FN:Lawrence Paulson
ORG:University of Cambridge;Computer Laboratory
TITLE:Professor of Computational Logic
EMAIL;type=INTERNET;type=WORK:lp15 at cam.ac.uk
EMAIL;type=INTERNET;type=WORK;type=pref:Larry.Paulson at cl.cam.ac.uk
TEL;type=WORK;type=pref:01223 334623
TEL;type=CELL:07774 017623
TEL;type=CELL:50623
TEL;type=WORK;type=FAX:01223 334678
item1.ADR;type=WORK;type=pref:;;William Gates Building;15 JJ Thomson Avenue;CAMBS;CB3 0FD;United Kingdom
item1.X-ABADR:uk
item2.URL;type=pref:http\://www.cl.cam.ac.uk/users/lcp/
item2.X-ABLabel:_$!<HomePage>!$_
X-AIM;type=WORK;type=pref:LawrenceCPaulson
PHOTO;BASE64:
  TU0AKgAAGAaAOdjJx/wKCO+BwVepR/tZaoR/t5jKV/vdnK2KxN/r1Smt/oxGEp/rVOFJ/xctP9Sp
  SRMZax5zs6IM5jHOGr2bOeXw1SyZvTiIzWKtaIPeiRWZTcxv9OJyRM5ex6JHuT1F/q2eyqstagTF
  GP93s6vxKxsaIN6k2iGOdrV+vQWxRta0slGMYv8AXkAWGCTGGRav2HAsa1wlzr2CReqK1OUtaqXH
  JSUqWSv89nscyPIXKPLVW5PKyuRGsximNqWUwKpUCw1SG1TDzbGSZOJSTVzYWabzle7mbWiqMbev
  /hVSoVTcRFnQypxGgT/kUKsSm9AC0RCBRCw9q4wK1s6+s6KS6IVilsZW7LJP9CIQhP+63cxnPMnP
  MZb7oyWZb3UxOJShDfqAx7QJSiaTJ0pZSqyThGNu1hrL/CKCt0n6bMepZWlapY9kY95ap24qGt0h
  ybImpauJyZzjKE6rmms3SYuw3SwoZGqwGsxJjK+l0Ls2pqUva975sy+KPtslT/vY/pCQ8m6YRWuU
  gjmkQ9jWzJCD2kwlCklIYhykQchy0xKEIjyaJm4aoJs47iFrNjdRBBSss8lMMNOpZnJ2hzVuiqjq
  xgiFAxHGbBu4ty4rQr6aONN7NKWSkkCULTTPakz0TYoDhI9Bc8lrAyskoRibMuiAYiEkUvpEBAUs
  zL6UhDMS8AQDB/1azIMBCEMkqlHaqqpRURqoXsNyW98OpEldL2LNbdpPFq9TQm8eFq4Jexms5jWB
  RMaW5GaqQIf4xyu9g5vfHtCOUs8ok4QibCFVB/hjU5/hDVp/ggFL3gxegABCu9/LuCF6ARWJ/1o0
  1YszfK7zEu72pS5K2K/Qb0QMoDk2a6ars+qqPUBCq4xg2Cku25Vh0cXtHRkuCqIQ4NiyEf9RJNNq
  JUEwlbXvU9Uhy94IX+f4MX1WwcpMDFZXzn+iYQvGgLwAAIYPoIAVpg+C3ro2ZyRlUzuGl0UW1dVh
  H+NY9ruSjKl6qzquEm1B5Zkx3qOqCPa6kdiuvseRpPYuLKvtRW7sVqIDHcdZ6lpt9JNguAaxoC71
  ikWlamu9acdXa86lqPMgBWum85oUwXEMaRNrPOv0dNtMK02klQW6i9UjS6duzk7iKsl0z5DdecIh
  tyGp3Cygtgtt5Vln1U3gvFc4Poep4TemBszxt8elL/K6dXemgRp/NVnz/n89hN41akTH9+1HiIKn
  bKJNJr30m0zqj2/r0KXvW+bXwbz+FsRwCrvqfcRtYrcijg5BirtL5mUxHve+1VWrVXtvPcg85+bz
  XQr8eovwvDVGnvcao+KD7QWkEiaiaaEo/whM+LAVYk5HhrCtJMSs95omoF5Y2no36JDhlcNWTZYh
  HmwQEKWllLAhDMkOKWQUr5YCCL2csBBz7VopRRe3B+KjzVcl3aGZkFK/XvPNXyZlf0G35r5YPGiE
  7zmAQYjDBc0yYldkFNcNYmxrx/kNJsdVSJIogk3OwtV4Lb2MQ9OGzc4hHTiLFNVHkc5XxSiMJSAh
  rEW2hPNBSBhWoSgUq7Qce8VoeyUicDXKMLSVQlHvClAheSupWmmBjF8f6Y2BNBdBCJzL3o0Ogc89
  p6x7yYmuG8UUc5ECIp/L0Y+ITgiFFnkERdTKKiijeiaN4v81ChzCKoRaPbUXwNCXsP8LSYz2BaQ+
  lY4io50myD2eedSOyZplI2IwqkpCUhzCkaMKRJl5uOc+0GCsFXxqzc7BFp7QGEydLAM6JY3o6zdL
  ycmRDfFmt3GMUJuZRRrGukfHmh1HphR3mG1Bzc3p8LHCkueehJ0G0sJmJw41LTwMUpajksckTiUw
  I2JRYaZj2OlVslxg694KvVAAvd7ppnQS6qUwYiNIptQ3AAzYtLYm6vrmCXAmxRqOTGHPSGhZSywk
  2Ag1YEMUiRntp3S9RdPKXUsYoSsnhzDakNprTKvFPVSBan4EIlKkyPVGgov2Ci93PRtYA0EtFUI8
  x2qkyqHa2TYFWq5SCyw96Plgmqy4Z0MBjIGFqSaU5phWkgpyQwiZDBe0rpsSdUVcLYI5IYeC2dOB
  rVypna4iC1yPJjNNF+Lzo3JPMhQvd8z0LiS+sOzMypBatpRUAQsuBB0co4MCUc1pQ47zFkdRomxC
  HUEpKwe80hprUnEteYR388jl3rd/SueE8yIJmI9KdIbyxGOGnmcZLMs6FNRVqqglIQku1DYBB957
  Q3LQecy8+fZmbMHYugXosJGMKlDIoUa67JCPFGq3dyJljY6lStCTckwcw1kinySIQgY07LuOJjBH
  aF8WszDGSaBDlmrPdiurVXNSmnpWiFTKt0nXomZVjA57sFqCS+VZG1+crpNK7LYTNsR1SjC1o9lo
  o11GXUbIrZmzOIMQDeu+MYpZAilkWI9WWkqtVdGmSoZk3pSzemTNIzOvhlglGZCFOGcyWJzEfz2l
  Q9+OWZhzztW4jsk5dzhkorthlyl/PMV2rlXD2HQ0XK+K2QR1TnZbo8X0Y2HcwFGmNNgguqWXZoha
  amz5QyPApBSAAf8q0iyxlarsMYOVd6NxiUskp9ZM63gSeylJKr9GYMzsDOuhCn5EK+CkCDm4tMGY
  LUqDEvS86SltOFzyu0QHllDVIiOWtz5hIJMebJFcyWbKRmkYyCN5vBJMYwzKetcxxnCGsIUXJe23
  IIN6nBhCbBroVtRxM3oIa31o2VWUknz6KnScaeS1yl1FgpOFnxJmgK7V1GTarQtNNPQ0VRBcyC82
  Y3QYejxGN2YezDV6JtjiBIIF6zUXpIlIl3frz4Patcb44lkHuVOxi723tnPIsxHj/mZEZKxDxmT0
  zuONSs3sQsZTyQiWdds38kr1uNLIGLzXSvxXnyRXFChKClJsIyUm5if7u3QN4glmJhVeIYWDveqh
  ramzWNbeXgat9/KvW49xpjMdJQ1Xa2YjCZ2s0ZKfZXPJVkqDWpfGFt1BU1pwcvixEJVwOafF89+t
  DTELbeKUqhmHol3Clv49iSg9nryx3PdJEd10jsqRGr2rJHUiI8QX4dX48jv1SbLGBkCTX5Kfaa2V
  rmKWvLaoKeSb07cULMmy9nXLbUtMJ1cqglJStCXvJ+tJHvEkbnRqUk3ITLX5I+Y3+bHy9ah9z3bM
  LJEBampE+E+Ckco4juHeqiIW5Q4o4E90MSUixid+rULEN+ruII66tc4sWArwpet2rctWWGnQymtO
  /YPOrcQ2j8naXkr8H+DmQcPYEoUgE4ogAAHu5cIi5gKO5kzUQoiW8MIa+GG9B8u3AGo9CAJUDmJT
  AOKY2S+w/YOQrcLEd+MuJGxuIank7sporbAvAsnXC2/CKup8Qc2i+sPK8yIiFKveIgVaNMDGEIxZ
  BcbKEIJM1ALC3UoWh28Kmmq8o5D0u7D4IjB88CKWvylBDIXMSwVkCUk0YOaqbKAwakEoeWLMMWDG
  PeQiOQruOCnU9AnSbsxgtWQuEYiEvgp8JwJS7sOwnkg1BVBYbSJSEYM2DnDg3NDmhaKGMLDukc5q
  /+sa+GscqfF2sazWGdCOSRDY2bCik4V218k8xcKYDWbs+gteN6RMp9E0vU4qv2nm6cnw/SnmRMrc
  +2JOpWvavQIgVoVqD2SUEI/o9qJTHZFkGc+OF6o8wySiuy98saufB2zS5zHwzDABD8oWKpDgPeVG
  SCC0JSnG6hCm9YI8tKPKv7A7BFC1HGIGveXAxknUt5G6I2xqIvAonkHetecvBUSpFUS2xSPgXI9r
  DiL1BnHhFow0OcI8QCo8mMscIsobHyss1WzDCIwi0SQ4z2JCXOxQI3CNHCnq/LBc2ED2+Uzsp8R2
  WHA4pWIfE4M6xrKrI46c2TE0LyAQl8EISQDXDYPgXM1uPobKJC3MKMIqIRDouyIs1aV6JSj1CHH7
  LrF8KMw6s6LgI8S0JEz+qU0qgkm+e+AQl6Ck7S/IzwTsnUcIM7MdFHMlE4MclEJHBOPSdipKakr4
  MyM8U4mYEIM27hEC/pDkGsjyswkcy4KSkbBzBzLw8NJw1lF+Hu1iJ+J83qxaxOhW2UbsC1N+POCk
  Qyn3Mu/UnGKvBOFrMjKuxpKuM7OVMwnQ7dCOnULygim8RgR4WuJUcIZm7cZmPTBaKXDkGM+PNQ1C
  YyKsT0RQLmKRB9CFL0LA1iheo8ueI8SoWTKOEI0Gz+V2C0107cJMTeMc4pGkxs3up8IfMrMg+VIb
  MsI6NpG3Myxim6akE5PA08Ko7g/VDc9rNKKXFgdi5WIEkdPMKMIwMQnqxqQahnLUJIPfNtLo+NF9
  LwzNPsKQSC8ulENoqBCWMgvE/LQXG49Y2FDJBgvFOkQzBOlIhnDJQjGa+eiAxqkoUrBYFLPEdmdI
  LuCUCU9g8uVQfm/vRKsxHkIsIwPBIuI9FASCqAVGPePErE1KxFAFD7RuLCmWSCzy7dE4r1K0JVOn
  OnRZKPSQ2hGaNpSPUShnG2WqTzKnPIkoI2tWJUIegCMW3LGcPeC017S2qlTKo9ROIcIyIwtuMXKx
  FAKZMtOWQAhcpGjpJ2zEm2scpOMs2TUKlCU44oEo4pTY0TTaJFV7P4xY2TBdP1SWQVKPE1E1I0Gs
  PETcK+M8OMulWaPGV8ZUUXUm1AIlVAo9TNVEHuI4LAFqOY9ZVSJSlKMyG8UczYjyoYKC5wJNRqzA
  Oaz6My39XtN7VolEJFCNU0z6bK8unwMynbWBCm6rUOKZKPE8rsODV3I2XgKeJcLkWyIoLYIwJiIo
  LRYzWcywRhW7RNY/TPXawtXHUAUhSeS1DKYiFqfOFKWOD2yo52IyvEP2T0IYV0V2k7ZylcgTGS0B
  N68zXwSw2S+c8wJNWLOSnc+5EwRMnUx5LOQFYyMMIuOVY2IoRgIpW1W9HkJvY+/xaoJ0tU0ZV5Cm
  TMPeQadM6i8PXSF6YjbaTdFKOHFAxVN6lijioVZ6VtZ4nDP8nEz+ZnSOqBQoWqiFCdG/G+xgaqak
  DmPsJGFrHlO0KC1JYraoIlazJbW2/wK5a9VEeCKRTQpxUKkkJMnafeqAXcPeJ/LpL5XYIkQALjDM
  JtYFb8Ya10BzESD23+0JbO8pUa/ZCPBPYXI1KitdaW2CXqeaSaIYFabWTcJnUqK4OYITcs3MJio9
  Je7nU/c0y4PRBqrot2xgphL9SfFiG8Y6vAIUJNfQrsI+tNIHBU2SznBVN7Dg2bJRcHVVOVMnIncN
  aZG5cY/UtMDXFgY4OYukKgIZeiOcK+yxRKOVevZBBnPNa7ZFXAwyMQIKtKpynrUCfw3KT4vRZWu/
  apGdPweWS0pQPrX+lEMzBchrDJCW2elDCPIwTPf7T/fkQWIoE4RAJOGsG8KvebS6hm6+T0Ypg1gb
  HgsxiVgdesQozDVC3RaoJOwyISHfgxMeI2p0J0JnDNC8U4teMvdlcYI/jI4knKlRaGPfGLd2xslB
  fyMcxqxnGutWM64oxSJaouJHeaF7j1j7HhOAKo46PgqEJXgZcxPMbnHkIky0IkwsT0KHTNczc2kT
  ZGIyPGvZi8PEIgXaJsS4n4hYRBHkJAK+ZUy1QA1/dO8vfeMbSdQHVVjlKhFHVReEp8lJX5cbSwy0
  bSIwbSIoFrj0VQKWuOeShUUmqkUjIEp8UiK+NrQ3lspaJAMWrqIc73inaoHeJJgytq9Ez2XmjIyW
  bXPMKaIIQ0IwXcJsMbbPJRffhnMuTtBO6bE3C3I1I1Ky6MNNgG/s1sTASqSaa2IIVPlAJNYgeOgc
  L0SyJsSyUhC+pWVEvmpXIOJMcNHbBO8gRMpwIRl7jInyS3mOV0LuE48abXHkn3JYakPm7e6OI654
  0GMlbPUZYVli0WxpWOz0Q+QWcQuROGMXceIaHOHuXFgIaQz9OKgaqlgAMtKOno+a8gPYnQSsffBO
  xQJSxcSCnQJIIYxuvJOKlS9OeknDpIK0Io4+uQ0iZnKbCK3vSZcDbPYNKOLM6tT++YI+zyGdqAXk
  6Ox+JVeaGdh+KZmA9mIpn6lmdGXhoOLyXGI9S6iOvmxgUiIYMvkE6PskZmv68yxweW0CXEnzoMhU
  XjcUOJj0wAayyQXuwUhUwLR5nevQQveDKwxreFVRVwNOIpeZHlsrsrsPiDHhj+XEtMovHhsIX1MB
  tAL0JBsinQNJqlRDKOPmQ5CiTKIhIOI8S6vrU2PgeWS6S8lki+YEeagWg6V2UmVS7TOGZ+ldHQIJ
  OpC0Ryp7Ks/YiAnlgGVItMBzuwVLUoIpFgKptQGsHOHeI+8aGNr+i7BQJFuoqlmlBVrTqToLU3TX
  CjoTkJIRGcnEcPIOKXwydII9vC1oYaaSrRpSuYIYarK/S6Pee6x8nDsgI/rSmtYbA9IbpyUiIIKb
  siv7lInFIOP8IZvoKYKwpJr5PMGNr87EMzOGJsX1sQABQwIxvyQ7ma7hBbx9jIZ8JTqOUnIQcPoK
  S+fiqEbMKpm+1vuxxUaKLuQWIIr455xypXsYjTEdQwJUvTKpwatMVOMycMKW9ivqcOVOPeVFzVgG
  PhOLr3zNU2JsBjS6Vsewr9PIL1wThKSWIgPsKpOBw6ew9MlmwIPhuwwIxwhZt2hWgZ0Xr2VQcYrQ
  ktLCIZU3RDCjj7HlrF0rzIJNzCp2MXOVj5j7h9NQ08y1nMKZSxj3HlBW2mew7Du8Xr2OXp00TBRG
  AA8h0ofqPwK+PaIhqOVbU1m8VkVRvKVd0UhUhYgrt3mKoQ7EuK2bpyMZx9wsMfh3zkovPMUnqlIE
  P1xcKprLu2/mIIF6GdHhcfPNr8HOIiG9iAX+yQewX4LuwFzI4yaCBjx5sIOqn2r+wLwghVx4XgJN
  pN2Ui8ll45qs1uqFzGcMvq6O0UJSaGNNoKziXqld1bBR0BfctNr9NRwJNRSwIw7gIJsqP00609FU
  R5yLcdkWHP4H4uVUXqeXmKVoV2NIKXqPmL2cqkZ41uwKS5qr4yfKXp6khZV68hQ3MsXthbCjcYVI
  4oX148i52OaIP0IYSzO3PNrF4LiB7oOJ38P4K+n2WOtN4B6CKvh7LCIJyLNQVuaK9OVkuBx3oJ1C
  6Pz/tT0eLz44lSxV0WSyKo0UKXopsLX4v0TMnvGYNJqqcPKa7fKKpSMzw2Z8Pfy8XkexvDxGRAy1
  cfkX4L4JiByLHh8II3j96Hr9iBLGIgQWIxBWIZuJ4702JF2z3CPf5QdJugKpt39EqlS7ywVl8zBU
  v1GdRDGZ1GZnqcSsiLCiQaIgnaSCrUSzPxx5KaI8XsYSeQhZmL+qdx1jh77sRht7eb5ySOIYIAjE
  4nH+tV6xn+a0YjIKvV6/xiQiU/xSOSE/4sUn+GBCKYpFn+ezWc4SWi0/ykSomWilF5NJ4tFwBMwA
  OZAUpY/5ZEzmazG/zGWonQY1KYvLYvPpOjDnP6U/yUQhy/znKZRUqpVjXJqoY4mIRjUyUUp+MbDE
  BSMX/AoIe0IhH/DoenFarX+hIW/29e3+zms1n/f29gb/IYHd7yIZBY5PYanEYnKpcY5+QqsQsxEK
  xY41MX/NAAUtFIabJZOlD3P6DJzHWDGOY1XpXUYTXpRVqFU8xSa1lKhmZtU7TU5tF4zUJVKLG/4H
  BGNB7jDsRDG853fgW912t1X+53O94Tb43FX/HeFZ4jnctyuJ68xutdXKjas9oDnPYTtCEMY9qdY2
  j5q6k6mp+OauDXBCQqFAT2KA5KfKdBKkKui6wuMkDdn+yyNC0nzpsMSioK4e7wO7Ei9ROd53vA4q
  PousDiNhDSJRmi7MQ43yWI0qKXCUmCbIxGjQNyoDMpaqaiKoLSjqwprYtGrbYvuhMpwNDisKMu49
  j2oEci0n8JwyiyJhSzMyxs5KHIQYxalqkLxO8wbqvA7xzp1DqIIif4ILSiCQPNGbOuWHMvpQMY1y
  Ci6ovasTRs4z6aUWoEFyJKKqQSraTqEi49pau7xDmPaSDG/Et1HTxGLxN8uS+p1QpRQsMhTPrMIn
  MdAzyiZSrrDTRmMvyCmMhD0xdYrFIuDE9CFQ6dDmuEO0Q2FNDXLlpRrWCTssytCtA1tFSBI7awHD
  ye0QoKXUKt8uVDLhOLzBFEJUicty5elLpJU0up/R8dPK8lH2OijM3sJUEmdYSMSAisXzLgSvvIHM
  fWw5Cf4ijTLJOJVSV7fdC4jbNmNgn8htwzYcv7KbKQikj75ZBN2KpKd7Xg29sxpez70RL6NPvLky
  zJiNevUyLlwtYtayDW0ZMUqdkqmCE9YWzSNMgjFCjXVSyWinE9z1W8fUQGLl2XRDQICAAA4BAAAD
  AAAAAQAsAAABAQADAAAAAQBAAAABAgADAAAABAAAGLQBAwADAAAAAQAFAAABBgADAAAAAQACAAAB
  EQAEAAAAAQAAAAgBFQADAAAAAQAEAAABFgAEAAAAAQAAALoBFwAEAAAAAQAAF/4BGgAFAAAAAQAA
  GLwBGwAFAAAAAQAAGMQBHAADAAAAAQABAAABKAADAAAAAQACAAABUgADAAAAAQABAAAAAAAAAAgA
  CAAIAAgACvyAAAAnEAAK/IAAACcQ
CATEGORIES:Personal
X-ABUID:F9DA5726-C706-11D6-ABE7-00039384D4B8\:ABPerson
END:VCARD


On 20 Mar 2008, at 02:55, jwang whu.edu.cn (jwang) wrote:
   I have processed the (/Isabelle/src/HOL/Auth/)NS_Public_Bad file in
Isabelle,but I am puzzled by some result from Isabelle.For example,



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.